added command_state markup;
authorwenzelm
Thu, 15 Jan 2009 00:41:24 +0100
changeset 29482 fe044b49e34f
parent 29481 3e8420c1124a
child 29483 e959ae4a0bca
added command_state markup;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
--- 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 *)
 
--- 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 */