Merge PR #6736: [toplevel] Move beautify to its own pass.

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 dedad1990..da1fe6d3d 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 deb2c2038..5afc4e182 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -90,10 +90,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
@@ -192,7 +192,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
@@ -230,7 +230,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 ();
@@ -271,7 +271,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
@@ -286,17 +286,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