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.

7 files changed, 32 insertions, 23 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 7f4bc149d..8291e7462 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -77,17 +77,6 @@ open Pp_control
    \end{description}
  *)
 
-let comments = ref []
-
-let rec split_com comacc acc pos = function
-    [] -> comments := List.rev acc; comacc
-  | ((b,e),c as com)::coms ->
-      (* Take all comments that terminates before pos, or begin exactly
-         at pos (used to print comments attached after an expression) *)
-      if e<=pos || pos=b then split_com (c::comacc) acc pos coms
-      else  split_com comacc (com::acc) pos coms
-
-
 type block_type =
   | Pp_hbox of int
   | Pp_vbox of int
@@ -111,7 +100,7 @@ type 'a ppcmd_token =
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
   | Ppcmd_close_tbox
-  | Ppcmd_comment of int
+  | Ppcmd_comment of string list
   | Ppcmd_open_tag of Tag.t
   | Ppcmd_close_tag
 
@@ -177,7 +166,7 @@ let tab () = Glue.atom(Ppcmd_set_tab)
 let fnl () = Glue.atom(Ppcmd_force_newline)
 let pifb () = Glue.atom(Ppcmd_print_if_broken)
 let ws n = Glue.atom(Ppcmd_white_space n)
-let comment n = Glue.atom(Ppcmd_comment n)
+let comment l = Glue.atom(Ppcmd_comment l)
 
 (* derived commands *)
 let mt () = Glue.empty
@@ -321,8 +310,7 @@ let pp_dirs ?pp_tag ft =
         com_brk ft; Format.pp_force_newline ft ()
     | Ppcmd_print_if_broken   ->
         com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ()))
-    | Ppcmd_comment i         ->
-        let coms = split_com [] [] i !comments in
+    | Ppcmd_comment coms      ->
 (*        Format.pp_open_hvbox ft 0;*)
         List.iter (pr_com ft) coms(*;
         Format.pp_close_box ft ()*)
diff --git a/lib/pp.mli b/lib/pp.mli
index 3bd560812..f607e99db 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -23,8 +23,7 @@ val ws    : int -> std_ppcmds
 val mt    : unit -> std_ppcmds
 val ismt  : std_ppcmds -> bool
 
-val comment  : int -> std_ppcmds
-val comments : ((int * int) * string) list ref
+val comment  : string list -> std_ppcmds
 
 (** {6 Manipulation commands} *)
 
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 777cdc9bf..181c4b7fd 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -340,18 +340,29 @@ let comm_loc bp = match !comment_begin with
 | None -> comment_begin := Some bp
 | _ -> ()
 
+let comments = ref []
 let current_comment = Buffer.create 8192
 let between_commands = ref true
 
+let rec split_comments comacc acc pos = function
+    [] -> comments := List.rev acc; comacc
+  | ((b,e),c as com)::coms ->
+      (* Take all comments that terminates before pos, or begin exactly
+         at pos (used to print comments attached after an expression) *)
+      if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
+      else split_comments comacc (com::acc) pos coms
+
+let extract_comments pos = split_comments [] [] pos !comments
+
 type comments_state = int option * string * bool * ((int * int) * string) list
 let restore_comments_state (o,s,b,c) =
   comment_begin := o;
   Buffer.clear current_comment; Buffer.add_string current_comment s;
   between_commands := b;
-  Pp.comments := c
+  comments := c
 let default_comments_state = (None,"",true,[])
 let comments_state () =
-  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !Pp.comments) in
+  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) in
   restore_comments_state default_comments_state; s
 
 let real_push_char c = Buffer.add_char current_comment c
@@ -390,7 +401,7 @@ let comment_stop ep =
              ++ str current_s ++str"' ending at  "
              ++ int ep);
           ep-1 in
-    Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
+    comments := ((bp,ep),current_s) :: !comments);
   Buffer.clear current_comment;
   comment_begin := None;
   between_commands := false
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 2c05d6a95..3ad49eb74 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -36,6 +36,10 @@ val unfreeze : frozen_t -> unit
 
 val xml_output_comment : (string -> unit) Hook.t
 
+(* Retrieve the comments lexed at a given location of the stream
+   currently being processeed *)
+val extract_comments : int -> string list
+
 val terminal : string -> Tok.t
 
 (** The lexer of Coq: *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index fa5a70899..c94650f1e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -129,7 +129,7 @@ end) = struct
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if Flags.do_beautify() && not (Int.equal n 0) then comment n
+    if Flags.do_beautify() && not (Int.equal n 0) then comment (CLexer.extract_comments n)
     else mt()
 
   let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 906b463a8..57a1d957e 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -11,5 +11,9 @@ open Pp
 let pr_located pr (loc, x) =
   if Flags.do_beautify () && loc <> Loc.ghost then
     let (b, e) = Loc.unloc loc in
-    Pp.comment b ++ pr x ++ Pp.comment e
+    (* Side-effect: order matters *)
+    let before = Pp.comment (CLexer.extract_comments b) in
+    let x = pr x in
+    let after = Pp.comment (CLexer.extract_comments e) in
+    before ++ x ++ after
   else pr x
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5db604237..b8e44db9a 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;