--- 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
--- 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;