# HG changeset patch
# User wenzelm
# Date 1309857397 -7200
# Node ID 573d1272f36d900351ae042bc021053995670132
# Parent  47af50b0c8c54dee7c56a2e977016da01e68fcdb
tuned signature;
tuned;

diff -r 47af50b0c8c5 -r 573d1272f36d src/Pure/Concurrent/future.ML
--- 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;
 
 
diff -r 47af50b0c8c5 -r 573d1272f36d src/Pure/General/markup.ML
--- 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;
diff -r 47af50b0c8c5 -r 573d1272f36d src/Pure/Isar/toplevel.ML
--- 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) ();
diff -r 47af50b0c8c5 -r 573d1272f36d src/Pure/PIDE/isar_document.ML
--- 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));