diff options
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
2 files changed, 8 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 95cecb7fe2..3bcefa6388 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -109,9 +109,13 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = set_id_for_feedback ?route (Feedback.State id); Aux_file.record_in_aux_set_at loc; prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr)); - try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) + let a = Lexer.com_state () in + try + Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)); + Lexer.restore_com_state a with e -> let e = Errors.push e in + Lexer.restore_com_state a; iraise Hooks.(call_process_error_once e) end diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1f7b947e93..177f3c775b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -230,7 +230,9 @@ let rec vernac_com checknav (loc,com) = if do_beautify () then pr_new_syntax loc (Some com); if !Flags.time then display_cmd_header loc com; let com = if !Flags.time then VernacTime [loc,com] else com in - interp com + let a = Lexer.com_state () in + interp com; + Lexer.restore_com_state a with reraise -> let (reraise, info) = Errors.push reraise in Format.set_formatter_out_channel stdout; |