Merge branch 'v8.6'

4 files changed, 25 insertions, 24 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 69d68bd357..71e1f9593d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -23,7 +23,7 @@ type input_buffer = {
   mutable str : string; (* buffer of already read characters *)
   mutable len : int;    (* number of chars in the buffer *)
   mutable bols : int list; (* offsets in str of beginning of lines *)
-  mutable tokens : Gram.parsable; (* stream of tokens *)
+  mutable tokens : Gram.coq_parsable; (* stream of tokens *)
   mutable start : int } (* stream count of the first char of the buffer *)
 
 (* Double the size of the buffer. *)
@@ -274,9 +274,9 @@ let rec discard_to_dot () =
     | End_of_input -> raise End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_sentence () =
+let read_sentence input =
   try
-    let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in
+    let (loc, _ as r) = Vernac.parse_sentence input in
     CWarnings.set_current_loc loc; r
   with reraise ->
     let reraise = CErrors.push reraise in
@@ -298,7 +298,8 @@ let do_vernac () =
   if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
-    Vernac.eval_expr (read_sentence ())
+    let input = (top_buffer.tokens, None) in
+    Vernac.eval_expr input (read_sentence input)
   with
     | End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 00554da308..e40353e0f9 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -18,7 +18,7 @@ type input_buffer = {
   mutable str : string; (** buffer of already read characters *)
   mutable len : int;    (** number of chars in the buffer *)
   mutable bols : int list; (** offsets in str of begining of lines *)
-  mutable tokens : Pcoq.Gram.parsable; (** stream of tokens *)
+  mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *)
   mutable start : int } (** stream count of the first char of the buffer *)
 
 (** The input buffer of stdin. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 07bccb5329..a37859c9ca 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,34 +124,37 @@ let set_formatter_translator() =
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
-let pr_new_syntax loc ocom =
+let pr_new_syntax_in_context loc ocom =
   let loc = Loc.unloc loc in
   if !beautify_file then set_formatter_translator();
   let fs = States.freeze ~marshallable:`No in
+  (* Side-effect: order matters *)
+  let before = comment (CLexer.extract_comments (fst loc)) in
   let com = match ocom with
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
+  let after = comment (CLexer.extract_comments (snd loc)) in
   if !beautify_file then
-    Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+    Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
   else
     Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
+let pr_new_syntax (po,_) loc ocom =
+  (* Reinstall the context of parsing which includes the bindings of comments to locations *)
+  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom
+
 let save_translator_coqdoc () =
   (* translator state *)
   let ch = !chan_beautify in
-  let cl = !Pp.comments in
-  let cs = CLexer.com_state() in
   (* end translator state *)
   let coqdocstate = CLexer.location_table () in
-  ch,cl,cs,coqdocstate
+  ch,coqdocstate
 
-let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
+let restore_translator_coqdoc (ch,coqdocstate) =
   if !Flags.beautify_file then close_out !chan_beautify;
   chan_beautify := ch;
-  Pp.comments := cl;
-  CLexer.restore_com_state cs;
   CLexer.restore_location_table coqdocstate
 
 (* For coqtop -time, we display the position in the file,
@@ -182,7 +185,7 @@ let print_cmd_header loc com =
   Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Pp_control.std_ft ()
 
-let rec vernac_com checknav (loc,com) =
+let rec vernac_com input checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
@@ -194,7 +197,6 @@ let rec vernac_com checknav (loc,com) =
 	if !Flags.beautify_file then
 	  begin
 	    chan_beautify := open_out (f^beautify_suffix);
-	    Pp.comments := []
           end;
 	begin
 	  try
@@ -214,13 +216,11 @@ let rec vernac_com checknav (loc,com) =
   in
     try
       checknav loc com;
-      if do_beautify () then pr_new_syntax loc (Some com);
+      if do_beautify () then pr_new_syntax input loc (Some com);
       (* XXX: This is not 100% correct if called from an IDE context *)
       if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
-      let a = CLexer.com_state () in
-      interp com;
-      CLexer.restore_com_state a
+      interp com
     with reraise ->
       let (reraise, info) = CErrors.push reraise in
       Format.set_formatter_out_channel stdout;
@@ -240,7 +240,7 @@ and read_vernac_file verbosely s =
     while true do
       let loc_ast = parse_sentence input in
       CWarnings.set_current_loc (fst loc_ast);
-      vernac_com checknav loc_ast;
+      vernac_com input checknav loc_ast;
     done
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
@@ -249,7 +249,7 @@ and read_vernac_file verbosely s =
     match e with
       | End_of_input ->
           if do_beautify () then
-            pr_new_syntax (Loc.make_loc (max_int,max_int)) None
+            pr_new_syntax input (Loc.make_loc (max_int,max_int)) None
       | reraise ->
 	 iraise (disable_drop e, info)
 
@@ -264,7 +264,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com checknav loc_ast
+let eval_expr input loc_ast = vernac_com input checknav loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 7bfddd9470..2fd86ddc22 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -11,7 +11,7 @@
 (** Read a vernac command on the specified input (parse only).
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
-val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
+val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option ->
  Loc.t * Vernacexpr.vernac_expr
 
 (** Reads and executes vernac commands from a stream.
@@ -21,7 +21,7 @@ exception End_of_input
 
 val just_parsing : bool ref
 
-val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit
+val eval_expr : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -> unit
 
 (** Set XML hooks *)
 val xml_start_library : (unit -> unit) Hook.t