diff options
| author | Pierre-Marie Pédrot | 2014-04-25 13:59:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-25 14:00:43 +0200 |
| commit | b35edb34769fecd4dbdf7030222ba3078eab1c93 (patch) | |
| tree | 0efb56c5711b0a2d9ae8eef5b7792b734899f2be /toplevel | |
| parent | a5e0b28f9344744edf2209001fe047b1535775f6 (diff) | |
Fixing various backtrace recordings.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 5 | ||||
| -rw-r--r-- | toplevel/stm.ml | 9 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 5 |
3 files changed, 14 insertions, 5 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index b930c4eec9..07a398903c 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -290,7 +290,10 @@ let rec discard_to_dot () = let read_sentence () = try Vernac.parse_sentence (top_buffer.tokens, None) - with reraise -> discard_to_dot (); raise reraise + with reraise -> + let reraise = Errors.push reraise in + discard_to_dot (); + raise reraise (** [do_vernac] reads and executes a toplevel phrase, and print error messages when an exception is raised, except for the following: diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 875c933efa..cc6b7d0c40 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -762,8 +762,9 @@ end = struct (* {{{ *) { verbose = false; loc; expr = (VernacEndProof (Proved (true,None))) }; Some proof - with e -> (try - match Stateid.get e with + with e -> + let e = Errors.push e in + (try match Stateid.get e with | None -> Pp.pperrnl Pp.( str"File " ++ str name ++ str ": proof of " ++ str s ++ @@ -891,7 +892,8 @@ end = struct (* {{{ *) if WorkersPool.is_empty () then if !Flags.compilation_mode = Flags.BuildVi then begin let force () : Entries.proof_output list Future.assignement = - try `Val (build_proof_here_core loc stop ()) with e -> `Exn e in + try `Val (build_proof_here_core loc stop ()) + with e -> let e = Errors.push e in `Exn e in let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in let uuid = Future.uuid f in TQueue.push queue (TaskBuildProof @@ -1578,6 +1580,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in (u,a,true), p with e -> + let e = Errors.push e in Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e); exit 1 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1854e11265..22e2f0c545 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -346,7 +346,10 @@ let dump_universes_gen g s = Univ.dump_universes output_constraint g; close (); msg_info (str ("Universes written to file \""^s^"\".")) - with reraise -> close (); raise reraise + with reraise -> + let reraise = Errors.push reraise in + close (); + raise reraise let dump_universes sorted s = let g = Global.universes () in |