--- a/src/Pure/General/markup.ML Thu Jan 08 13:18:34 2009 +0100
+++ b/src/Pure/General/markup.ML Fri Jan 09 23:33:59 2009 +0100
@@ -85,8 +85,9 @@
val subgoalN: string val subgoal: T
val sendbackN: string val sendback: T
val hiliteN: string val hilite: T
+ val taskN: string
val unprocessedN: string val unprocessed: T
- val runningN: string val running: T
+ val runningN: string val running: string -> T
val failedN: string val failed: T
val finishedN: string val finished: T
val disposedN: string val disposed: T
@@ -259,8 +260,10 @@
(* command status *)
+val taskN = "task";
+
val (unprocessedN, unprocessed) = markup_elem "unprocessed";
-val (runningN, running) = markup_elem "running";
+val (runningN, running) = markup_string "running" taskN;
val (failedN, failed) = markup_elem "failed";
val (finishedN, finished) = markup_elem "finished";
val (disposedN, disposed) = markup_elem "disposed";
--- a/src/Pure/General/markup.scala Thu Jan 08 13:18:34 2009 +0100
+++ b/src/Pure/General/markup.scala Fri Jan 09 23:33:59 2009 +0100
@@ -110,6 +110,8 @@
/* command status */
+ val TASK = "task"
+
val UNPROCESSED = "unprocessed"
val RUNNING = "running"
val FAILED = "failed"
--- a/src/Pure/Isar/isar.ML Thu Jan 08 13:18:34 2009 +0100
+++ b/src/Pure/Isar/isar.ML Fri Jan 09 23:33:59 2009 +0100
@@ -194,7 +194,7 @@
Finished of Toplevel.state;
fun status_markup Unprocessed = Markup.unprocessed
- | status_markup Running = Markup.running
+ | status_markup Running = (Markup.runningN, [])
| status_markup (Failed _) = Markup.failed
| status_markup (Finished _) = Markup.finished;