aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/reduction.ml6
-rw-r--r--engine/universes.ml7
-rw-r--r--ide/ide_slave.ml2
-rw-r--r--stm/stm.ml20
-rw-r--r--tools/fake_ide.ml4
-rw-r--r--vernac/search.ml2
-rw-r--r--vernac/search.mli2
-rw-r--r--vernac/vernacentries.ml7
8 files changed, 27 insertions, 23 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ec16aa261..28c0126b4 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -176,9 +176,9 @@ let sort_cmp env univ pb s0 s1 =
then begin
if !Flags.debug then begin
let op = match pb with CONV -> "=" | CUMUL -> "<=" in
- Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
- (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
- ++ Univ.pr_universes univ))
+ Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+ str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+ ++ Univ.pr_universes univ)
end;
raise NotConvertible
end
diff --git a/engine/universes.ml b/engine/universes.ml
index 6720fcef8..30a9ef163 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -416,10 +416,9 @@ let constr_of_global gr =
(* Should be an error as we might forget constraints, allow for now
to make firstorder work with "using" clauses *)
c
- else raise (Invalid_argument
- ("constr_of_global: globalization of polymorphic reference " ^
- Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^
- " would forget universes."))
+ else CErrors.user_err ~hdr:"constr_of_global"
+ Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
+ str " would forget universes.")
else c
let constr_of_reference = constr_of_global
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index e3e1a8890..2065a4546 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -255,7 +255,7 @@ let status force =
let export_coq_object t = {
Interface.coq_object_prefix = t.Search.coq_object_prefix;
Interface.coq_object_qualid = t.Search.coq_object_qualid;
- Interface.coq_object_object = t.Search.coq_object_object
+ Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
}
let pattern_of_string ?env s =
diff --git a/stm/stm.ml b/stm/stm.ml
index ee142b293..b9dbb7891 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -6,11 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr
let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else ()
let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
+let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else ()
+
open Vernacexpr
open CErrors
open Pp
@@ -994,11 +997,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
in
let aux_interp cmd =
if is_filtered_command cmd then
- stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
+ stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr)
else match cmd with
| VernacShow ShowScript -> ShowScript.show_script ()
| expr ->
- stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
+ stm_pperr_endline Pp.(fun () -> str "interpreting " ++ pr_vernac expr);
try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
with e ->
let e = CErrors.push e in
@@ -1431,11 +1434,10 @@ end = struct (* {{{ *)
| Some (safe, err) -> err, safe
| None -> Stateid.dummy, Stateid.dummy in
let e_msg = iprint (e, info) in
- stm_prerr_endline (fun () -> "failed with the following exception:");
- stm_prerr_endline (fun () -> string_of_ppcmds e_msg);
+ stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg);
let e_safe_states = List.filter State.is_cached_and_valid my_states in
RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
-
+
let perform_states query =
if query = [] then [] else
let is_tac e = match classify_vernac e with
@@ -1880,10 +1882,10 @@ end = struct (* {{{ *)
let open Notations in
try
let pt, uc = Future.join f in
- stm_prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+ stm_pperr_endline (fun () -> hov 0 (
str"g=" ++ int (Evar.repr gid) ++ spc () ++
str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
- str"uc=" ++ Evd.pr_evar_universe_context uc)));
+ str"uc=" ++ Evd.pr_evar_universe_context uc));
(if abstract then Tactics.tclABSTRACT None else (fun x -> x))
(V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
Tactics.exact_no_check pt)
@@ -2514,7 +2516,7 @@ let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
let process_transaction ?(newtip=Stateid.fresh ()) ~tty
({ verbose; loc; expr } as x) c =
- stm_prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
+ stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
let vcs = VCS.backup () in
try
let head = VCS.current_branch () in
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 5dd2a9220..7a891239b 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -12,6 +12,8 @@ let error s =
prerr_endline ("fake_id: error: "^s);
exit 1
+let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
+
type coqtop = {
xml_printer : Xml_printer.t;
xml_parser : Xml_parser.t;
@@ -170,7 +172,7 @@ let print_document () =
Str.global_replace (Str.regexp "^[\n ]*") ""
(if String.length s > 20 then String.sub s 0 17 ^ "..."
else s) in
- prerr_endline (Pp.string_of_ppcmds
+ pperr_endline (
(Document.print doc
(fun b state_id { name; text } ->
Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
diff --git a/vernac/search.ml b/vernac/search.ml
index e1b56b131..540573843 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -367,7 +367,7 @@ let interface_search =
let answer = {
coq_object_prefix = prefix;
coq_object_qualid = qualid;
- coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr);
+ coq_object_object = constr;
} in
ans := answer :: !ans;
in
diff --git a/vernac/search.mli b/vernac/search.mli
index c9167c485..82b79f75d 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -67,7 +67,7 @@ type 'a coq_object = {
}
val interface_search : ?glnum:int -> (search_constraint * bool) list ->
- string coq_object list
+ constr coq_object list
(** {6 Generic search function} *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 999fe297e..32e18a014 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -39,8 +39,9 @@ module NamedDecl = Context.Named.Declaration
let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
let debug = false
-let vernac_prerr_endline x =
- if debug then prerr_endline (x ()) else ()
+(* XXX Should move to a common library *)
+let vernac_pperr_endline pp =
+ if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
(* Misc *)
@@ -1933,7 +1934,7 @@ let vernac_load interp fname =
* still parsed as the obsolete_locality grammar entry for retrocompatibility.
* loc is the Loc.t of the vernacular command being interpreted. *)
let interp ?proof ~loc locality poly c =
- vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
+ vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
match c with
(* The below vernac are candidates for removal from the main type
and to be put into a new doc_command datatype: *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 05:27:48 +0000