[pp] Prepare for serialization, remove opaque glue.

We also remove flushing operations `msg_with`, now the flushing
responsibility belong to the owner of the formatter.

10 files changed, 83 insertions, 151 deletions

diff --git a/lib/feedback.ml b/lib/feedback.ml
index e723bf4ba..971a51e35 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -51,7 +51,9 @@ open Pp_control
 
 type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
 
-let msgnl_with ?pp_tag fmt strm = msg_with ?pp_tag fmt (strm ++ fnl ())
+let msgnl_with ?pp_tag fmt strm =
+  pp_with ?pp_tag fmt (strm ++ fnl ());
+  Format.pp_print_flush fmt ()
 
 (* XXX: This is really painful! *)
 module Emacs = struct
diff --git a/lib/pp.ml b/lib/pp.ml
index 9d2445d49..6d7bdf75e 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -6,44 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module Glue : sig
-
-  (** The [Glue] module implements a container data structure with
-      efficient concatenation. *)
-
-  type 'a t
-
-  val atom : 'a -> 'a t
-  val glue : 'a t -> 'a t -> 'a t
-  val empty : 'a t
-  val is_empty : 'a t -> bool
-  val iter : ('a -> unit) -> 'a t -> unit
-
-end = struct
-
-  type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t
-
-  let atom x = GLeaf x
-
-  let glue x y =
-    match x, y with
-    | GEmpty, _ -> y
-    | _, GEmpty -> x
-    | _, _ -> GNode (x,y)
-
-  let empty = GEmpty
-
-  let is_empty x = x = GEmpty
-
-  let rec iter f = function
-    | GEmpty -> ()
-    | GLeaf x -> f x
-    | GNode (x,y) -> iter f x; iter f y
-
-end
-
-type pp_tag = string list
-
 open Pp_control
 
 (* The different kinds of blocks are:
@@ -63,36 +25,22 @@ type block_type =
   | Pp_hvbox  of int
   | Pp_hovbox of int
 
-type ppcmd_token =
+type pp_tag = string list
+
+type std_ppcmds =
+  | Ppcmd_empty
   | Ppcmd_string of string
-  | Ppcmd_box of block_type * (ppcmd_token Glue.t)
+  | Ppcmd_glue of std_ppcmds * std_ppcmds
+  | Ppcmd_box  of block_type * std_ppcmds
   | Ppcmd_print_break of int * int
   | Ppcmd_white_space of int
   | Ppcmd_force_newline
-  | Ppcmd_print_if_broken
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
   | Ppcmd_comment of string list
   | Ppcmd_open_tag of pp_tag
   | Ppcmd_close_tag
 
-type 'a ppdir_token =
-  | Ppdir_ppcmds of ppcmd_token Glue.t
-  | Ppdir_print_newline
-  | Ppdir_print_flush
-
-type ppcmd = ppcmd_token
-
-type std_ppcmds = ppcmd Glue.t
-
-type 'a ppdirs = 'a ppdir_token Glue.t
-
-let (++) = Glue.glue
-
-let app = Glue.glue
-
-let is_empty g = Glue.is_empty g
-
 (* Compute length of an UTF-8 encoded string
    Rem 1 : utf8_length <= String.length (equal if pure ascii)
    Rem 2 : if used for an iso8859_1 encoded string, the result is
@@ -129,22 +77,30 @@ let utf8_length s =
   done ;
   !cnt
 
+let app s1 s2 = match s1, s2 with
+  | Ppcmd_empty, s
+  | s, Ppcmd_empty -> s
+  | s1, s2         -> Ppcmd_glue(s1, s2)
+
+let (++) = app
+
 (* formatting commands *)
-let str s = Glue.atom(Ppcmd_string s)
-let brk (a,b) = Glue.atom(Ppcmd_print_break (a,b))
-let fnl () = Glue.atom(Ppcmd_force_newline)
-let pifb () = Glue.atom(Ppcmd_print_if_broken)
-let ws n = Glue.atom(Ppcmd_white_space n)
-let comment l = Glue.atom(Ppcmd_comment l)
+let str s     = Ppcmd_string s
+let brk (a,b) = Ppcmd_print_break (a,b)
+let fnl  ()   = Ppcmd_force_newline
+let ws n      = Ppcmd_white_space n
+let comment l = Ppcmd_comment l
 
 (* derived commands *)
-let mt () = Glue.empty
-let spc () = Glue.atom(Ppcmd_print_break (1,0))
-let cut () = Glue.atom(Ppcmd_print_break (0,0))
-let align () = Glue.atom(Ppcmd_print_break (0,0))
-let int n = str (string_of_int n)
-let real r = str (string_of_float r)
-let bool b = str (string_of_bool b)
+let mt    () = Ppcmd_empty
+let spc   () = Ppcmd_print_break (1,0)
+let cut   () = Ppcmd_print_break (0,0)
+let align () = Ppcmd_print_break (0,0)
+let int   n  = str (string_of_int n)
+let real  r  = str (string_of_float r)
+let bool  b  = str (string_of_bool b)
+
+(* XXX: To Remove *)
 let strbrk s =
   let rec aux p n =
     if n < String.length s then
@@ -153,7 +109,7 @@ let strbrk s =
         else str (String.sub s p (n-p)) :: spc () :: aux (n+1) (n+1)
       else aux p (n + 1)
     else if p = n then [] else [str (String.sub s p (n-p))]
-  in List.fold_left (++) Glue.empty (aux 0 0)
+  in List.fold_left (++) Ppcmd_empty (aux 0 0)
 
 let pr_loc_pos loc =
   if Loc.is_ghost loc then (str"<unknown>")
@@ -174,26 +130,25 @@ let pr_loc loc =
 	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
 	   str":" ++ fnl())
 
-let ismt = is_empty
+let ismt = function | Ppcmd_empty -> true | _ -> false
 
 (* boxing commands *)
-let h n s = Glue.atom(Ppcmd_box(Pp_hbox n,s))
-let v n s = Glue.atom(Ppcmd_box(Pp_vbox n,s))
-let hv n s = Glue.atom(Ppcmd_box(Pp_hvbox n,s))
-let hov n s = Glue.atom(Ppcmd_box(Pp_hovbox n,s))
+let h   n s = Ppcmd_box(Pp_hbox n,s)
+let v   n s = Ppcmd_box(Pp_vbox n,s)
+let hv  n s = Ppcmd_box(Pp_hvbox n,s)
+let hov n s = Ppcmd_box(Pp_hovbox n,s)
 
 (* Opening and closing of boxes *)
-let hb n = Glue.atom(Ppcmd_open_box(Pp_hbox n))
-let vb n = Glue.atom(Ppcmd_open_box(Pp_vbox n))
-let hvb n = Glue.atom(Ppcmd_open_box(Pp_hvbox n))
-let hovb n = Glue.atom(Ppcmd_open_box(Pp_hovbox n))
-let close () = Glue.atom(Ppcmd_close_box)
+let hb   n   = Ppcmd_open_box(Pp_hbox n)
+let vb   n   = Ppcmd_open_box(Pp_vbox n)
+let hvb  n   = Ppcmd_open_box(Pp_hvbox n)
+let hovb n   = Ppcmd_open_box(Pp_hovbox n)
+let close () = Ppcmd_close_box
 
 (* Opening and closed of tags *)
-let open_tag t = Glue.atom(Ppcmd_open_tag t)
-let close_tag () = Glue.atom(Ppcmd_close_tag)
+let open_tag  t  = Ppcmd_open_tag t
+let close_tag () = Ppcmd_close_tag
 let tag t s = open_tag t ++ s ++ close_tag ()
-let eval_ppcmds l = l
 
 (* In new syntax only double quote char is escaped by repeating it *)
 let escape_string s =
@@ -223,27 +178,27 @@ let rec pr_com ft s =
 type tag_handler = pp_tag -> Format.tag
 
 (* pretty printing functions *)
-let pp_dirs ?pp_tag ft =
-  let pp_open_box = function
+let pp_with ?pp_tag ft =
+  let cpp_open_box = function
     | Pp_hbox n   -> Format.pp_open_hbox ft ()
     | Pp_vbox n   -> Format.pp_open_vbox ft n
     | Pp_hvbox n  -> Format.pp_open_hvbox ft n
     | Pp_hovbox n -> Format.pp_open_hovbox ft n
   in
-  let rec pp_cmd = function
-    | Ppcmd_string str         ->
-      let n = utf8_length str in
-      Format.pp_print_as ft n str
+  let rec pp_cmd = let open Format in function
+    | Ppcmd_empty             -> ()
+    | Ppcmd_glue(s1,s2)       -> pp_cmd s1; pp_cmd s2
+    | Ppcmd_string str        -> let n = utf8_length str in
+                                 pp_print_as ft n str
     | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
-        pp_open_box bty ;
-        if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss;
+        cpp_open_box bty ;
+        if not (Format.over_max_boxes ()) then pp_cmd ss;
         Format.pp_close_box ft ()
-    | Ppcmd_open_box bty      -> pp_open_box bty
-    | Ppcmd_close_box         -> Format.pp_close_box ft ()
-    | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
-    | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
-    | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
-    | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft ()
+    | Ppcmd_open_box bty      -> cpp_open_box bty
+    | Ppcmd_close_box         -> pp_close_box ft ()
+    | Ppcmd_white_space n     -> pp_print_break ft n 0
+    | Ppcmd_print_break(m,n)  -> pp_print_break ft m n
+    | Ppcmd_force_newline     -> pp_force_newline ft ()
     | Ppcmd_comment coms      -> List.iter (pr_com ft) coms
     | Ppcmd_open_tag tag ->
       begin match pp_tag with
@@ -256,34 +211,19 @@ let pp_dirs ?pp_tag ft =
       | Some _ -> Format.pp_close_tag ft ()
       end
   in
-  let pp_dir = function
-    | Ppdir_ppcmds cmdstream -> Glue.iter pp_cmd cmdstream
-    | Ppdir_print_newline    -> Format.pp_print_newline ft ()
-    | Ppdir_print_flush      -> Format.pp_print_flush ft ()
-  in
-  fun (dirstream : _ ppdirs) ->
-    try
-      Glue.iter pp_dir dirstream
-    with reraise ->
-      let reraise = Backtrace.add_backtrace reraise in
-      let () = Format.pp_print_flush ft () in
-      Exninfo.iraise reraise
-
-(* pretty printing functions WITHOUT FLUSH *)
-let pp_with ?pp_tag ft strm =
-  pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm))
-
-(* pretty printing functions WITH FLUSH *)
-let msg_with ?pp_tag ft strm =
-  pp_dirs ?pp_tag ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
+  try pp_cmd
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    let () = Format.pp_print_flush ft () in
+    Exninfo.iraise reraise
 
 (* If mixing some output and a goal display, please use msg_warning,
    so that interfaces (proofgeneral for example) can easily dispatch
    them to different windows. *)
 
 (** Output to a string formatter *)
-let string_of_ppcmds c =
-  Format.fprintf Format.str_formatter "@[%a@]" (msg_with ?pp_tag:None) c;
+let string_of_ppcmds ?pp_tag c =
+  Format.fprintf Format.str_formatter "@[%a@]" (pp_with ?pp_tag) c;
   Format.flush_str_formatter ()
 
 (* Copy paste from Util *)
@@ -310,7 +250,7 @@ let pr_nth n =
 
 (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
 
-let prlist pr l = List.fold_left (fun x e -> x ++ pr e) Glue.empty l
+let prlist pr l = List.fold_left (fun x e -> x ++ pr e) Ppcmd_empty l
 
 (* unlike all other functions below, [prlist] works lazily.
    if a strict behavior is needed, use [prlist_strict] instead.
diff --git a/lib/pp.mli b/lib/pp.mli
index 82accfff3..f61261a17 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -15,7 +15,6 @@ type std_ppcmds
 val str   : string -> std_ppcmds
 val brk   : int * int -> std_ppcmds
 val fnl   : unit -> std_ppcmds
-val pifb  : unit -> std_ppcmds
 val ws    : int -> std_ppcmds
 val mt    : unit -> std_ppcmds
 val ismt  : std_ppcmds -> bool
@@ -30,12 +29,6 @@ val app : std_ppcmds -> std_ppcmds -> std_ppcmds
 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
 (** Infix alias for [app]. *)
 
-val eval_ppcmds : std_ppcmds -> std_ppcmds
-(** Force computation. *)
-
-val is_empty : std_ppcmds -> bool
-(** Test emptyness. *)
-
 (** {6 Derived commands} *)
 
 val spc : unit -> std_ppcmds
@@ -73,10 +66,6 @@ val tag : pp_tag -> std_ppcmds -> std_ppcmds
 val open_tag : pp_tag -> std_ppcmds
 val close_tag : unit -> std_ppcmds
 
-(** {6 Utilities} *)
-
-val string_of_ppcmds : std_ppcmds -> string
-
 (** {6 Printing combinators} *)
 
 val pr_comma : unit -> std_ppcmds
@@ -145,13 +134,11 @@ val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 
 val pr_loc : Loc.t -> std_ppcmds
 
-(** {6 Low-level pretty-printing functions with and without flush} *)
+(** {6 Main renderers, to formatter and to string } *)
 
 (** FIXME: These ignore the logging settings and call [Format] directly *)
 type tag_handler = pp_tag -> Format.tag
 
-(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt]  *)
-val msg_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
-
-(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
-val pp_with  : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
+(** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
+val pp_with          : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
+val string_of_ppcmds : ?pp_tag:tag_handler -> std_ppcmds -> string
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index d89bf95ee..d8e382155 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/printing/printer.ml b/printing/printer.ml
index 00c2b636b..5e7e9ce54 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -722,7 +722,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
               (let s = Proof_global.Bullet.suggest p in
-               if Pp.is_empty s then s else fnl () ++ s) ++
+               if Pp.ismt s then s else fnl () ++ s) ++
               fnl ()
             in
 	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
diff --git a/printing/printmod.ml b/printing/printmod.ml
index ac7ff7697..521b4ec2a 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -405,11 +405,11 @@ let rec printable_body dir =
 
 let print_expression' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me
+    (fun e -> print_expression is_type env mp [] e) me
 
 let print_signature' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me
+    (fun e -> print_signature is_type env mp [] e) me
 
 let unsafe_print_module env mp with_body mb =
   let name = print_modpath [] mp in
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 5521e8a40..2cb608326 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -13,7 +13,9 @@ open Flags
 open Vernac
 open Pcoq
 
-let top_stderr x = msg_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x
+let top_stderr x =
+  pp_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x;
+  Format.pp_print_flush !Pp_control.err_ft ()
 
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cc1c44fe3..0ece0b014 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -595,7 +595,7 @@ let parse_args arglist =
     parse ()
   with
     | UserError(_, s) as e ->
-      if is_empty s then exit 1
+      if ismt s then exit 1
       else fatal_error (CErrors.print e) false
     | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index de7bc6929..5d17054fc 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -143,7 +143,8 @@ let pr_new_syntax_in_context loc chan_beautify ocom =
       | None -> mt() in
     let after = comment (CLexer.extract_comments (snd loc)) in
     if !beautify_file then
-      Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
+      (Pp.pp_with !Pp_control.std_ft (hov 0 (before ++ com ++ after));
+       Format.pp_print_flush !Pp_control.std_ft ())
     else
       Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
     States.unfreeze fs;
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 148d029bc..5b91af03c 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -91,7 +91,7 @@ let process_vernac_interp_error with_header exn = match fst exn with
       let s = Lazy.force s in
       wrap_vernac_error with_header 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 ".")