merged

--- a/src/Pure/General/markup.ML	Fri Jan 09 19:41:33 2009 +0100
+++ b/src/Pure/General/markup.ML	Fri Jan 09 23:39:53 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	Fri Jan 09 19:41:33 2009 +0100
+++ b/src/Pure/General/markup.scala	Fri Jan 09 23:39:53 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	Fri Jan 09 19:41:33 2009 +0100
+++ b/src/Pure/Isar/isar.ML	Fri Jan 09 23:39:53 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;
 

--- a/src/Pure/Isar/proof.ML	Fri Jan 09 19:41:33 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Jan 09 23:39:53 2009 +0100
@@ -345,7 +345,8 @@
       (case filter_out (fn s => s = "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
+    fun prt_goal (SOME (ctxt, (i,
+      {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^

--- a/src/Pure/Thy/thy_load.ML	Fri Jan 09 19:41:33 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Jan 09 23:39:53 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/thy_load.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Theory loader primitives, including load path.
@@ -22,6 +21,7 @@
   val ml_exts: string list
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
+  val split_thy_path: Path.T -> Path.T * string
   val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_thy: Path.T -> string -> Path.T * File.ident
@@ -62,6 +62,11 @@
 val ml_path = Path.ext "ML" o Path.basic;
 val thy_path = Path.ext "thy" o Path.basic;
 
+fun split_thy_path path =
+  (case Path.split_ext path of
+    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
+  | _ => error ("Bad theory file specification " ^ Path.implode path));
+
 
 (* check files *)