--- 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 *)
--- 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 */
--- /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
+ }
+}
+
--- 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))
}
--- 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
--- 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
}
}