# HG changeset patch
# User wenzelm
# Date 1231976484 -3600
# Node ID fe044b49e34fe09076043b6c44d781fc84441a50
# Parent  3e8420c1124a485be0a1da2a629f815941998249
added command_state markup;

diff -r 3e8420c1124a -r fe044b49e34f src/Pure/General/markup.ML
--- 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 *)
 
diff -r 3e8420c1124a -r fe044b49e34f src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Jan 14 19:38:55 2009 +0100
+++ b/src/Pure/General/markup.scala	Thu Jan 15 00:41:24 2009 +0100
@@ -117,6 +117,7 @@
   val FAILED = "failed"
   val FINISHED = "finished"
   val DISPOSED = "disposed"
+  val COMMAND_STATE = "command_state"
 
 
   /* messages */