From a4ff40931201f91cde79c212a9d2cc19a62b8128 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 10 Apr 2016 17:04:44 +0200
Subject: Protect the beautifier from change in the lexer state (typically by
 calling Pcoq.parse_string, what some plugins such as coretactics, are doing,
 thus breaking the beautification of "Declare ML Module").

---
 toplevel/vernac.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 0a32c88d64..94972e272f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -228,7 +228,9 @@ let rec vernac_com verbose 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 = CLexer.com_state () in
+      interp com;
+      CLexer.restore_com_state a
     with reraise ->
       let (reraise, info) = Errors.push reraise in
       Format.set_formatter_out_channel stdout;
-- 
cgit v1.2.3