# HG changeset patch
# User wenzelm
# Date 1742578625 -3600
# Node ID 83584916b6d7e42a24dddadba15b37486185e1e7
# Parent  6c68eff8355a9153b0b7df6695c41ca1456f028d
support for writeln_urgent, which is shown in Output before state messages (reminiscent of old Output.urgent_message before 521cea5fa777);

diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/General/output.ML	Fri Mar 21 18:37:05 2025 +0100
@@ -23,6 +23,8 @@
   exception Protocol_Message of Properties.T
   val protocol_message_undefined: protocol_message_fn
   val writelns: string list -> unit
+  val writelns_urgent: string list -> unit
+  val writeln_urgent: string -> unit
   val state: string -> unit
   val information: string -> unit
   val error_message': serial * string -> unit
@@ -39,6 +41,7 @@
 sig
   include OUTPUT
   val writeln_fn: (output list -> unit) Unsynchronized.ref
+  val writeln_urgent_fn: (output list -> unit) Unsynchronized.ref
   val state_fn: (output list -> unit) Unsynchronized.ref
   val information_fn: (output list -> unit) Unsynchronized.ref
   val tracing_fn: (output list -> unit) Unsynchronized.ref
@@ -61,6 +64,7 @@
 (* primitives -- provided via bootstrap environment *)
 
 val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn;
+val writeln_urgent_fn = Unsynchronized.ref Output_Primitives.writeln_urgent_fn;
 val state_fn = Unsynchronized.ref Output_Primitives.state_fn;
 val information_fn = Unsynchronized.ref Output_Primitives.information_fn;
 val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn;
@@ -94,6 +98,7 @@
 
 fun init_channels () =
  (writeln_fn := (physical_writeln o implode);
+  writeln_urgent_fn := (fn ss => ! writeln_fn ss);
   state_fn := (fn ss => ! writeln_fn ss);
   information_fn := Output_Primitives.ignore_outputs;
   tracing_fn := (fn ss => ! writeln_fn ss);
@@ -110,6 +115,8 @@
 
 fun writelns ss = ! writeln_fn ss;
 fun writeln s = writelns [s];
+fun writelns_urgent ss = ! writeln_urgent_fn ss;
+fun writeln_urgent s = writelns_urgent [s];
 fun state s = ! state_fn [s];
 fun information s = ! information_fn [s];
 fun tracing s = ! tracing_fn [s];
diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/General/output_primitives.ML
--- a/src/Pure/General/output_primitives.ML	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/General/output_primitives.ML	Fri Mar 21 18:37:05 2025 +0100
@@ -11,6 +11,7 @@
   type properties = (string * string) list
   val ignore_outputs: output list -> unit
   val writeln_fn: output list -> unit
+  val writeln_urgent_fn: output list -> unit
   val state_fn: output list -> unit
   val information_fn: output list -> unit
   val tracing_fn: output list -> unit
@@ -38,6 +39,7 @@
 fun ignore_outputs (_: output list) = ();
 
 val writeln_fn = ignore_outputs;
+val writeln_urgent_fn = ignore_outputs;
 val state_fn = ignore_outputs;
 val information_fn = ignore_outputs;
 val tracing_fn = ignore_outputs;
diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/General/output_primitives_virtual.ML
--- a/src/Pure/General/output_primitives_virtual.ML	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/General/output_primitives_virtual.ML	Fri Mar 21 18:37:05 2025 +0100
@@ -10,6 +10,7 @@
 open Output_Primitives;
 
 fun writeln_fn x = ! Private_Output.writeln_fn x;
+fun writeln_urgent_fn x = ! Private_Output.writeln_urgent_fn x;
 fun state_fn x = ! Private_Output.state_fn x;
 fun information_fn x = ! Private_Output.information_fn x;
 fun tracing_fn x = ! Private_Output.tracing_fn x;
diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/General/pretty.ML	Fri Mar 21 18:37:05 2025 +0100
@@ -89,6 +89,7 @@
   val string_of: T -> string
   val pure_string_of: T -> string
   val writeln: T -> unit
+  val writeln_urgent: T -> unit
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
   val chunks2: T list -> T
@@ -528,8 +529,12 @@
 
 val pure_string_of = string_of_ops (pure_output_ops NONE);
 
-fun writeln prt =
-  Output.writelns (Bytes.contents (output (output_ops NONE) prt));
+fun gen_writeln urgent prt =
+  (if urgent then Output.writelns_urgent else Output.writelns)
+    (Bytes.contents (output (output_ops NONE) prt));
+
+val writeln = gen_writeln false;
+val writeln_urgent = gen_writeln true;
 
 
 (* chunks *)
diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Mar 21 18:37:05 2025 +0100
@@ -223,6 +223,7 @@
   val consolidatingN: string val consolidating: T
   val consolidatedN: string val consolidated: T
   val exec_idN: string
+  val urgent_properties: Properties.T
   val initN: string
   val statusN: string val status: T
   val resultN: string val result: T
@@ -752,6 +753,8 @@
 
 val exec_idN = "exec_id";
 
+val urgent_properties = [("urgent", "true")];
+
 val initN = "init";
 val (statusN, status) = markup_elem "status";
 val (resultN, result) = markup_elem "result";
diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Mar 21 18:37:05 2025 +0100
@@ -584,6 +584,8 @@
 
   /* messages */
 
+  val Urgent = new Properties.Boolean("urgent")
+
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"
diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Mar 21 18:37:05 2025 +0100
@@ -107,6 +107,12 @@
 
   /* result messages */
 
+  def is_urgent(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(_, props), _) => Markup.Urgent.get(props)
+      case _ => false
+    }
+
   def is_result(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.RESULT, _), _) => true
diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Mar 21 18:37:05 2025 +0100
@@ -99,7 +99,9 @@
     val (states, other) =
       results.iterator.map(_._2).filterNot(Protocol.is_result).toList
         .partition(Protocol.is_state)
-    (if (output_state) states else Nil) ::: other
+    val (urgent, regular) = other.partition(Protocol.is_urgent)
+
+    urgent ::: (if (output_state) states else Nil) ::: regular
   }
 
 
diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/System/isabelle_process.ML	Fri Mar 21 18:37:05 2025 +0100
@@ -122,6 +122,8 @@
         (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #>
       Unsynchronized.setmp Private_Output.writeln_fn
         (fn s => standard_message (serial_props ()) Markup.writelnN s) #>
+      Unsynchronized.setmp Private_Output.writeln_urgent_fn
+        (fn s => standard_message (serial_props () @ Markup.urgent_properties) Markup.writelnN s) #>
       Unsynchronized.setmp Private_Output.state_fn
         (fn s => standard_message (serial_props ()) Markup.stateN s) #>
       Unsynchronized.setmp Private_Output.information_fn