# HG changeset patch
# User wenzelm
# Date 1232016829 -3600
# Node ID 8fc3aeece219be5bfe75d3a33c8c5bb21e6acec3
# Parent  06f4bb9fdb859fbf8aeeebb0fd08540122c67e33
replaced command_state by edits/edit;

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 *)
diff -r 06f4bb9fdb85 -r 8fc3aeece219 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Thu Jan 15 00:48:45 2009 +0100
+++ b/src/Pure/General/markup.scala	Thu Jan 15 11:53:49 2009 +0100
@@ -117,7 +117,12 @@
   val FAILED = "failed"
   val FINISHED = "finished"
   val DISPOSED = "disposed"
-  val COMMAND_STATE = "command_state"
+
+
+  /* interactive documents */
+
+  val EDITS = "edits"
+  val EDIT = "edit"
 
 
   /* messages */