# HG changeset patch # User wenzelm # Date 1745527504 -7200 # Node ID abd3885a3fcffbe45b2138d2f0a638cb103f54c9 # Parent bcee022fbe3063d8338e633def89647b156a8b2a more scalable; diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/General/pretty.ML --- 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 = diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/PIDE/markup.ML --- 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 "" = "" diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/PIDE/query_operation.ML --- 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 ()); diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/Tools/find_consts.ML --- 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; diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/Tools/find_theorems.ML --- 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; diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/Tools/print_operation.ML --- 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;