prefer static YXML.output_markup_only (without print_mode): Output.status is only relevant for PIDE (with print_mode "isabelle_process");
--- a/src/Pure/PIDE/command.ML Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/command.ML Mon Sep 09 19:40:18 2024 +0200
@@ -213,14 +213,14 @@
NONE => ()
| SOME 0 => ()
| SOME n =>
- let val report = Markup.markup_only (Markup.command_indent (n - 1));
+ let val report = YXML.output_markup_only (Markup.command_indent (n - 1));
in Toplevel.setmp_thread_position tr (fn () => Output.report [report]) () end)
else ()
end
| NONE => ());
fun status tr m =
- Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) ();
+ Toplevel.setmp_thread_position tr (fn () => Output.status [YXML.output_markup_only m]) ();
fun eval_state keywords span tr ({state, ...}: eval_state) =
let
--- a/src/Pure/PIDE/document.ML Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/document.ML Mon Sep 09 19:40:18 2024 +0200
@@ -635,7 +635,7 @@
val _ = List.app (fn (thy, r) => Context_Position.reports_global thy [r]) parents_reports;
val thy = Resources.begin_theory master_dir header parents;
- val _ = Output.status [Markup.markup_only Markup.initialized];
+ val _ = Output.status [YXML.output_markup_only Markup.initialized];
in thy end;
fun get_special_parent node =
@@ -785,10 +785,10 @@
val consolidate =
Command.print0 {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ =>
let
- val _ = Output.status [Markup.markup_only Markup.consolidating];
+ val _ = Output.status [YXML.output_markup_only Markup.consolidating];
val result = Exn.capture (Thy_Info.apply_presentation context) thy;
val _ = Lazy.force (get_consolidated node);
- val _ = Output.status [Markup.markup_only Markup.consolidated];
+ val _ = Output.status [YXML.output_markup_only Markup.consolidated];
in Exn.release result end};
val result_entry =
(case lookup_entry node id of
--- a/src/Pure/PIDE/execution.ML Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/execution.ML Mon Sep 09 19:40:18 2024 +0200
@@ -141,7 +141,7 @@
val props =
if ! Multithreading.trace >= 2
then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
- in Output.status (map (Markup.markup_only o Markup.properties props) markups) end;
+ in Output.status (map (YXML.output_markup_only o Markup.properties props) markups) end;
type params = {name: string, pos: Position.T, pri: int};
--- a/src/Pure/PIDE/markup.ML Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/markup.ML Mon Sep 09 19:40:18 2024 +0200
@@ -285,7 +285,6 @@
val enclose: T -> Output.output -> Output.output
val markup: T -> string -> string
val markups: T list -> string -> string
- val markup_only: T -> string
val markup_report: string -> string
end;
@@ -874,8 +873,6 @@
val markups = fold_rev markup;
-fun markup_only m = markup m "";
-
fun markup_report "" = ""
| markup_report txt = markup report txt;
--- a/src/Pure/PIDE/query_operation.ML Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/query_operation.ML Mon Sep 09 19:40:18 2024 +0200
@@ -22,7 +22,7 @@
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 (Markup.markup_only m);
+ fun status m = output_result (YXML.output_markup_only m);
fun writeln_result s = output_result (Markup.markup Markup.writeln s);
fun toplevel_error exn =
output_result (Markup.markup Markup.error (Runtime.exn_message exn));
--- a/src/Pure/PIDE/yxml.ML Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML Mon Sep 09 19:40:18 2024 +0200
@@ -28,6 +28,7 @@
val bytes_of: XML.tree -> Bytes.T
val write_body: Path.T -> XML.body -> unit
val output_markup: Markup.T -> string * string
+ val output_markup_only: Markup.T -> string
val output_markup_elem: Markup.T -> (string * string) * string
val markup_ops: Markup.ops
val parse_body: string -> XML.body
@@ -95,6 +96,8 @@
if Markup.is_empty markup then Markup.no_output
else (XY ^ name ^ implode (map (fn p => Y ^ Properties.print_eq p) atts) ^ X, XYX);
+val output_markup_only = op ^ o output_markup;
+
fun output_markup_elem markup =
let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
in ((bg1, bg2), en) end;