@@ -1311,8 +1311,24 @@ loadSource lidr f toline
13111311 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
13121312 let syntax = defaultSyntax{ syn_namespace = reverse mname,
13131313 maxline = toline }
1314+ ist <- getIState
1315+ -- Save the span from parsing the module header, because
1316+ -- an empty program parse might obliterate it.
1317+ let oldSpan = idris_parsedSpan ist
13141318 ds' <- parseProg syntax f file pos
13151319
1320+ case (ds', oldSpan) of
1321+ ([], Just fc) ->
1322+ -- If no program elements were parsed, we dind't
1323+ -- get a loaded region in the IBC file. That
1324+ -- means we need to add it back.
1325+ do ist <- getIState
1326+ putIState ist { idris_parsedSpan = oldSpan
1327+ , ibc_write = IBCParsedRegion fc :
1328+ ibc_write ist
1329+ }
1330+ _ -> return ()
1331+
13161332 -- Parsing done, now process declarations
13171333
13181334 let ds = namespaces mname ds'