# HG changeset patch # User wenzelm # Date 1281910048 -7200 # Node ID 9951852fae91dc6487360c133d769fb1226b0611 # Parent c13c95c97e899978bf533990eee8d5d72088c6ca simplified command status: interpret stacked markup on demand; diff -r c13c95c97e89 -r 9951852fae91 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Sun Aug 15 23:13:56 2010 +0200 +++ b/src/Pure/General/markup.ML Mon Aug 16 00:07:28 2010 +0200 @@ -104,13 +104,10 @@ 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: string -> T val forkedN: string val forked: T val joinedN: string val joined: T val failedN: string val failed: T val finishedN: string val finished: T - val disposedN: string val disposed: T val versionN: string val execN: string val assignN: string val assign: int -> T @@ -318,13 +315,11 @@ val taskN = "task"; -val (unprocessedN, unprocessed) = markup_elem "unprocessed"; -val (runningN, running) = markup_string "running" taskN; val (forkedN, forked) = markup_elem "forked"; val (joinedN, joined) = markup_elem "joined"; + val (failedN, failed) = markup_elem "failed"; val (finishedN, finished) = markup_elem "finished"; -val (disposedN, disposed) = markup_elem "disposed"; (* interactive documents *) diff -r c13c95c97e89 -r 9951852fae91 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Sun Aug 15 23:13:56 2010 +0200 +++ b/src/Pure/General/markup.scala Mon Aug 16 00:07:28 2010 +0200 @@ -193,13 +193,10 @@ val TASK = "task" - val UNPROCESSED = "unprocessed" - val RUNNING = "running" val FORKED = "forked" val JOINED = "joined" val FAILED = "failed" val FINISHED = "finished" - val DISPOSED = "disposed" /* interactive documents */ diff -r c13c95c97e89 -r 9951852fae91 src/Pure/Isar/toplevel.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/toplevel.scala Mon Aug 16 00:07:28 2010 +0200 @@ -0,0 +1,31 @@ +/* Title: Pure/Isar/toplevel.scala + Author: Makarius + +Isabelle/Isar toplevel transactions. +*/ + +package isabelle + + +object Toplevel +{ + sealed abstract class Status + case class Forked(forks: Int) extends Status + case object Unprocessed extends Status + case object Finished extends Status + case object Failed extends Status + + def command_status(markup: List[Markup]): Status = + { + val forks = (0 /: markup) { + case (i, Markup(Markup.FORKED, _)) => i + 1 + case (i, Markup(Markup.JOINED, _)) => i - 1 + case (i, _) => i + } + if (forks != 0) Forked(forks) + else if (markup.exists(_.name == Markup.FAILED)) Failed + else if (markup.exists(_.name == Markup.FINISHED)) Finished + else Unprocessed + } +} + diff -r c13c95c97e89 -r 9951852fae91 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sun Aug 15 23:13:56 2010 +0200 +++ b/src/Pure/PIDE/command.scala Mon Aug 16 00:07:28 2010 +0200 @@ -14,14 +14,6 @@ object Command { - object Status extends Enumeration - { - val UNPROCESSED = Value("UNPROCESSED") - val FINISHED = Value("FINISHED") - val FAILED = Value("FAILED") - val UNDEFINED = Value("UNDEFINED") - } - case class HighlightInfo(kind: String, sub_kind: Option[String]) { override def toString = kind } @@ -35,8 +27,7 @@ case class State( val command: Command, - val status: Command.Status.Value, - val forks: Int, + val status: List[Markup], val reverse_results: List[XML.Tree], val markup: Markup_Text) { @@ -90,15 +81,7 @@ def accumulate(message: XML.Tree): Command.State = message match { case XML.Elem(Markup(Markup.STATUS, _), elems) => - (this /: elems)((state, elem) => - elem match { - case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED) - case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED) - case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED) - case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1) - case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1) - case _ => System.err.println("Ignored status message: " + elem); state - }) + copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status) case XML.Elem(Markup(Markup.REPORT, _), elems) => (this /: elems)((state, elem) => @@ -184,6 +167,5 @@ /* accumulated results */ - val empty_state: Command.State = - Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source)) + val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source)) } diff -r c13c95c97e89 -r 9951852fae91 src/Pure/build-jars --- a/src/Pure/build-jars Sun Aug 15 23:13:56 2010 +0200 +++ b/src/Pure/build-jars Mon Aug 16 00:07:28 2010 +0200 @@ -36,6 +36,7 @@ Isar/keyword.scala Isar/outer_syntax.scala Isar/parse.scala + Isar/toplevel.scala Isar/token.scala PIDE/command.scala PIDE/document.scala diff -r c13c95c97e89 -r 9951852fae91 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Sun Aug 15 23:13:56 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 16 00:07:28 2010 +0200 @@ -28,14 +28,13 @@ { val state = snapshot.state(command) if (snapshot.is_outdated) new Color(240, 240, 240) - else if (state.forks > 0) new Color(255, 228, 225) - else if (state.forks < 0) Color.red else - state.status match { - case Command.Status.UNPROCESSED => new Color(255, 228, 225) - case Command.Status.FINISHED => new Color(234, 248, 255) - case Command.Status.FAILED => new Color(255, 193, 193) - case Command.Status.UNDEFINED => Color.red + Toplevel.command_status(state.status) match { + case Toplevel.Forked(i) if i > 0 => new Color(255, 228, 225) + case Toplevel.Finished => new Color(234, 248, 255) + case Toplevel.Failed => new Color(255, 193, 193) + case Toplevel.Unprocessed => new Color(255, 228, 225) + case _ => Color.red } }