clarified command state -- markup within proper_range, excluding trailing whitespace;

--- a/src/Pure/PIDE/command.scala	Tue Mar 13 20:04:24 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Mar 13 21:17:37 2012 +0100
@@ -34,7 +34,7 @@
           (this /: msgs)((state, msg) =>
             msg match {
               case elem @ XML.Elem(markup, Nil) =>
-                state.add_status(markup).add_markup(Text.Info(command.range, elem))  // FIXME proper_range??
+                state.add_status(markup).add_markup(Text.Info(command.proper_range, elem))
 
               case _ => System.err.println("Ignored status message: " + msg); state
             })

--- a/src/Pure/PIDE/document.ML	Tue Mar 13 20:04:24 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Mar 13 21:17:37 2012 +0100
@@ -273,9 +273,13 @@
 
 (* commands *)
 
-fun tokenize_command id text =
+fun parse_command id text =
   Position.setmp_thread_data (Position.id_only id)
-    (fn () => Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text) ();
+    (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) ();
 
 fun define_command (id: command_id) name text =
   map_state (fn (versions, commands, execution) =>
@@ -284,7 +288,7 @@
         (singleton o Future.forks)
           {name = "Document.define_command", group = SOME (Future.new_group NONE),
             deps = [], pri = ~1, interrupts = false}
-          (fn () => tokenize_command (print_id id) text);
+          (fn () => parse_command (print_id id) text);
       val commands' =
         Inttab.update_new (id, (name, future)) commands
           handle Inttab.DUP dup => err_dup "command" dup;

--- a/src/Pure/PIDE/isabelle_markup.ML	Tue Mar 13 20:04:24 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Mar 13 21:17:37 2012 +0100
@@ -90,6 +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 forkedN: string val forked: Markup.T
   val joinedN: string val joined: Markup.T
   val failedN: string val failed: Markup.T
@@ -282,6 +283,7 @@
 
 val taskN = "task";
 
+val (parsedN, parsed) = markup_elem "parsed";
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
 

--- a/src/Pure/PIDE/isabelle_markup.scala	Tue Mar 13 20:04:24 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Mar 13 21:17:37 2012 +0100
@@ -198,6 +198,7 @@
 
   val TASK = "task"
 
+  val PARSED = "parsed"
   val FORKED = "forked"
   val JOINED = "joined"
   val FAILED = "failed"

--- a/src/Pure/PIDE/protocol.scala	Tue Mar 13 20:04:24 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Mar 13 21:17:37 2012 +0100
@@ -49,24 +49,27 @@
   }
 
   sealed case class Status(
+    private val parsed: Boolean = false,
     private val finished: Boolean = false,
     private val failed: Boolean = false,
     forks: Int = 0)
   {
-    def is_unprocessed: Boolean = !finished && !failed && forks == 0
+    def is_unprocessed: Boolean = parsed && !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(finished || that.finished, failed || that.failed, forks + that.forks)
+      Status(parsed || that.parsed, finished || that.finished,
+        failed || that.failed, forks + that.forks)
   }
 
   val command_status_markup: Set[String] =
-    Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
+    Set(Isabelle_Markup.PARSED, 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.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)