# HG changeset patch
# User wenzelm
# Date 1262627796 -3600
# Node ID 5ccdc8bf3849a1e53e862055641ea86cc2522ece
# Parent  8611f1813fc92b06676dc290ca4f65ac8da4dad5
explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);

diff -r 8611f1813fc9 -r 5ccdc8bf3849 src/Pure/General/markup.ML
--- 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)]);
 
diff -r 8611f1813fc9 -r 5ccdc8bf3849 src/Pure/General/markup.scala
--- 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"
 
 
diff -r 8611f1813fc9 -r 5ccdc8bf3849 src/Pure/Isar/isar_document.ML
--- 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