1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 05 10:54:05 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jul 05 11:16:37 2011 +0200
     1.3 @@ -584,9 +584,9 @@
     1.4        (case worker_task () of
     1.5          NONE => I
     1.6        | SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]);
     1.7 -    val _ = Output.status (Markup.markup (task_props Markup.forked) "");
     1.8 +    val _ = Output.status (Markup.markup_only (task_props Markup.forked));
     1.9      val x = e ();  (*sic -- report "joined" only for success*)
    1.10 -    val _ = Output.status (Markup.markup (task_props Markup.joined) "");
    1.11 +    val _ = Output.status (Markup.markup_only (task_props Markup.joined));
    1.12    in x end;
    1.13  
    1.14  

     2.1 --- a/src/Pure/General/markup.ML	Tue Jul 05 10:54:05 2011 +0200
     2.2 +++ b/src/Pure/General/markup.ML	Tue Jul 05 11:16:37 2011 +0200
     2.3 @@ -110,7 +110,7 @@
     2.4    val versionN: string
     2.5    val execN: string
     2.6    val assignN: string val assign: int -> T
     2.7 -  val editN: string val edit: int -> int -> T
     2.8 +  val editN: string val edit: int * int -> T
     2.9    val serialN: string
    2.10    val promptN: string val prompt: T
    2.11    val readyN: string val ready: T
    2.12 @@ -123,6 +123,7 @@
    2.13    val output: T -> Output.output * Output.output
    2.14    val enclose: T -> Output.output -> Output.output
    2.15    val markup: T -> string -> string
    2.16 +  val markup_only: T -> string
    2.17  end;
    2.18  
    2.19  structure Markup: MARKUP =
    2.20 @@ -347,7 +348,7 @@
    2.21  val (assignN, assign) = markup_int "assign" versionN;
    2.22  
    2.23  val editN = "edit";
    2.24 -fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
    2.25 +fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
    2.26  
    2.27  
    2.28  (* messages *)
    2.29 @@ -387,4 +388,6 @@
    2.30    let val (bg, en) = output m
    2.31    in Library.enclose (Output.escape bg) (Output.escape en) end;
    2.32  
    2.33 +fun markup_only m = markup m "";
    2.34 +
    2.35  end;

     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 05 10:54:05 2011 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 05 11:16:37 2011 +0200
     3.3 @@ -567,7 +567,7 @@
     3.4    Position.setmp_thread_data pos f x;
     3.5  
     3.6  fun status tr m =
     3.7 -  setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
     3.8 +  setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
     3.9  
    3.10  fun error_msg tr msg =
    3.11    setmp_thread_position tr (fn () => Output.error_msg msg) ();

     4.1 --- a/src/Pure/PIDE/isar_document.ML	Tue Jul 05 10:54:05 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.ML	Tue Jul 05 11:16:37 2011 +0200
     4.3 @@ -33,9 +33,8 @@
     4.4        val _ = Document.cancel state;
     4.5        val (updates, state') = Document.edit old_id new_id edits state;
     4.6        val _ =
     4.7 -        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
     4.8 -        |> Markup.markup (Markup.assign new_id)
     4.9 -        |> Output.status;
    4.10 +        Output.status (Markup.markup (Markup.assign new_id)
    4.11 +          (implode (map (Markup.markup_only o Markup.edit) updates)));
    4.12        val state'' = Document.execute new_id state';
    4.13      in state'' end));
    4.14