added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);

--- a/src/Pure/PIDE/command.ML	Sat Apr 07 18:08:29 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Apr 07 19:28:44 2012 +0200
@@ -6,7 +6,6 @@
 
 signature COMMAND =
 sig
-  val parse_command: string -> string -> Token.T list
   type 'a memo
   val memo: (unit -> 'a) -> 'a memo
   val memo_value: 'a -> 'a memo
@@ -18,17 +17,6 @@
 structure Command: COMMAND =
 struct
 
-(* parse command *)
-
-fun parse_command id text =
-  Position.setmp_thread_data (Position.id_only id)
-    (fn () =>
-      let
-        val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
-        val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
-      in toks end) ();
-
-
 (* memo results *)
 
 datatype 'a expr =

--- a/src/Pure/PIDE/document.ML	Sat Apr 07 18:08:29 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Apr 07 19:28:44 2012 +0200
@@ -276,7 +276,15 @@
 fun define_command (id: command_id) name text =
   map_state (fn (versions, commands, execution) =>
     let
-      val span = Lazy.lazy (fn () => Command.parse_command (print_id id) text);
+      val id_string = print_id id;
+      val span = Lazy.lazy (fn () =>
+        Position.setmp_thread_data (Position.id_only id_string)
+          (fn () =>
+            Thy_Syntax.parse_tokens
+              (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
+      val _ =
+        Position.setmp_thread_data (Position.id_only id_string)
+          (fn () => Output.status (Markup.markup_only Isabelle_Markup.accepted)) ();
       val commands' =
         Inttab.update_new (id, (name, span)) commands
           handle Inttab.DUP dup => err_dup "command" dup;

--- a/src/Pure/PIDE/document.scala	Sat Apr 07 18:08:29 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Apr 07 19:28:44 2012 +0200
@@ -364,7 +364,7 @@
       }
 
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
-    def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)  // FIXME rename
+    def the_command_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
     def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment =
       assignments.getOrElse(version.id, fail)
@@ -390,7 +390,7 @@
       val (changed_commands, new_execs) =
         ((Nil: List[Command], execs) /: command_execs) {
           case ((commands1, execs1), (cmd_id, exec)) =>
-            val st = the_command(cmd_id)
+            val st = the_command_state(cmd_id)
             val commands2 = st.command :: commands1
             val execs2 =
               exec match {
@@ -470,7 +470,11 @@
         the_exec(the_assignment(version).check_finished.command_execs
           .getOrElse(command.id, fail))
       }
-      catch { case _: State.Fail => command.empty_state }
+      catch {
+        case _: State.Fail =>
+          try { the_command_state(command.id) }
+          catch { case _: State.Fail => command.empty_state }
+      }
     }
 
 

--- a/src/Pure/PIDE/isabelle_markup.ML	Sat Apr 07 18:08:29 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Sat Apr 07 19:28:44 2012 +0200
@@ -90,7 +90,7 @@
   val sendbackN: string val sendback: Markup.T
   val hiliteN: string val hilite: Markup.T
   val taskN: string
-  val parsedN: string val parsed: Markup.T
+  val acceptedN: string val accepted: Markup.T
   val forkedN: string val forked: Markup.T
   val joinedN: string val joined: Markup.T
   val failedN: string val failed: Markup.T
@@ -283,7 +283,7 @@
 
 val taskN = "task";
 
-val (parsedN, parsed) = markup_elem "parsed";
+val (acceptedN, accepted) = markup_elem "accepted";
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
 

--- a/src/Pure/PIDE/isabelle_markup.scala	Sat Apr 07 18:08:29 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Sat Apr 07 19:28:44 2012 +0200
@@ -198,7 +198,7 @@
 
   val TASK = "task"
 
-  val PARSED = "parsed"
+  val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
   val FAILED = "failed"

--- a/src/Pure/PIDE/protocol.scala	Sat Apr 07 18:08:29 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Apr 07 19:28:44 2012 +0200
@@ -49,27 +49,27 @@
   }
 
   sealed case class Status(
-    private val parsed: Boolean = false,
+    private val accepted: Boolean = false,
     private val finished: Boolean = false,
     private val failed: Boolean = false,
     forks: Int = 0)
   {
-    def is_unprocessed: Boolean = parsed && !finished && !failed && forks == 0
+    def is_unprocessed: Boolean = accepted && !finished && !failed && forks == 0
     def is_running: Boolean = forks != 0
     def is_finished: Boolean = finished && forks == 0
     def is_failed: Boolean = failed && forks == 0
     def + (that: Status): Status =
-      Status(parsed || that.parsed, finished || that.finished,
+      Status(accepted || that.accepted, finished || that.finished,
         failed || that.failed, forks + that.forks)
   }
 
   val command_status_markup: Set[String] =
-    Set(Isabelle_Markup.PARSED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
+    Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
       Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
 
   def command_status(status: Status, markup: Markup): Status =
     markup match {
-      case Markup(Isabelle_Markup.PARSED, _) => status.copy(parsed = true)
+      case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
       case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
       case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
       case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)