Merge PR#390: Updates to the Pretty Printing Infrastructure

9 files changed, 379 insertions, 39 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 594f2e9449..6d71601cc5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -444,14 +444,14 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                with Not_found ->
 		 (* spiwack: the format of this error message should probably
 	                     be improved. *)
-		 let err_msg = string_of_ppcmds
+		 let err_msg =
 	                                (str "boolean->Leibniz:" ++
                                          str "You have to declare the" ++
 			   	         str "decidability over " ++
 				         Printer.pr_constr tt1 ++
 				         str " first.")
 		 in
-		 error err_msg
+		 user_err err_msg
                in let bl_args =
                         Array.append (Array.append
                           (Array.map (fun x -> x) v)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 17897460c0..f1e0c48f03 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -45,15 +45,9 @@ let _ = CErrors.register_handler explain_exn_default
 
 (** Pre-explain a vernac interpretation error *)
 
-let wrap_vernac_error with_header (exn, info) strm =
-  if with_header then
-    let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
-    let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
-    (e, info)
-  else
-    (EvaluatedError (strm, None), info)
+let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info)
 
-let process_vernac_interp_error with_header exn = match fst exn with
+let process_vernac_interp_error exn = match fst exn with
   | Univ.UniverseInconsistency i ->
     let msg =
       if !Constrextern.print_universes then
@@ -61,40 +55,40 @@ let process_vernac_interp_error with_header exn = match fst exn with
 	  Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
       else
 	mt() in
-    wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".")
+    wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te)
+      wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te)
+      wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te)
+      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
   | InductiveError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_inductive_error e)
+      wrap_vernac_error exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_module_error e)
+      wrap_vernac_error exn (Himsg.explain_module_error e)
   | Modintern.ModuleInternalizationError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e)
+      wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
   | RecursionSchemeError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e)
+      wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,sigma,e) ->
-      wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e)
+      wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e)
   | Tacred.ReductionTacticError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e)
+      wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_refiner_error e)
+      wrap_vernac_error exn (Himsg.explain_refiner_error e)
   | Nametab.GlobalizationError q ->
-      wrap_vernac_error with_header exn
+      wrap_vernac_error exn
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 	 spc () ++ str "was not found" ++
 	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
   | Refiner.FailError (i,s) ->
       let s = Lazy.force s in
-      wrap_vernac_error with_header exn
+      wrap_vernac_error exn
 	(str "Tactic failure" ++
-         (if Pp.is_empty s then s else str ": " ++ s) ++
+         (if Pp.ismt s then s else str ": " ++ s) ++
          if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
-      wrap_vernac_error with_header exn (msg ++ str ".")
+      wrap_vernac_error exn (msg ++ str ".")
   | _ ->
       exn
 
@@ -108,9 +102,9 @@ let additional_error_info = ref []
 let register_additional_error_info f =
   additional_error_info := f :: !additional_error_info
 
-let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) =
+let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
-  let e = process_vernac_interp_error with_header (exc, info) in
+  let e = process_vernac_interp_error (exc, info) in
   let () =
     if not allow_uncaught && not (CErrors.handled (fst e)) then
       let (e, info) = e in
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index a67c887af3..370ad7e3b5 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -11,7 +11,7 @@ exception EvaluatedError of Pp.std_ppcmds * exn option
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/vernac/search.ml b/vernac/search.ml
index e1b56b1319..540573843e 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -367,7 +367,7 @@ let interface_search =
     let answer = {
       coq_object_prefix = prefix;
       coq_object_qualid = qualid;
-      coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr);
+      coq_object_object = constr;
     } in
     ans := answer :: !ans;
   in
diff --git a/vernac/search.mli b/vernac/search.mli
index c9167c485d..82b79f75de 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -67,7 +67,7 @@ type 'a coq_object = {
 }
 
 val interface_search : ?glnum:int -> (search_constraint * bool) list ->
-  string coq_object list
+  constr coq_object list
 
 (** {6 Generic search function} *)
 
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
new file mode 100644
index 0000000000..f843484f7e
--- /dev/null
+++ b/vernac/topfmt.ml
@@ -0,0 +1,289 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Feedback
+open Pp
+
+(** Pp control also belongs here as the terminal is private to the toplevel *)
+
+type pp_global_params = {
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+(* Default parameters of pretty-printing *)
+
+let dflt_gp = {
+  margin     = 78;
+  max_indent = 50;
+  max_depth  = 50;
+  ellipsis   = "..." }
+
+(* A deeper pretty-printer to print proof scripts *)
+
+let deep_gp = {
+  margin     = 78;
+  max_indent = 50;
+  max_depth  = 10000;
+  ellipsis   = "..." }
+
+(* set_gp : Format.formatter -> pp_global_params -> unit
+ * set the parameters of a formatter *)
+
+let set_gp ft gp =
+  Format.pp_set_margin ft gp.margin ;
+  Format.pp_set_max_indent ft gp.max_indent ;
+  Format.pp_set_max_boxes ft gp.max_depth ;
+  Format.pp_set_ellipsis_text ft gp.ellipsis
+
+let set_dflt_gp ft = set_gp ft dflt_gp
+
+let get_gp ft =
+  { margin = Format.pp_get_margin ft ();
+    max_indent = Format.pp_get_max_indent ft ();
+    max_depth = Format.pp_get_max_boxes ft ();
+    ellipsis = Format.pp_get_ellipsis_text ft () }
+
+(* with_fp : 'a pp_formatter_params -> Format.formatter
+ * returns of formatter for given formatter functions *)
+
+let with_fp chan out_function flush_function =
+  let ft = Format.make_formatter out_function flush_function in
+  Format.pp_set_formatter_out_channel ft chan;
+  ft
+
+(* Output on a channel ch *)
+
+let with_output_to ch =
+  let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in
+  set_gp ft deep_gp;
+  ft
+
+let std_ft = ref Format.std_formatter
+let _ = set_dflt_gp !std_ft
+
+let err_ft = ref Format.err_formatter
+let _ = set_gp !err_ft deep_gp
+
+let deep_ft = ref (with_output_to stdout)
+let _ = set_gp !deep_ft deep_gp
+
+(* For parametrization through vernacular *)
+let default = Format.pp_get_max_boxes !std_ft ()
+let default_margin = Format.pp_get_margin !std_ft ()
+
+let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ())
+let set_depth_boxes v =
+  Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v)
+
+let get_margin () = Some (Format.pp_get_margin !std_ft ())
+let set_margin v =
+  let v = match v with None -> default_margin | Some v -> v in
+  Format.pp_set_margin Format.str_formatter v;
+  Format.pp_set_margin !std_ft v;
+  Format.pp_set_margin !deep_ft v;
+  (* Heuristic, based on usage: the column on the right of max_indent
+     column is 20% of width, capped to 30 characters *)
+  let m = max (64 * v / 100) (v-30) in
+  Format.pp_set_max_indent Format.str_formatter m;
+  Format.pp_set_max_indent !std_ft m;
+  Format.pp_set_max_indent !deep_ft m
+
+(** Console display of feedback *)
+
+(** Default tags *)
+module Tag = struct
+
+  let error   = "message.error"
+  let warning = "message.warning"
+  let debug   = "message.debug"
+
+end
+
+type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
+
+let msgnl_with fmt strm =
+  pp_with fmt (strm ++ fnl ());
+  Format.pp_print_flush fmt ()
+
+(* XXX: This is really painful! *)
+module Emacs = struct
+
+  (* Special chars for emacs, to detect warnings inside goal output *)
+  let emacs_quote_start = String.make 1 (Char.chr 254)
+  let emacs_quote_end   = String.make 1 (Char.chr 255)
+
+  let emacs_quote_err g =
+    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+
+  let emacs_quote_info_start = "<infomsg>"
+  let emacs_quote_info_end = "</infomsg>"
+
+  let emacs_quote_info g =
+    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+
+end
+
+open Emacs
+
+let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
+let info_hdr = mt ()
+let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
+let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
+
+let make_body quoter info ?loc s =
+  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
+  quoter (hov 0 (loc ++ info ++ s))
+
+(* Generic logger *)
+let gen_logger dbg err ?loc level msg = match level with
+  | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_hdr ?loc msg)
+  | Info    -> msgnl_with !std_ft (make_body dbg info_hdr ?loc msg)
+  (* XXX: What to do with loc here? *)
+  | Notice  -> msgnl_with !std_ft msg
+  | Warning -> Flags.if_warn (fun () ->
+               msgnl_with !err_ft (make_body err warn_hdr ?loc msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_hdr ?loc msg)
+
+(** Standard loggers *)
+
+(* We provide a generic clear_log_backend callback for backends
+   wanting to do clenaup after the print.
+*)
+let std_logger_cleanup = ref (fun () -> ())
+
+let std_logger ?loc level msg =
+  gen_logger (fun x -> x) (fun x -> x) ?loc level msg;
+  !std_logger_cleanup ()
+
+(** Color logging. Moved from Ppstyle, it may need some more refactoring  *)
+
+(* Tag map for terminal style *)
+let default_tag_map () = let open Terminal in [
+  (* Local to console toplevel *)
+    "message.error"    , make ~bold:true ~fg_color:`WHITE ~bg_color:`RED ()
+  ; "message.warning"  , make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW ()
+  ; "message.debug"    , make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA ()
+  (* Coming from the printer *)
+  ; "constr.evar"      , make            ~fg_color:`LIGHT_BLUE ()
+  ; "constr.keyword"   , make ~bold:true ()
+  ; "constr.type"      , make ~bold:true ~fg_color:`YELLOW ()
+  ; "constr.notation"  , make ~fg_color:`WHITE ()
+  (* ["constr"; "variable"] is not assigned *)
+  ; "constr.reference" , make ~fg_color:`LIGHT_GREEN ()
+  ; "constr.path"      , make ~fg_color:`LIGHT_MAGENTA ()
+  ; "module.definition", make ~bold:true ~fg_color:`LIGHT_RED ()
+  ; "module.keyword"   , make ~bold:true ()
+  ; "tactic.keyword"   , make ~bold:true ()
+  ; "tactic.primitive" , make ~fg_color:`LIGHT_GREEN ()
+  ; "tactic.string"    , make ~fg_color:`LIGHT_RED ()
+  ]
+
+let tag_map = ref CString.Map.empty
+
+let init_tag_map styles =
+  let set accu (name, st) = CString.Map.add name st accu in
+  tag_map := List.fold_left set !tag_map styles
+
+let clear_styles () =
+  tag_map := CString.Map.empty
+
+let parse_color_config file =
+  let styles = Terminal.parse file in
+  init_tag_map styles
+
+let dump_tags () = CString.Map.bindings !tag_map
+
+(** Not thread-safe. We should put a lock somewhere if we print from
+    different threads. Do we? *)
+let make_style_stack () =
+  (** Default tag is to reset everything *)
+  let empty = Terminal.make () in
+  let default_tag = Terminal.({
+      fg_color = Some `DEFAULT;
+      bg_color = Some `DEFAULT;
+      bold = Some false;
+      italic = Some false;
+      underline = Some false;
+      negative = Some false;
+    })
+  in
+  let style_stack = ref [] in
+  let peek () = match !style_stack with
+  | []      -> default_tag  (** Anomalous case, but for robustness *)
+  | st :: _ -> st
+  in
+  let push tag =
+    let style =
+      try CString.Map.find tag !tag_map
+      with | Not_found -> empty
+    in
+    (** Use the merging of the latest tag and the one being currently pushed.
+    This may be useful if for instance the latest tag changes the background and
+    the current one the foreground, so that the two effects are additioned. *)
+    let style = Terminal.merge (peek ()) style in
+    style_stack := style :: !style_stack;
+    Terminal.eval style
+  in
+  let pop _ = match !style_stack with
+  | []       -> (** Something went wrong, we fallback *)
+                Terminal.eval default_tag
+  | _ :: rem -> style_stack := rem;
+                Terminal.eval (peek ())
+  in
+  let clear () = style_stack := [] in
+  push, pop, clear
+
+let init_color_output () =
+  init_tag_map (default_tag_map ());
+  let push_tag, pop_tag, clear_tag = make_style_stack () in
+  std_logger_cleanup := clear_tag;
+  let tag_handler = {
+    Format.mark_open_tag   = push_tag;
+    Format.mark_close_tag  = pop_tag;
+    Format.print_open_tag  = ignore;
+    Format.print_close_tag = ignore;
+  } in
+  Format.pp_set_mark_tags !std_ft true;
+  Format.pp_set_mark_tags !err_ft true;
+  Format.pp_set_formatter_tag_functions !std_ft tag_handler;
+  Format.pp_set_formatter_tag_functions !err_ft tag_handler
+
+(* Rules for emacs:
+   - Debug/info: emacs_quote_info
+   - Warning/Error: emacs_quote_err
+   - Notice: unquoted
+ *)
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+
+(* Output to file, used only in extraction so a candidate for removal *)
+let ft_logger old_logger ft ?loc level mesg =
+  let id x = x in
+  match level with
+  | Debug   -> msgnl_with ft (make_body id  dbg_hdr mesg)
+  | Info    -> msgnl_with ft (make_body id info_hdr mesg)
+  | Notice  -> msgnl_with ft mesg
+  | Warning -> old_logger ?loc level mesg
+  | Error   -> old_logger ?loc level mesg
+
+let with_output_to_file fname func input =
+  (* XXX FIXME: redirect std_ft  *)
+  (* let old_logger = !logger in *)
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *)
+  try
+    let output = func input in
+    (* logger := old_logger; *)
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    (* logger := old_logger; *)
+    close_out channel;
+    Exninfo.iraise reraise
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
new file mode 100644
index 0000000000..1555f80a9f
--- /dev/null
+++ b/vernac/topfmt.mli
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Console printing options *)
+
+type pp_global_params = {
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+val dflt_gp : pp_global_params
+val deep_gp : pp_global_params
+val set_gp : Format.formatter -> pp_global_params -> unit
+val set_dflt_gp : Format.formatter -> unit
+val get_gp : Format.formatter -> pp_global_params
+
+(** {6 Output functions of pretty-printing. } *)
+
+val with_output_to : out_channel -> Format.formatter
+
+val std_ft  : Format.formatter ref
+val err_ft  : Format.formatter ref
+val deep_ft : Format.formatter ref
+
+(** {6 For parametrization through vernacular. } *)
+
+val set_depth_boxes : int option -> unit
+val get_depth_boxes : unit -> int option
+
+val set_margin : int option -> unit
+val get_margin : unit -> int option
+
+(** Headers for tagging *)
+val err_hdr : Pp.std_ppcmds
+
+(** Console display of feedback *)
+val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+
+val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+
+val init_color_output : unit -> unit
+val clear_styles : unit -> unit
+val parse_color_config : string -> unit
+val dump_tags : unit -> (string * Terminal.style) list
+
+(** [with_output_to_file file f x] executes [f x] with logging
+    redirected to a file [file] *)
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 94ef54f70f..283c095eb6 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -14,4 +14,5 @@ Record
 Assumptions
 Vernacinterp
 Mltop
+Topfmt
 Vernacentries
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3afe04b37b..32e18a0149 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -39,8 +39,9 @@ module NamedDecl = Context.Named.Declaration
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
 let debug = false
-let prerr_endline x =
-  if debug then prerr_endline (x ()) else ()
+(* XXX Should move to a common library *)
+let vernac_pperr_endline pp =
+  if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
 
 (* Misc *)
 
@@ -1448,8 +1449,8 @@ let _ =
       optdepr  = false;
       optname  = "the printing depth";
       optkey   = ["Printing";"Depth"];
-      optread  = Pp_control.get_depth_boxes;
-      optwrite = Pp_control.set_depth_boxes }
+      optread  = Topfmt.get_depth_boxes;
+      optwrite = Topfmt.set_depth_boxes }
 
 let _ =
   declare_int_option
@@ -1457,8 +1458,8 @@ let _ =
       optdepr  = false;
       optname  = "the printing width";
       optkey   = ["Printing";"Width"];
-      optread  = Pp_control.get_margin;
-      optwrite = Pp_control.set_margin }
+      optread  = Topfmt.get_margin;
+      optwrite = Topfmt.set_margin }
 
 let _ =
   declare_bool_option
@@ -1933,7 +1934,7 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~loc locality poly c =
-  prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
   match c with
   (* The below vernac are candidates for removal from the main type
      and to be put into a new doc_command datatype: *)
@@ -2193,7 +2194,7 @@ let with_fail b f =
            | e ->
               let e = CErrors.push e in
               raise (HasFailed (CErrors.iprint
-                (ExplainErr.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e))))
+                (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))))
         ()
     with e when CErrors.noncritical e ->
       let (e, _) = CErrors.push e in
@@ -2226,7 +2227,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
     | VernacRedirect (s, (_,v)) ->
-         Feedback.with_output_to_file s (aux false) v
+         Topfmt.with_output_to_file s (aux false) v
     | VernacTime (_,v) ->
         System.with_time !Flags.time
           (aux ?locality ?polymorphism isprogcmd) v;