diff options
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 9718ccad..85234775 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2822,7 +2822,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, [])) end) -and elabSgn (env, denv) (sgn, loc) = +and elabSgn (env, denv) (sgn, loc): (L'.sgn * D.goal list) = case sgn of L.SgnConst sgis => let @@ -4187,6 +4187,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = | NONE => let val () = if !verbose then TextIO.print ("CHECK: " ^ x ^ "\n") else () + val () = ErrorMsg.startElabStructure x val () = if x = "Basis" then raise Fail "Not allowed to redefine structure 'Basis'" @@ -4228,7 +4229,10 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = L'.StrFun _ => () | _ => strError env (FunctorRebind loc)) | _ => (); - Option.map (fn tm => ModDb.insert (dNew, tm)) tmo; + Option.map (fn tm => ModDb.insert (dNew, + tm, + ErrorMsg.stopElabStructureAndGetErrored x + )) tmo; ([dNew], (env', denv', gs' @ gs)) end) @@ -4243,6 +4247,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = end | NONE => let + val () = ErrorMsg.startElabStructure x + val (sgn', gs') = enterSignature (fn () => elabSgn (env, denv) sgn) val (env', n) = E.pushStrNamed env x sgn' @@ -4261,7 +4267,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = epreface ("item", p_sgn_item env sgi))) | _ => raise Fail "FFI signature isn't SgnConst"; - Option.map (fn tm => ModDb.insert (dNew, tm)) tmo; + Option.map (fn tm => ModDb.insert (dNew, tm, ErrorMsg.stopElabStructureAndGetErrored x)) tmo; ([dNew], (env', denv, enD gs' @ gs)) end) @@ -4754,9 +4760,11 @@ and elabStr (env, denv) (str, loc) = fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env -fun elabFile basis basis_tm topStr topSgn top_tm env file = +fun elabFile basis basis_tm topStr topSgn top_tm env changeEnv file = let val () = ModDb.snapshot () + val () = ErrorMsg.resetStructureTracker () + val () = mayDelay := true val () = delayedUnifs := [] @@ -4779,7 +4787,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = val (env', basis_n) = E.pushStrNamed env "Basis" sgn in - ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm); + ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm, false); (* TODO: also check for errors? *) (basis_n, env', sgn) end | SOME (d' as (L'.DFfiStr (_, basis_n, sgn), _)) => @@ -4838,7 +4846,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = val (env', top_n) = E.pushStrNamed env' "Top" topSgn in - ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm); + ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm, false); (* TODO: also check for errors? *) (top_n, env', topSgn, topStr) end | SOME (d' as (L'.DStr (_, top_n, topSgn, topStr), _)) => @@ -4849,6 +4857,8 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} + val env' = changeEnv env' + fun elabDecl' x = (resetKunif (); resetCunif (); @@ -5121,11 +5131,6 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = else (); - if ErrorMsg.anyErrors () then - ModDb.revert () - else - (); - (*Print.preface("File", ElabPrint.p_file env file);*) (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) |