# HG changeset patch
# User wenzelm
# Date 1442840843 -7200
# Node ID 7a421e7ef97c3220b06309e2de7ba31cdda28f43
# Parent  19118f9b939d309640859321b231644211ba9945
tuned signature;

diff -r 19118f9b939d -r 7a421e7ef97c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Sep 21 14:56:55 2015 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Sep 21 15:07:23 2015 +0200
@@ -155,16 +155,16 @@
   val failedN: string val failed: T
   val exec_idN: string
   val initN: string
-  val statusN: string
-  val resultN: string
-  val writelnN: string
-  val stateN: string
-  val informationN: string
-  val tracingN: string
-  val warningN: string
-  val legacyN: string
-  val errorN: string
-  val systemN: string
+  val statusN: string val status: T
+  val resultN: string val result: T
+  val writelnN: string val writeln: T
+  val stateN: string val state: T
+  val informationN: string val information: T
+  val tracingN: string val tracing: T
+  val warningN: string val warning: T
+  val legacyN: string val legacy: T
+  val errorN: string val error: T
+  val systemN: string val system: T
   val protocolN: string
   val reportN: string val report: T
   val no_reportN: string val no_report: T
@@ -550,16 +550,16 @@
 val exec_idN = "exec_id";
 
 val initN = "init";
-val statusN = "status";
-val resultN = "result";
-val writelnN = "writeln";
-val stateN = "state"
-val informationN = "information";
-val tracingN = "tracing";
-val warningN = "warning";
-val legacyN = "legacy";
-val errorN = "error";
-val systemN = "system";
+val (statusN, status) = markup_elem "status";
+val (resultN, result) = markup_elem "result";
+val (writelnN, writeln) = markup_elem "writeln";
+val (stateN, state) = markup_elem "state"
+val (informationN, information) = markup_elem "information";
+val (tracingN, tracing) = markup_elem "tracing";
+val (warningN, warning) = markup_elem "warning";
+val (legacyN, legacy) = markup_elem "legacy";
+val (errorN, error) = markup_elem "error";
+val (systemN, system) = markup_elem "system";
 val protocolN = "protocol";
 
 val (reportN, report) = markup_elem "report";
@@ -645,7 +645,7 @@
   fun add_mode name output =
     Synchronized.change modes (fn tab =>
       (if not (Symtab.defined tab name) then ()
-       else warning ("Redefining markup mode " ^ quote name);
+       else Output.warning ("Redefining markup mode " ^ quote name);
        Symtab.update (name, {output = output}) tab));
   fun get_mode () =
     the_default default
diff -r 19118f9b939d -r 7a421e7ef97c src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Mon Sep 21 14:56:55 2015 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Mon Sep 21 15:07:23 2015 +0200
@@ -22,9 +22,8 @@
           let
             fun result s = Output.result [(Markup.instanceN, instance)] [s];
             fun status m = result (Markup.markup_only m);
-            fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
-            fun toplevel_error exn =
-              result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
+            fun output_result s = result (Markup.markup Markup.writeln s);
+            fun toplevel_error exn = result (Markup.markup Markup.error (Runtime.exn_message exn));
 
             val _ = status Markup.running;
             fun run () = f {state = state, args = args, output_result = output_result};
@@ -43,7 +42,7 @@
   register {name = "print_state", pri = Task_Queue.urgent_pri + 2}
     (fn {state = st, output_result, ...} =>
       if Toplevel.is_proof st
-      then output_result (Markup.markup (Markup.stateN, []) (Toplevel.string_of_state st))
+      then output_result (Markup.markup Markup.state (Toplevel.string_of_state st))
       else ());
 
 end;