--- a/src/Pure/General/pretty.ML Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/General/pretty.ML Thu Apr 24 22:45:04 2025 +0200
@@ -87,6 +87,7 @@
val output: output_ops -> T -> Bytes.T
val string_of_ops: output_ops -> T -> string
val string_of: T -> string
+ val strings_of: T -> string list
val pure_string_of: T -> string
val writeln: T -> unit
val writeln_urgent: T -> unit
@@ -527,6 +528,8 @@
fun string_of_ops ops = Bytes.content o output ops;
fun string_of prt = string_of_ops (output_ops NONE) prt;
+fun strings_of prt = Bytes.contents (output (output_ops NONE) prt);
+
val pure_string_of = string_of_ops (pure_output_ops NONE);
fun gen_writeln urgent prt =
--- a/src/Pure/PIDE/markup.ML Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/PIDE/markup.ML Thu Apr 24 22:45:04 2025 +0200
@@ -293,6 +293,7 @@
val no_output: output
val output: T -> output
val markup: T -> string -> string
+ val markup_strings: T -> string list -> string list
val markups: T list -> string -> string
val markup_report: string -> string
end;
@@ -898,6 +899,10 @@
fun markup m = output m |-> Library.enclose;
+fun markup_strings m =
+ let val (bg, en) = output m
+ in fn ss => [bg] @ ss @ [en] end;
+
val markups = fold_rev markup;
fun markup_report "" = ""
--- a/src/Pure/PIDE/query_operation.ML Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/PIDE/query_operation.ML Thu Apr 24 22:45:04 2025 +0200
@@ -9,7 +9,9 @@
sig
val register: {name: string, pri: int} ->
({state: Toplevel.state, args: string list,
- output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit
+ output_result: string list -> unit,
+ writelns_result: string list -> unit,
+ writeln_result: string -> unit} -> unit) -> unit
end;
structure Query_Operation: QUERY_OPERATION =
@@ -21,16 +23,17 @@
SOME {delay = NONE, pri = pri, persistent = false, strict = false,
print_fn = fn _ => Thread_Attributes.uninterruptible (fn run => fn state =>
let
- fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
- fun status m = output_result (YXML.output_markup_only m);
- fun writeln_result s = output_result (Markup.markup Markup.writeln s);
+ fun output_result ss = Output.result [(Markup.instanceN, instance)] ss;
+ fun status m = output_result [YXML.output_markup_only m];
+ fun writelns_result ss = output_result (Markup.markup_strings Markup.writeln ss);
+ val writeln_result = writelns_result o single;
fun toplevel_error exn =
- output_result (Markup.markup Markup.error (Runtime.exn_message exn));
+ output_result [Markup.markup Markup.error (Runtime.exn_message exn)];
val _ = status Markup.running;
fun main () =
f {state = state, args = args, output_result = output_result,
- writeln_result = writeln_result};
+ writelns_result = writelns_result, writeln_result = writeln_result};
val _ =
(case Exn.capture_body (*sic!*) (run main) of
Exn.Res () => ()
@@ -47,5 +50,10 @@
Query_Operation.register {name = "print_state", pri = Task_Queue.urgent_pri}
(fn {state = st, output_result, ...} =>
if Toplevel.is_proof st
- then output_result (Markup.markup Markup.state (Toplevel.string_of_state st))
+ then
+ Toplevel.pretty_state st
+ |> Pretty.chunks
+ |> Pretty.strings_of
+ |> Markup.markup_strings Markup.state
+ |> output_result
else ());
--- a/src/Pure/Tools/find_consts.ML Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/Tools/find_consts.ML Thu Apr 24 22:45:04 2025 +0200
@@ -159,13 +159,13 @@
val _ =
Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
- (fn {state, args, writeln_result, ...} =>
+ (fn {state, args, writelns_result, ...} =>
(case try Toplevel.context_of state of
SOME ctxt =>
let
val [query_arg] = args;
val query = read_query Position.none query_arg;
- in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end
+ in writelns_result (Pretty.strings_of (pretty_consts ctxt query)) end
| NONE => error "Unknown context"));
end;
--- a/src/Pure/Tools/find_theorems.ML Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/Tools/find_theorems.ML Thu Apr 24 22:45:04 2025 +0200
@@ -536,7 +536,7 @@
val _ =
Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
- (fn {state = st, args, writeln_result, ...} =>
+ (fn {state = st, args, writelns_result, ...} =>
if can Toplevel.context_of st then
let
val [limit_arg, allow_dups_arg, query_arg] = args;
@@ -544,7 +544,7 @@
val opt_limit = Int.fromString limit_arg;
val rem_dups = allow_dups_arg = "false";
val criteria = read_query Position.none query_arg;
- in writeln_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
+ in writelns_result (Pretty.strings_of (pretty_theorems state opt_limit rem_dups criteria)) end
else error "Unknown context");
end;
--- a/src/Pure/Tools/print_operation.ML Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/Tools/print_operation.ML Thu Apr 24 22:45:04 2025 +0200
@@ -40,7 +40,7 @@
val _ =
Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
- (fn {state, args, writeln_result, ...} =>
+ (fn {state, args, writelns_result, ...} =>
let
val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
fun err s = Pretty.mark_str (Markup.bad (), s);
@@ -48,7 +48,7 @@
(case AList.lookup (op =) (Synchronized.value print_operations) name of
SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
| NONE => [err ("Unknown print operation: " ^ quote name)]);
- in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
+ in writelns_result (Pretty.strings_of (Pretty.chunks (maps print args))) end);
end;