Made Pp.std_ppcmds opaque.

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

7 files changed, 31 insertions, 26 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index fd13cc195..f43a03f4a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -342,12 +342,9 @@ let parse_args argv =
   try
     parse (List.tl (Array.to_list argv))
   with
-    | UserError(_,s) as e -> begin
-	try
-	  Stream.empty s; exit 1
-	with Stream.Failure ->
-	  fatal_error (explain_exn e)
-      end
+    | UserError(_, s) as e ->
+      if Pp.is_empty s then exit 1
+      else fatal_error (explain_exn e)
     | e -> begin fatal_error (explain_exn e) end
 
 
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index c3d66642c..87425ef54 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -191,7 +191,7 @@ let declare_tactic loc s cl =
           $atomic_tactics$
       with e ->
 	Pp.msg_warning
-	  (Stream.iapp
+	  (Pp.app
 	     (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
 	     (Errors.print e));
       Egramml.extend_tactic_grammar $se$ $gl$;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index d6b023fd4..029755f08 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -58,7 +58,7 @@ let declare_command loc s nt cl =
 	try Vernacinterp.vinterp_add $se$ $funcl$
 	with e ->
 	  Pp.msg_warning
-	    (Stream.iapp
+	    (Pp.app
 	       (Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
 	       (Errors.print e));
 	Egramml.extend_vernac_command_grammar $se$ $nt$ $gl$
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} *)
 
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 3f8f18d4a..4fc1fc2b7 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -26,9 +26,7 @@ open Names;;
 
 exception Different
 
-let xmlstream s =
-  (* In XML we want to print the whole stream so we can force the evaluation *)
-  Stream.of_list (List.map xmlescape (Stream.npeek max_int s))
+let xmlstream s = xmlescape s
 ;;
 
 let thin_sign osign sign =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a97d8748a..f06edd316 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -317,12 +317,9 @@ let parse_args arglist =
   try
     parse arglist
   with
-    | UserError(_,s) as e -> begin
-	try
-	  Stream.empty s; exit 1
-	with Stream.Failure ->
-	  fatal_error (Errors.print e)
-      end
+    | UserError(_, s) as e ->
+      if is_empty s then exit 1
+      else fatal_error (Errors.print e)
     | e -> fatal_error (Errors.print e)
 
 let init arglist =