diff -r 06f4bb9fdb85 -r 8fc3aeece219 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Jan 15 00:48:45 2009 +0100
+++ b/src/Pure/General/markup.ML	Thu Jan 15 11:53:49 2009 +0100
@@ -91,7 +91,8 @@
   val failedN: string val failed: T
   val finishedN: string val finished: T
   val disposedN: string val disposed: T
-  val command_stateN: string val command_state: string -> string -> T
+  val editsN: string val edits: string -> T
+  val editN: string val edit: string -> string -> T
   val pidN: string
   val sessionN: string
   val classN: string
@@ -269,8 +270,13 @@
 val (finishedN, finished) = markup_elem "finished";
 val (disposedN, disposed) = markup_elem "disposed";
 
-val command_stateN = "command_state";
-fun command_state id state_id : T = (command_stateN, [(idN, id), (stateN, state_id)]);
+
+(* interactive documents *)
+
+val (editsN, edits) = markup_string "edits" idN;
+
+val editN = "edit";
+fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
 
 
 (* messages *)