From 25b0a871bde109788492992f1cb417e7e163ffa3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Oct 2016 22:02:12 +0200
Subject: Fixing beautification to file.

---
 toplevel/vernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 55f3a31a34..bdd834d52f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -132,7 +132,7 @@ let pr_new_syntax loc ocom =
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() 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 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
     Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
-- 
cgit v1.2.3


From 8a8caba36ea6b0fd67e026ee3833d3b5b25af56d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 7 Oct 2016 16:38:26 +0200
Subject: Attaching all extra imperative components of the lexer/parser state
 to the state of parsable streams, so that different lexing/parsing processes
 can be started independently without conflicting.

Note however that these different lexing/parsing processes cannot be
run concurrently as they still work on the same piece of global memory
(i.e. calls to entry_parse should remain atomic). To go further, one
would typically need to be able to functionally pass the lexing state
to each call to the lexer.

Note that currently the beautifier is also running in the context of a
lexer/parser state (for the mapping of location to comments).

In particular, this fixes #5102 (parsing/lexing of bullets depending on
the lexing state which was global).
---
 toplevel/coqloop.ml  | 12 +++++++-----
 toplevel/coqloop.mli |  2 +-
 toplevel/vernac.ml   | 29 +++++++++++++----------------
 toplevel/vernac.mli  |  4 ++--
 4 files changed, 23 insertions(+), 24 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 69d68bd357..bdcfa8336d 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,10 +274,12 @@ let rec discard_to_dot () =
     | End_of_input -> raise End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_sentence () =
+let read_eval_sentence () =
   try
-    let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in
-    CWarnings.set_current_loc loc; r
+    let input = (top_buffer.tokens, None) in
+    let (loc, _ as r) = Vernac.parse_sentence input in
+    CWarnings.set_current_loc loc;
+    Vernac.eval_expr input r
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
@@ -298,7 +300,7 @@ let do_vernac () =
   if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
-    Vernac.eval_expr (read_sentence ())
+    read_eval_sentence ()
   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 bdd834d52f..5db6042371 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,7 +124,7 @@ 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
@@ -138,20 +138,20 @@ let pr_new_syntax loc ocom =
   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 +182,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 +194,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 +213,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 +237,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 +246,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 +261,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
-- 
cgit v1.2.3


From b8ae2de5be242bbd1e34ec974627c81f99b16d23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Oct 2016 22:51:09 +0200
Subject: Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
 done by the Ppcmd_comment token) and so that lexing/parsing side-effects are
 collected at the same place, i.e. in CLexer.

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

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5db6042371..b8e44db9a7 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -128,11 +128,14 @@ 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
-    Pp.msg_with !Pp_control.std_ft (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;
-- 
cgit v1.2.3


From e3798c52c3bd52d43fa84feedd7caaa4def57db8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Oct 2016 15:47:43 +0200
Subject: Fixing #5133 (error reporting delayed).

I wrongly moved call to the function interpreting commands within a
different try-with block in 8a8caba36e.
---
 toplevel/coqloop.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index bdcfa8336d..71e1f9593d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -274,12 +274,10 @@ let rec discard_to_dot () =
     | End_of_input -> raise End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_eval_sentence () =
+let read_sentence input =
   try
-    let input = (top_buffer.tokens, None) in
     let (loc, _ as r) = Vernac.parse_sentence input in
-    CWarnings.set_current_loc loc;
-    Vernac.eval_expr input r
+    CWarnings.set_current_loc loc; r
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
@@ -300,7 +298,8 @@ let do_vernac () =
   if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
-    read_eval_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
-- 
cgit v1.2.3