diff options
| -rw-r--r-- | lib/pp.ml4 | 4 | ||||
| -rw-r--r-- | lib/pp.mli | 2 | ||||
| -rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 7 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 5 | ||||
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 10 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 4 |
6 files changed, 13 insertions, 19 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 854e4b49c..c602b403e 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -332,3 +332,7 @@ let msgnl x = msgnl_with !std_ft x let msgerr x = msg_with !err_ft x let msgerrnl x = msgnl_with !err_ft x let msg_warning x = msg_warning_with !err_ft x + +let string_of_ppcmds c = + msg_with Format.str_formatter c; + Format.flush_str_formatter () diff --git a/lib/pp.mli b/lib/pp.mli index 44732c7ef..7070e3f5f 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -112,3 +112,5 @@ val msgnl : std_ppcmds -> unit val msgerr : std_ppcmds -> unit val msgerrnl : std_ppcmds -> unit val msg_warning : std_ppcmds -> unit + +val string_of_ppcmds : std_ppcmds -> string diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index c948ef58b..b0e4fcc69 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -14,11 +14,6 @@ let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";; -let std_ppcmds_to_string s = - Pp.msg_with Format.str_formatter s; - Format.flush_str_formatter () -;; - let idref_of_id id = "v" ^ id;; (* Transform a constr to an Xml.token Stream.t *) @@ -156,7 +151,7 @@ Pp.ppnl (Pp.(++) (Pp.str | _ -> (****** la tactique employee *) let prtac = Pptactic.pr_tactic (Global.env()) in - let tac = std_ppcmds_to_string (prtac tactic_expr) in + let tac = Pp.string_of_ppcmds (prtac tactic_expr) in let tacname= first_word tac in let of_attribute = ("name",tacname)::("script",tac)::of_attribute in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0f3fed704..99552c552 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -179,10 +179,9 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - pp_with Format.str_formatter + Util.error (Pp.string_of_ppcmds (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++ - str"Use \"Abort All\" first or complete proof(s).") ; - Util.error (Format.flush_str_formatter ()) + str"Use \"Abort All\" first or complete proof(s).")) end diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 83b63067e..f4dab15f0 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -346,13 +346,12 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = msg_with Format.str_formatter + let err_msg = string_of_ppcmds (str "Leibniz->boolean:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr type_of_pq ++ - str " first."); - Format.flush_str_formatter () + str " first.") in error err_msg in let lb_args = Array.append (Array.append @@ -404,13 +403,12 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = msg_with Format.str_formatter + let err_msg = string_of_ppcmds (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ Printer.pr_constr tt1 ++ - str " first."); - Format.flush_str_formatter () + str " first.") in error err_msg in let bl_args = diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index cbd7d4353..5309a4505 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -352,10 +352,6 @@ let rewind count = (** Goal display *) -let string_of_ppcmds c = - Pp.msg_with Format.str_formatter c; - Format.flush_str_formatter () - let hyp_next_tac sigma env (id,_,ast) = let id_s = Names.string_of_id id in let type_s = string_of_ppcmds (pr_ltype_env env ast) in |