src/Pure/General/markup.ML
changeset 29482 fe044b49e34f
parent 29417 779ff1187327
child 29488 8fc3aeece219
--- a/src/Pure/General/markup.ML	Wed Jan 14 19:38:55 2009 +0100
+++ b/src/Pure/General/markup.ML	Thu Jan 15 00:41:24 2009 +0100
@@ -91,6 +91,7 @@
   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 pidN: string
   val sessionN: string
   val classN: string
@@ -268,6 +269,9 @@
 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)]);
+
 
 (* messages *)