# HG changeset patch
# User wenzelm
# Date 1355418024 -3600
# Node ID 50f141b34bb798b40acad02db10b1716a9994365
# Parent  51408dde956f9415211b5d590410d92fc3cc6504
enable Isabelle/ML to produce uninterpreted result messages as well;

diff -r 51408dde956f -r 50f141b34bb7 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Thu Dec 13 17:46:33 2012 +0100
+++ b/src/Pure/General/output.ML	Thu Dec 13 18:00:24 2012 +0100
@@ -34,6 +34,7 @@
     val prompt_fn: (output -> unit) Unsynchronized.ref
     val status_fn: (output -> unit) Unsynchronized.ref
     val report_fn: (output -> unit) Unsynchronized.ref
+    val result_fn: (serial * output -> unit) Unsynchronized.ref
     val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
   end
   val urgent_message: string -> unit
@@ -42,6 +43,7 @@
   val prompt: string -> unit
   val status: string -> unit
   val report: string -> unit
+  val result: serial * string -> unit
   val protocol_message: Properties.T -> string -> unit
   exception TRACING_LIMIT of int
 end;
@@ -97,6 +99,7 @@
   val prompt_fn = Unsynchronized.ref physical_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
+  val result_fn = Unsynchronized.ref (fn _: serial * output => ());
   val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
     Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
 end;
@@ -110,6 +113,7 @@
 fun prompt s = ! Private_Hooks.prompt_fn (output s);
 fun status s = ! Private_Hooks.status_fn (output s);
 fun report s = ! Private_Hooks.report_fn (output s);
+fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
 fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
 
 exception TRACING_LIMIT of int;
diff -r 51408dde956f -r 50f141b34bb7 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Dec 13 17:46:33 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Dec 13 18:00:24 2012 +0100
@@ -106,6 +106,7 @@
   val serialN: string
   val initN: string
   val statusN: string
+  val resultN: string
   val writelnN: string
   val tracingN: string
   val warningN: string
@@ -357,6 +358,7 @@
 
 val initN = "init";
 val statusN = "status";
+val resultN = "result";
 val writelnN = "writeln";
 val tracingN = "tracing";
 val warningN = "warning";
@@ -383,7 +385,7 @@
 val padding_line = (paddingN, lineN);
 
 val dialogN = "dialog";
-fun dialog i result = (dialogN, [(serialN, print_int i), ("result", result)]);
+fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
 
 
 (* protocol message functions *)
diff -r 51408dde956f -r 50f141b34bb7 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Dec 13 17:46:33 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Dec 13 18:00:24 2012 +0100
@@ -286,7 +286,7 @@
   val PADDING_LINE = (PADDING, LINE)
 
   val DIALOG = "dialog"
-  val Result = new Properties.String("result")
+  val Result = new Properties.String(RESULT)
 
 
   /* protocol message functions */
diff -r 51408dde956f -r 50f141b34bb7 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Dec 13 17:46:33 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Dec 13 18:00:24 2012 +0100
@@ -126,6 +126,8 @@
   in
     Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN;
     Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN;
+    Output.Private_Hooks.result_fn :=
+      (fn (i, s) => standard_message mbox (SOME i) Markup.resultN s);
     Output.Private_Hooks.writeln_fn :=
       (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
     Output.Private_Hooks.tracing_fn :=