explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
--- a/src/Pure/General/markup.ML Mon Jan 04 18:55:32 2010 +0100
+++ b/src/Pure/General/markup.ML Mon Jan 04 18:56:36 2010 +0100
@@ -105,6 +105,7 @@
val failedN: string val failed: T
val finishedN: string val finished: T
val disposedN: string val disposed: T
+ val assignN: string val assign: T
val editN: string val edit: string -> string -> T
val pidN: string
val promptN: string val prompt: T
@@ -305,6 +306,8 @@
(* interactive documents *)
+val (assignN, assign) = markup_elem "assign";
+
val editN = "edit";
fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
--- a/src/Pure/General/markup.scala Mon Jan 04 18:55:32 2010 +0100
+++ b/src/Pure/General/markup.scala Mon Jan 04 18:56:36 2010 +0100
@@ -153,6 +153,7 @@
/* interactive documents */
+ val ASSIGN = "assign"
val EDIT = "edit"
--- a/src/Pure/Isar/isar_document.ML Mon Jan 04 18:55:32 2010 +0100
+++ b/src/Pure/Isar/isar_document.ML Mon Jan 04 18:56:36 2010 +0100
@@ -234,8 +234,9 @@
fun report_updates [] = ()
| report_updates updates =
- Output.status
- (implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates));
+ implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
+ |> Markup.markup Markup.assign
+ |> Output.status;
in