15a76ff · Idris-dev · git.iko.soy

1311 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]

1312 let syntax = defaultSyntax{ syn_namespace = reverse mname,

1313 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

1314 ds' <- parseProg syntax f file pos

1318 ds' <- parseProg syntax f file pos

1315

1319

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+

1316 -- Parsing done, now process declarations

1332 -- Parsing done, now process declarations

1317

1333

1318 let ds = namespaces mname ds'

1334 let ds = namespaces mname ds'