Merge PR#390: Updates to the Pretty Printing Infrastructure

7 files changed, 99 insertions, 173 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0a591e786f..fc8d5356c8 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -67,7 +67,9 @@ let pp_boxed_tuple f = function
     blocks is less that a line length. To avoid this awkward situation,
     we attach a big virtual size to [fnl] newlines. *)
 
-let fnl () = stras (1000000,"") ++ fnl ()
+(* EG: This looks quite suspicious... but beware of bugs *)
+(* let fnl () = stras (1000000,"") ++ fnl () *)
+let fnl () = fnl ()
 
 let fnl2 () = fnl () ++ fnl ()
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index e019bb3c2a..2b12462ad5 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -472,13 +472,14 @@ let formatter dry file =
     if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
     else
       match file with
-	| Some f -> Pp_control.with_output_to f
+	| Some f -> Topfmt.with_output_to f
 	| None -> Format.formatter_of_buffer buf
   in
+  (* XXX: Fixme, this shouldn't depend on Topfmt *)
   (* We never want to see ellipsis ... in extracted code *)
   Format.pp_set_max_boxes ft max_int;
   (* We reuse the width information given via "Set Printing Width" *)
-  (match Pp_control.get_margin () with
+  (match Topfmt.get_margin () with
     | None -> ()
     | Some i ->
       Format.pp_set_margin ft i;
@@ -518,8 +519,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
     set_phase Impl;
     pp_with ft (d.preamble mo comment opened unsafe_needs);
     pp_with ft (d.pp_struct struc);
+    Format.pp_print_flush ft ();
     Option.iter close_out cout;
   with reraise ->
+    Format.pp_print_flush ft ();
     Option.iter close_out cout; raise reraise
   end;
   if not dry then Option.iter info_file fn;
@@ -532,8 +535,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 set_phase Intf;
 	 pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
 	 pp_with ft (d.pp_sig (signature_of_structure struc));
+         Format.pp_print_flush ft ();
 	 close_out cout;
        with reraise ->
+         Format.pp_print_flush ft ();
 	 close_out cout; raise reraise
        end;
        info_file si)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index d89bf95ee8..d8e3821557 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -66,7 +66,7 @@ let pp_header_comment = function
   | None -> mt ()
   | Some com -> pp_comment com ++ fnl2 ()
 
-let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl ()
+let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl ()
 
 let pp_tdummy usf =
   if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt ()
@@ -618,7 +618,7 @@ and pp_module_type params = function
       push_visible mp params;
       let try_pp_specif l x =
         let px = pp_specif x in
-        if Pp.is_empty px then l else px::l
+        if Pp.ismt px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_specif *)
       let l = List.fold_left try_pp_specif [] sign in
@@ -696,7 +696,7 @@ and pp_module_expr params = function
       push_visible mp params;
       let try_pp_structure_elem l x =
         let px = pp_structure_elem x in
-        if Pp.is_empty px then l else px::l
+        if Pp.ismt px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_structure_elem *)
       let l = List.fold_left try_pp_structure_elem [] sel in
@@ -714,7 +714,7 @@ let rec prlist_sep_nonempty sep f = function
   | h::t ->
      let e = f h in
      let r = prlist_sep_nonempty sep f t in
-     if Pp.is_empty e then r
+     if Pp.ismt e then r
      else e ++ sep () ++ r
 
 let do_struct f s =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6f4ef37b44..dc418d530e 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -27,6 +27,26 @@ open Pputils
 open Ppconstr
 open Printer
 
+module Tag =
+struct
+
+  let keyword   = "tactic.keyword"
+  let primitive = "tactic.primitive"
+  let string    = "tactic.string"
+
+end
+
+let tag t s = Pp.tag t s
+let do_not_tag _ x = x
+let tag_keyword                 = tag Tag.keyword
+let tag_primitive               = tag Tag.primitive
+let tag_string                  = tag Tag.string
+let tag_glob_tactic_expr        = do_not_tag
+let tag_glob_atomic_tactic_expr = do_not_tag
+let tag_raw_tactic_expr         = do_not_tag
+let tag_raw_atomic_tactic_expr  = do_not_tag
+let tag_atomic_tactic_expr      = do_not_tag
+
 let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
 type 'a grammar_tactic_prod_item_expr =
@@ -64,30 +84,6 @@ type 'a extra_genarg_printer =
     (tolerability -> Val.t -> std_ppcmds) ->
     'a -> std_ppcmds
 
-module Make
-  (Ppconstr : Ppconstrsig.Pp)
-  (Taggers : sig
-      val tag_keyword
-        : std_ppcmds -> std_ppcmds
-      val tag_primitive
-        : std_ppcmds -> std_ppcmds
-      val tag_string
-        : std_ppcmds -> std_ppcmds
-      val tag_glob_tactic_expr
-        : glob_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_glob_atomic_tactic_expr
-        : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_raw_tactic_expr
-        : raw_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_raw_atomic_tactic_expr
-        : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_atomic_tactic_expr
-        : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
-  end)
-= struct
-
-  open Taggers
-
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
 
@@ -1206,37 +1202,6 @@ module Make
 
   let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
 
-end
-
-module Tag =
-struct
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["tactic"; "keyword"]
-
-  let primitive =
-    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
-    Ppstyle.make ~style ["tactic"; "primitive"]
-
-  let string =
-    let style = Terminal.make ~fg_color:`LIGHT_RED () in
-    Ppstyle.make ~style ["tactic"; "string"]
-
-end
-
-include Make (Ppconstr) (struct
-    let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
-    let do_not_tag _ x = x
-    let tag_keyword                 = tag Tag.keyword
-    let tag_primitive               = tag Tag.primitive
-    let tag_string                  = tag Tag.string
-    let tag_glob_tactic_expr        = do_not_tag
-    let tag_glob_atomic_tactic_expr = do_not_tag
-    let tag_raw_tactic_expr         = do_not_tag
-    let tag_raw_atomic_tactic_expr  = do_not_tag
-    let tag_atomic_tactic_expr      = do_not_tag
-end)
-
 let declare_extra_genarg_pprule wit
   (f : 'a raw_extra_genarg_printer)
   (g : 'b glob_extra_genarg_printer)
@@ -1338,22 +1303,3 @@ let () =
   let pr_unit _ _ _ () = str "()" in
   let printer _ _ prtac = prtac (0, E) in
   declare_extra_genarg_pprule wit_ltac printer printer pr_unit
-
-module Richpp = struct
-
-  include Make (Ppconstr.Richpp) (struct
-    open Ppannotation
-    open Genarg
-    let do_not_tag _ x = x
-    let tag e s = Pp.tag (Pp.Tag.inj e tag) s
-    let tag_keyword                   = tag AKeyword
-    let tag_primitive                 = tag AKeyword
-    let tag_string                    = do_not_tag ()
-    let tag_glob_tactic_expr        e = tag (AGlbGenArg (in_gen (glbwit wit_ltac) e))
-    let tag_glob_atomic_tactic_expr   = do_not_tag
-    let tag_raw_tactic_expr         e = tag (ARawGenArg (in_gen (rawwit wit_ltac) e))
-    let tag_raw_atomic_tactic_expr    = do_not_tag
-    let tag_atomic_tactic_expr        = do_not_tag
-  end)
-
-end
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 86e3ea5484..43e22dba3f 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -13,6 +13,8 @@ open Pp
 open Genarg
 open Geninterp
 open Names
+open Misctypes
+open Environ
 open Constrexpr
 open Tacexpr
 open Ppextend
@@ -54,14 +56,66 @@ type pp_tactic = {
 
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
-(** The default pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as raw strings. *)
-include Pptacticsig.Pp
+val pr_with_occurrences :
+  ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
+val pr_red_expr :
+  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+  ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
+val pr_may_eval :
+  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+  ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
+
+val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
+val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+
+val pr_in_clause :
+  ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+val pr_clauses :  bool option ->
+  ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+val pr_raw_extend: env -> int ->
+  ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+
+val pr_glob_extend: env -> int ->
+  ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
+
+val pr_extend :
+  (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+
+val pr_alias_key : Names.KerName.t -> std_ppcmds
+
+val pr_alias : (Val.t -> std_ppcmds) ->
+  int -> Names.KerName.t -> Val.t list -> std_ppcmds
+
+val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+
+val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
+
+val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
+
+val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
+
+val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
+
+val pr_hintbases : string list option -> std_ppcmds
+
+val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
+
+val pr_bindings :
+  ('constr -> std_ppcmds) ->
+  ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
+
+val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+  ('b, 'a) match_rule -> std_ppcmds
+
+val pr_value : tolerability -> Val.t -> std_ppcmds
 
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as annotated strings. The annotations can be
-    retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}. *)
-module Richpp : Pptacticsig.Pp
 
 val ltop : tolerability
diff --git a/plugins/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli
deleted file mode 100644
index 74ddd377ad..0000000000
--- a/plugins/ltac/pptacticsig.mli
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*  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 Pp
-open Genarg
-open Geninterp
-open Tacexpr
-open Ppextend
-open Environ
-open Misctypes
-
-module type Pp = sig
-
-  val pr_with_occurrences :
-    ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
-  val pr_red_expr :
-    ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
-    ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
-  val pr_may_eval :
-    ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-    ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
-
-  val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
-
-  val pr_in_clause :
-    ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-
-  val pr_clauses :  bool option ->
-    ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-
-  val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
-
-  val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
-
-  val pr_raw_extend: env -> int ->
-    ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
-
-  val pr_glob_extend: env -> int ->
-    ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
-
-  val pr_extend :
-    (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
-
-  val pr_alias_key : Names.KerName.t -> std_ppcmds
-
-  val pr_alias : (Val.t -> std_ppcmds) ->
-    int -> Names.KerName.t -> Val.t list -> std_ppcmds
-
-  val pr_alias_key : Names.KerName.t -> std_ppcmds
-
-  val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
-
-  val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
-
-  val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
-
-  val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
-
-  val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
-
-  val pr_hintbases : string list option -> std_ppcmds
-
-  val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
-
-  val pr_bindings :
-    ('constr -> std_ppcmds) ->
-    ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
-
-  val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
-
-  val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-    ('b, 'a) match_rule -> std_ppcmds
-
-  val pr_value : tolerability -> Val.t -> std_ppcmds
-
-end
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 8b92611136..1ad4d622b2 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -505,12 +505,12 @@ let pp_mapint map =
 		pp_form obj ++ str " => " ++
 				 pp_list (fun (i,f) -> pp_form f) l ++
 				 cut ()) ) map;
-    str "{ " ++ vb 0 ++  (!pp) ++ str " }" ++ close ()
+    str "{ " ++ hv 0 (!pp ++ str " }")
 
 let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2
 
 let pp_gl gl= cut () ++
-  str "{ " ++ vb 0 ++
+  str "{ " ++ hv 0 (
 	      begin
 		match gl.abs with
 		    None -> str ""
@@ -520,7 +520,7 @@ let pp_gl gl= cut () ++
   str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++
   str "arrows=" ++ pp_mapint gl.right ++ cut () ++
   str "cnx   =" ++ pp_list pp_connect gl.cnx ++ cut () ++
-  str "goal  =" ++ pp_form gl.gl ++ str " }" ++ close ()
+  str "goal  =" ++ pp_form gl.gl ++ str " }")
 
 let pp =
   function