Made Pp.std_ppcmds opaque.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 22 insertions, 9 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 983b6ea08..463e3fc3c 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -73,6 +73,9 @@ type std_ppcmds = ppcmd Stream.t
 
 type 'a ppdirs = 'a ppdir_token Stream.t
 
+let is_empty s =
+  try Stream.empty s; true with Stream.Failure -> false
+
 (* 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
@@ -158,6 +161,8 @@ let tclose () = Stream.of_list [Ppcmd_close_tbox]
 
 let (++) = Stream.iapp
 
+let app = Stream.iapp
+
 let rec eval_ppcmds l =
   let rec aux l =
     try
@@ -183,6 +188,9 @@ let qstring s = str ("\""^escape_string s^"\"")
 let qs = qstring
 let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
+let stream_map f s =
+  Stream.of_list (List.map f (Stream.npeek max_int s))
+
 let rec xmlescape ppcmd =
   let rec escape what withwhat (len, str) =
     try
@@ -199,10 +207,11 @@ let rec xmlescape ppcmd =
         Ppcmd_print (escape '"' "&quot;"
           (escape '<' "&lt;" (escape '&' "&amp;" (len, str))))
       (* In XML we always print whole content so we can npeek the whole stream *)
-    | Ppcmd_box (x, str) -> Ppcmd_box (x, Stream.of_list
-        (List.map xmlescape (Stream.npeek max_int str)))
+    | Ppcmd_box (x, str) ->
+      Ppcmd_box (x, stream_map xmlescape str)
     | x -> x
 
+let xmlescape = stream_map xmlescape
 
 (* This flag tells if the last printed comment ends with a newline, to
   avoid empty lines *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 6316ab410..614023758 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -16,9 +16,7 @@ val make_pp_nonemacs:unit -> unit
 
 (** Pretty-printers. *)
 
-type ppcmd
-
-type std_ppcmds = ppcmd Stream.t
+type std_ppcmds
 
 (** {6 Formatting commands} *)
 
@@ -36,13 +34,19 @@ val ismt : std_ppcmds -> bool
 val comment : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
 
-(** {6 Concatenation. } *)
+(** {6 Manipulation commands} *)
 
-val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
+val app : std_ppcmds -> std_ppcmds -> std_ppcmds
+(** Concatenation. *)
 
-(** {6 Evaluation} *)
+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} *)
 
@@ -57,7 +61,7 @@ val qs : string -> std_ppcmds
 val quote : std_ppcmds -> std_ppcmds
 val strbrk : string -> std_ppcmds
 
-val xmlescape : ppcmd -> ppcmd
+val xmlescape : std_ppcmds -> std_ppcmds
 
 (** {6 Boxing commands} *)