From 338608a73bc059670eb8196788c45a37419a3e4d Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 13 Sep 2012 13:12:40 +0000 Subject: Made Pp.std_ppcmds opaque. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/checker.ml | 9 +++------ grammar/tacextend.ml4 | 2 +- grammar/vernacextend.ml4 | 2 +- lib/pp.ml | 13 +++++++++++-- lib/pp.mli | 18 +++++++++++------- plugins/xml/dumptree.ml4 | 4 +--- toplevel/coqtop.ml | 9 +++------ 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 '"' """ (escape '<' "<" (escape '&' "&" (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 = -- cgit v1.2.3