[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!

4 files changed, 82 insertions, 73 deletions

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