--- a/src/Pure/Concurrent/future.ML Tue Jul 05 10:54:05 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Jul 05 11:16:37 2011 +0200
@@ -584,9 +584,9 @@
(case worker_task () of
NONE => I
| SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
- val _ = Output.status (Markup.markup (task_props Markup.forked) "");
+ val _ = Output.status (Markup.markup_only (task_props Markup.forked));
val x = e (); (*sic -- report "joined" only for success*)
- val _ = Output.status (Markup.markup (task_props Markup.joined) "");
+ val _ = Output.status (Markup.markup_only (task_props Markup.joined));
in x end;
--- a/src/Pure/General/markup.ML Tue Jul 05 10:54:05 2011 +0200
+++ b/src/Pure/General/markup.ML Tue Jul 05 11:16:37 2011 +0200
@@ -110,7 +110,7 @@
val versionN: string
val execN: string
val assignN: string val assign: int -> T
- val editN: string val edit: int -> int -> T
+ val editN: string val edit: int * int -> T
val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
@@ -123,6 +123,7 @@
val output: T -> Output.output * Output.output
val enclose: T -> Output.output -> Output.output
val markup: T -> string -> string
+ val markup_only: T -> string
end;
structure Markup: MARKUP =
@@ -347,7 +348,7 @@
val (assignN, assign) = markup_int "assign" versionN;
val editN = "edit";
-fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
+fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
(* messages *)
@@ -387,4 +388,6 @@
let val (bg, en) = output m
in Library.enclose (Output.escape bg) (Output.escape en) end;
+fun markup_only m = markup m "";
+
end;
--- a/src/Pure/Isar/toplevel.ML Tue Jul 05 10:54:05 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Jul 05 11:16:37 2011 +0200
@@ -567,7 +567,7 @@
Position.setmp_thread_data pos f x;
fun status tr m =
- setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
+ setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
fun error_msg tr msg =
setmp_thread_position tr (fn () => Output.error_msg msg) ();
--- a/src/Pure/PIDE/isar_document.ML Tue Jul 05 10:54:05 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Tue Jul 05 11:16:37 2011 +0200
@@ -33,9 +33,8 @@
val _ = Document.cancel state;
val (updates, state') = Document.edit old_id new_id edits state;
val _ =
- implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
- |> Markup.markup (Markup.assign new_id)
- |> Output.status;
+ Output.status (Markup.markup (Markup.assign new_id)
+ (implode (map (Markup.markup_only o Markup.edit) updates)));
val state'' = Document.execute new_id state';
in state'' end));