From eb87cdaeb252d758b6a76b36867254823169576b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 9 Oct 2016 08:18:52 +0200
Subject: A tentative fix for #5102 (bullets parsing broken by calls to
 parse_entry).

More precisely, commands that calls parse_entry put the lexer in an
inconsistent state, breaking the lexing of bullet which relies on it.

(Not to be pushed to v8.6 which has a better fix).
---
 stm/stm.ml         | 6 +++++-
 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;
-- 
cgit v1.2.3