clarified command state -- markup within proper_range, excluding trailing whitespace;
authorwenzelm
Tue Mar 13 21:17:37 2012 +0100 (2012-03-13 ago)
changeset 469103e068ef04b42
parent 46909 3c73a121a387
child 46911 6d2a2f0e904e
clarified command state -- markup within proper_range, excluding trailing whitespace;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Mar 13 20:04:24 2012 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Mar 13 21:17:37 2012 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4            (this /: msgs)((state, msg) =>
     1.5              msg match {
     1.6                case elem @ XML.Elem(markup, Nil) =>
     1.7 -                state.add_status(markup).add_markup(Text.Info(command.range, elem))  // FIXME proper_range??
     1.8 +                state.add_status(markup).add_markup(Text.Info(command.proper_range, elem))
     1.9  
    1.10                case _ => System.err.println("Ignored status message: " + msg); state
    1.11              })
     2.1 --- a/src/Pure/PIDE/document.ML	Tue Mar 13 20:04:24 2012 +0100
     2.2 +++ b/src/Pure/PIDE/document.ML	Tue Mar 13 21:17:37 2012 +0100
     2.3 @@ -273,9 +273,13 @@
     2.4  
     2.5  (* commands *)
     2.6  
     2.7 -fun tokenize_command id text =
     2.8 +fun parse_command id text =
     2.9    Position.setmp_thread_data (Position.id_only id)
    2.10 -    (fn () => Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text) ();
    2.11 +    (fn () =>
    2.12 +      let
    2.13 +        val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
    2.14 +        val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
    2.15 +      in toks end) ();
    2.16  
    2.17  fun define_command (id: command_id) name text =
    2.18    map_state (fn (versions, commands, execution) =>
    2.19 @@ -284,7 +288,7 @@
    2.20          (singleton o Future.forks)
    2.21            {name = "Document.define_command", group = SOME (Future.new_group NONE),
    2.22              deps = [], pri = ~1, interrupts = false}
    2.23 -          (fn () => tokenize_command (print_id id) text);
    2.24 +          (fn () => parse_command (print_id id) text);
    2.25        val commands' =
    2.26          Inttab.update_new (id, (name, future)) commands
    2.27            handle Inttab.DUP dup => err_dup "command" dup;
     3.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Tue Mar 13 20:04:24 2012 +0100
     3.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Mar 13 21:17:37 2012 +0100
     3.3 @@ -90,6 +90,7 @@
     3.4    val sendbackN: string val sendback: Markup.T
     3.5    val hiliteN: string val hilite: Markup.T
     3.6    val taskN: string
     3.7 +  val parsedN: string val parsed: Markup.T
     3.8    val forkedN: string val forked: Markup.T
     3.9    val joinedN: string val joined: Markup.T
    3.10    val failedN: string val failed: Markup.T
    3.11 @@ -282,6 +283,7 @@
    3.12  
    3.13  val taskN = "task";
    3.14  
    3.15 +val (parsedN, parsed) = markup_elem "parsed";
    3.16  val (forkedN, forked) = markup_elem "forked";
    3.17  val (joinedN, joined) = markup_elem "joined";
    3.18  
     4.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Tue Mar 13 20:04:24 2012 +0100
     4.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Mar 13 21:17:37 2012 +0100
     4.3 @@ -198,6 +198,7 @@
     4.4  
     4.5    val TASK = "task"
     4.6  
     4.7 +  val PARSED = "parsed"
     4.8    val FORKED = "forked"
     4.9    val JOINED = "joined"
    4.10    val FAILED = "failed"
     5.1 --- a/src/Pure/PIDE/protocol.scala	Tue Mar 13 20:04:24 2012 +0100
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Mar 13 21:17:37 2012 +0100
     5.3 @@ -49,24 +49,27 @@
     5.4    }
     5.5  
     5.6    sealed case class Status(
     5.7 +    private val parsed: Boolean = false,
     5.8      private val finished: Boolean = false,
     5.9      private val failed: Boolean = false,
    5.10      forks: Int = 0)
    5.11    {
    5.12 -    def is_unprocessed: Boolean = !finished && !failed && forks == 0
    5.13 +    def is_unprocessed: Boolean = parsed && !finished && !failed && forks == 0
    5.14      def is_running: Boolean = forks != 0
    5.15      def is_finished: Boolean = finished && forks == 0
    5.16      def is_failed: Boolean = failed && forks == 0
    5.17      def + (that: Status): Status =
    5.18 -      Status(finished || that.finished, failed || that.failed, forks + that.forks)
    5.19 +      Status(parsed || that.parsed, finished || that.finished,
    5.20 +        failed || that.failed, forks + that.forks)
    5.21    }
    5.22  
    5.23    val command_status_markup: Set[String] =
    5.24 -    Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
    5.25 +    Set(Isabelle_Markup.PARSED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
    5.26        Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
    5.27  
    5.28    def command_status(status: Status, markup: Markup): Status =
    5.29      markup match {
    5.30 +      case Markup(Isabelle_Markup.PARSED, _) => status.copy(parsed = true)
    5.31        case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
    5.32        case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
    5.33        case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)