[toplevel] Move beautify to its own pass.

We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.

We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!

11 files changed, 115 insertions, 101 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 52a6fe16c..d7e3751fd 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -384,16 +384,6 @@ 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
-
 (* The state of the lexer visible from outside *)
 type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source
 
@@ -410,6 +400,8 @@ let release_lexer_state = get_lexer_state
 let drop_lexer_state () =
     set_lexer_state (init_lexer_state Loc.ToplevelInput)
 
+let get_comment_state (_,_,_,c,_) = c
+
 let real_push_char c = Buffer.add_char current_comment c
 
 (* Add a char if it is between two commands, if it is a newline or
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 5f4e10f14..2d35571f1 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -55,7 +55,4 @@ val get_lexer_state : unit -> lexer_state
 val release_lexer_state : unit -> lexer_state
 [@@ocaml.deprecated "Use get_lexer_state"]
 val drop_lexer_state : unit -> unit
-
-(* Retrieve the comments lexed at a given location of the stream
-   currently being processeed *)
-val extract_comments : int -> string list
+val get_comment_state : lexer_state -> ((int * int) * string) list
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 7a51908d9..fec26f941 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -88,7 +88,9 @@ module type S =
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
-  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
+
+  val comment_state : coq_parsable -> ((int * int) * string) list
+
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 
@@ -105,6 +107,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+
   type coq_parsable = parsable * CLexer.lexer_state ref
 
   let parsable ?(file=Loc.ToplevelInput) c =
@@ -129,15 +132,8 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
       let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
       Loc.raise ~loc e
 
-  let with_parsable (p,state) f x =
-    CLexer.set_lexer_state !state;
-    try
-      let a = f x in
-      state := CLexer.get_lexer_state ();
-      a
-    with e ->
-      CLexer.drop_lexer_state ();
-      raise e
+  let comment_state (p,state) =
+    CLexer.get_comment_state !state
 
   let entry_print ft x = Entry.print ft x
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f36250176..1b330aa04 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -78,7 +78,9 @@ module type S =
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
-  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
+
+  (* Get comment parsing information from the Lexer *)
+  val comment_state : coq_parsable -> ((int * int) * string) list
 
   (* Apparently not used *)
   val srules' : production_rule list -> symbol
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 3c7095505..0d84e1b9e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -149,7 +149,7 @@ let tag_var = tag Tag.variable
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
+    if !Flags.beautify && not (Int.equal n 0) then comment (Pputils.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 e779fc5fc..3d72c8da3 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -13,14 +13,26 @@ open Misctypes
 open Locus
 open Genredexpr
 
+let beautify_comments = ref []
+
+let rec split_comments comacc acc pos = function
+  | [] -> beautify_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 !beautify_comments
+
 let pr_located pr (loc, x) =
   match loc with
   | Some loc when !Flags.beautify ->
     let (b, e) = Loc.unloc loc in
     (* Side-effect: order matters *)
-    let before = Pp.comment (CLexer.extract_comments b) in
+    let before = Pp.comment (extract_comments b) in
     let x = pr x in
-    let after = Pp.comment (CLexer.extract_comments e) in
+    let after = Pp.comment (extract_comments e) in
     before ++ x ++ after
   | _ -> pr x
 
diff --git a/printing/pputils.mli b/printing/pputils.mli
index ec5c32fc4..483bd0ae3 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -37,3 +37,9 @@ val pr_red_expr_env : Environ.env -> Evd.evar_map ->
 
 val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
 val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t
+
+(* The comments interface is imperative due to the printer not
+   threading it, this could be solved using a better data
+   structure. *)
+val beautify_comments : ((int * int) * string) list ref
+val extract_comments : int -> string list
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index d8aaf3db8..6f461fd53 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -26,7 +26,7 @@ let load_rcfile ~rcfile ~time ~state =
       match rcfile with
       | Some rcfile ->
         if CUnix.file_readable_p rcfile then
-          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state rcfile
+          Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
       | None ->
 	try
@@ -37,7 +37,7 @@ let load_rcfile ~rcfile ~time ~state =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state inferedrc
+          Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc
         with Not_found -> state
 	(*
 	Flags.if_verbose
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 26ede1834..d4ccfdf1b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -92,10 +92,10 @@ let outputstate opts =
 (******************************************************************************)
 let load_vernacular opts ~state =
   List.fold_left
-    (fun state (f_in, verbosely) ->
+    (fun state (f_in, echo) ->
       let s = Loadpath.locate_file f_in in
       (* Should make the beautify logic clearer *)
-      let load_vernac f = Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true ~state f in
+      let load_vernac f = Vernac.load_vernac ~time:opts.time ~echo ~interactive:false ~check:true ~state f in
       if !Flags.beautify
       then Flags.with_option Flags.beautify_file load_vernac f_in
       else load_vernac s
@@ -194,7 +194,7 @@ let ensure_exists f =
     fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
-let compile opts ~verbosely ~f_in ~f_out =
+let compile opts ~echo ~f_in ~f_out =
   let open Vernac.State in
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
@@ -232,7 +232,7 @@ let compile opts ~verbosely ~f_in ~f_out =
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       let wall_clock1 = Unix.gettimeofday () in
-      let state = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false ~state long_f_dot_v in
+      let state = Vernac.load_vernac ~time:opts.time ~echo ~check:true ~interactive:false ~state long_f_dot_v in
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
@@ -273,7 +273,7 @@ let compile opts ~verbosely ~f_in ~f_out =
       let state = { doc; sid; proof = None } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
-      let state = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false ~state long_f_dot_v in
+      let state = Vernac.load_vernac ~time:opts.time ~echo ~check:false ~interactive:false ~state long_f_dot_v in
       let doc = Stm.finish ~doc:state.doc in
       check_pending_proofs ();
       let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
@@ -288,17 +288,17 @@ let compile opts ~verbosely ~f_in ~f_out =
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile opts ~verbosely ~f_in ~f_out =
+let compile opts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile opts ~verbosely ~f_in ~f_out;
+  compile opts ~echo ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
 
-let compile_file opts (f_in, verbosely) =
+let compile_file opts (f_in, echo) =
   if !Flags.beautify then
     Flags.with_option Flags.beautify_file
-      (fun f_in -> compile opts ~verbosely ~f_in ~f_out:None) f_in
+      (fun f_in -> compile opts ~echo ~f_in ~f_out:None) f_in
   else
-    compile opts ~verbosely ~f_in ~f_out:None
+    compile opts ~echo ~f_in ~f_out:None
 
 let compile_files opts =
   let compile_list = List.rev opts.compile_list in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a84990f91..5d3addfec 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -40,37 +40,6 @@ let vernac_echo ?loc in_chan = let open Loc in
       Feedback.msg_notice @@ str @@ really_input_string in_chan len
     ) loc
 
-(* vernac parses the given stream, executes interpfun on the syntax tree it
- * parses, and is verbose on "primitives" commands if verbosely is true *)
-
-let beautify_suffix = ".beautified"
-
-let set_formatter_translator ch =
-  let out s b e = output_substring ch s b e in
-  let ft = Format.make_formatter out (fun () -> flush ch) in
-  Format.pp_set_max_boxes ft max_int;
-  ft
-
-let pr_new_syntax_in_context ?loc ft_beautify ocom =
-  let loc = Option.cata Loc.unloc (0,0) loc in
-  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 !Flags.beautify_file then
-    (Pp.pp_with ft_beautify (hov 0 (before ++ com ++ after));
-     Format.pp_print_flush ft_beautify ())
-  else
-    Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
-  States.unfreeze fs
-
-let pr_new_syntax ?loc po ft_beautify 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 ft_beautify) ocom
-
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
 
@@ -174,18 +143,16 @@ let interp_vernac ~time ~check ~interactive ~state (loc,com) =
       end in iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
-let load_vernac ~time ~verbosely ~check ~interactive ~state file =
-  let ft_beautify, close_beautify =
-    if !Flags.beautify_file then
-      let chan_beautify = open_out (file^beautify_suffix) in
-      set_formatter_translator chan_beautify, fun () -> close_out chan_beautify;
-    else
-      !Topfmt.std_ft, fun () -> ()
-  in
+let load_vernac_core ~time ~echo ~check ~interactive ~state file =
+  (* Keep in sync *)
   let in_chan = open_utf8_file_in file in
-  let in_echo = if verbosely then Some (open_utf8_file_in file) else None in
+  let in_echo = if echo then Some (open_utf8_file_in file) else None in
+  let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
+
   let in_pa   = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
   let rstate  = ref state in
+  (* For beautify, list of parsed sids *)
+  let rids    = ref [] in
   let open State in
   try
     (* we go out of the following infinite loop when a End_of_input is
@@ -212,36 +179,78 @@ let load_vernac ~time ~verbosely ~check ~interactive ~state file =
        *)
       in
       (* Printing of vernacs *)
-      if !Flags.beautify then pr_new_syntax ?loc in_pa ft_beautify (Some ast);
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
       let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) (loc, ast) in
+      rids := state.sid :: !rids;
       rstate := state;
     done;
-    !rstate
+    input_cleanup ();
+    !rstate, !rids, Pcoq.Gram.comment_state in_pa
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
-    close_in in_chan;
-    Option.iter close_in in_echo;
+    input_cleanup ();
     match e with
-      | Stm.End_of_input ->
-          (* Is this called so comments at EOF are printed? *)
-          if !Flags.beautify then
-            pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None;
-          if !Flags.beautify_file then close_beautify ();
-          !rstate
-      | reraise ->
-         if !Flags.beautify_file then close_beautify ();
-	 iraise (disable_drop e, info)
-
-(** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
-   It executes one vernacular command. By default the command is
-   considered as non-state-preserving, in which case we add it to the
-   Backtrack stack (triggering a save of a frozen state and the generation
-   of a new state label). An example of state-preserving command is one coming
-   from the query panel of Coqide. *)
+    | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa
+    | reraise -> iraise (disable_drop e, info)
 
 let process_expr ~time ~state loc_ast =
   checknav_deep loc_ast;
   interp_vernac ~time ~interactive:true ~check:true ~state loc_ast
+
+(******************************************************************************)
+(* Beautify-specific code                                                     *)
+(******************************************************************************)
+
+(* vernac parses the given stream, executes interpfun on the syntax tree it
+ * parses, and is verbose on "primitives" commands if verbosely is true *)
+let beautify_suffix = ".beautified"
+
+let set_formatter_translator ch =
+  let out s b e = output_substring ch s b e in
+  let ft = Format.make_formatter out (fun () -> flush ch) in
+  Format.pp_set_max_boxes ft max_int;
+  ft
+
+let pr_new_syntax ?loc ft_beautify ocom =
+  let loc = Option.cata Loc.unloc (0,0) loc in
+  let before = comment (Pputils.extract_comments (fst loc)) in
+  let com = Option.cata Ppvernac.pr_vernac (mt ()) ocom in
+  let after = comment (Pputils.extract_comments (snd loc)) in
+  if !Flags.beautify_file then
+    (Pp.pp_with ft_beautify (hov 0 (before ++ com ++ after));
+     Format.pp_print_flush ft_beautify ())
+  else
+    Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)))
+
+(* load_vernac with beautify *)
+let beautify_pass ~doc ~comments ~ids ~filename =
+  let ft_beautify, close_beautify =
+    if !Flags.beautify_file then
+      let chan_beautify = open_out (filename^beautify_suffix) in
+      set_formatter_translator chan_beautify, fun () -> close_out chan_beautify;
+    else
+      !Topfmt.std_ft, fun () -> ()
+  in
+  (* The interface to the comment printer is imperative, so we first
+     set the comments, then we call print. This has to be done for
+     each file. *)
+  Pputils.beautify_comments := comments;
+  List.iter (fun id ->
+      Option.iter (fun (loc,ast) ->
+          pr_new_syntax ?loc ft_beautify (Some ast))
+        (Stm.get_ast ~doc id)) ids;
+
+  (* Is this called so comments at EOF are printed? *)
+  pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) ft_beautify None;
+  close_beautify ()
+
+(* Main driver for file loading. For now, we only do one beautify
+   pass. *)
+let load_vernac ~time ~echo ~check ~interactive ~state filename =
+  let ostate, ids, comments = load_vernac_core ~time ~echo ~check ~interactive ~state filename in
+  (* Pass for beautify *)
+  if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename;
+  (* End pass *)
+  ostate
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index e909ada1e..ca825197b 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -26,5 +26,5 @@ val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.l
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
     echo the commands if [echo] is set. Callers are expected to handle
     and print errors in form of exceptions. *)
-val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool ->
+val load_vernac : time:bool -> echo:bool -> check:bool -> interactive:bool ->
   state:State.t -> string -> State.t