# HG changeset patch
# User wenzelm
# Date 1231540439 -3600
# Node ID 779ff118732788d271bcdf04880c058522b8b726
# Parent  438c39fc93c8f4850abb93f116b1a8d12d9c13b2
added running task markup;

diff -r 438c39fc93c8 -r 779ff1187327 src/Pure/General/markup.ML
--- 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";
diff -r 438c39fc93c8 -r 779ff1187327 src/Pure/General/markup.scala
--- 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"
diff -r 438c39fc93c8 -r 779ff1187327 src/Pure/Isar/isar.ML
--- 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;