--- 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 */