# HG changeset patch # User wenzelm # Date 1333819724 -7200 # Node ID e6261a493f04264e4c8851dc32271503ad770dfe # Parent a360406f1fcbc2a071c6fbdbae043e47a84151d9 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel); diff -r a360406f1fcb -r e6261a493f04 src/Pure/PIDE/command.ML --- 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 = diff -r a360406f1fcb -r e6261a493f04 src/Pure/PIDE/document.ML --- 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; diff -r a360406f1fcb -r e6261a493f04 src/Pure/PIDE/document.scala --- 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 } + } } diff -r a360406f1fcb -r e6261a493f04 src/Pure/PIDE/isabelle_markup.ML --- 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"; diff -r a360406f1fcb -r e6261a493f04 src/Pure/PIDE/isabelle_markup.scala --- 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" diff -r a360406f1fcb -r e6261a493f04 src/Pure/PIDE/protocol.scala --- 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)