1.1 --- a/src/Pure/General/output.ML	Thu Dec 13 17:46:33 2012 +0100
     1.2 +++ b/src/Pure/General/output.ML	Thu Dec 13 18:00:24 2012 +0100
     1.3 @@ -34,6 +34,7 @@
     1.4      val prompt_fn: (output -> unit) Unsynchronized.ref
     1.5      val status_fn: (output -> unit) Unsynchronized.ref
     1.6      val report_fn: (output -> unit) Unsynchronized.ref
     1.7 +    val result_fn: (serial * output -> unit) Unsynchronized.ref
     1.8      val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
     1.9    end
    1.10    val urgent_message: string -> unit
    1.11 @@ -42,6 +43,7 @@
    1.12    val prompt: string -> unit
    1.13    val status: string -> unit
    1.14    val report: string -> unit
    1.15 +  val result: serial * string -> unit
    1.16    val protocol_message: Properties.T -> string -> unit
    1.17    exception TRACING_LIMIT of int
    1.18  end;
    1.19 @@ -97,6 +99,7 @@
    1.20    val prompt_fn = Unsynchronized.ref physical_stdout;
    1.21    val status_fn = Unsynchronized.ref (fn _: output => ());
    1.22    val report_fn = Unsynchronized.ref (fn _: output => ());
    1.23 +  val result_fn = Unsynchronized.ref (fn _: serial * output => ());
    1.24    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    1.25      Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
    1.26  end;
    1.27 @@ -110,6 +113,7 @@
    1.28  fun prompt s = ! Private_Hooks.prompt_fn (output s);
    1.29  fun status s = ! Private_Hooks.status_fn (output s);
    1.30  fun report s = ! Private_Hooks.report_fn (output s);
    1.31 +fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
    1.32  fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
    1.33  
    1.34  exception TRACING_LIMIT of int;

     2.1 --- a/src/Pure/PIDE/markup.ML	Thu Dec 13 17:46:33 2012 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Thu Dec 13 18:00:24 2012 +0100
     2.3 @@ -106,6 +106,7 @@
     2.4    val serialN: string
     2.5    val initN: string
     2.6    val statusN: string
     2.7 +  val resultN: string
     2.8    val writelnN: string
     2.9    val tracingN: string
    2.10    val warningN: string
    2.11 @@ -357,6 +358,7 @@
    2.12  
    2.13  val initN = "init";
    2.14  val statusN = "status";
    2.15 +val resultN = "result";
    2.16  val writelnN = "writeln";
    2.17  val tracingN = "tracing";
    2.18  val warningN = "warning";
    2.19 @@ -383,7 +385,7 @@
    2.20  val padding_line = (paddingN, lineN);
    2.21  
    2.22  val dialogN = "dialog";
    2.23 -fun dialog i result = (dialogN, [(serialN, print_int i), ("result", result)]);
    2.24 +fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
    2.25  
    2.26  
    2.27  (* protocol message functions *)

     3.1 --- a/src/Pure/PIDE/markup.scala	Thu Dec 13 17:46:33 2012 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Thu Dec 13 18:00:24 2012 +0100
     3.3 @@ -286,7 +286,7 @@
     3.4    val PADDING_LINE = (PADDING, LINE)
     3.5  
     3.6    val DIALOG = "dialog"
     3.7 -  val Result = new Properties.String("result")
     3.8 +  val Result = new Properties.String(RESULT)
     3.9  
    3.10  
    3.11    /* protocol message functions */

     4.1 --- a/src/Pure/System/isabelle_process.ML	Thu Dec 13 17:46:33 2012 +0100
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Dec 13 18:00:24 2012 +0100
     4.3 @@ -126,6 +126,8 @@
     4.4    in
     4.5      Output.Private_Hooks.status_fn := standard_message mbox NONE Markup.statusN;
     4.6      Output.Private_Hooks.report_fn := standard_message mbox NONE Markup.reportN;
     4.7 +    Output.Private_Hooks.result_fn :=
     4.8 +      (fn (i, s) => standard_message mbox (SOME i) Markup.resultN s);
     4.9      Output.Private_Hooks.writeln_fn :=
    4.10        (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
    4.11      Output.Private_Hooks.tracing_fn :=