simplified command status: interpret stacked markup on demand;
authorwenzelm
Mon Aug 16 00:07:28 2010 +0200 (2010-08-16)
changeset 384299951852fae91
parent 38428 c13c95c97e89
child 38443 be39c9e5ac39
simplified command status: interpret stacked markup on demand;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/Isar/toplevel.scala
src/Pure/PIDE/command.scala
src/Pure/build-jars
src/Tools/jEdit/src/jedit/document_view.scala
     1.1 --- a/src/Pure/General/markup.ML	Sun Aug 15 23:13:56 2010 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Mon Aug 16 00:07:28 2010 +0200
     1.3 @@ -104,13 +104,10 @@
     1.4    val sendbackN: string val sendback: T
     1.5    val hiliteN: string val hilite: T
     1.6    val taskN: string
     1.7 -  val unprocessedN: string val unprocessed: T
     1.8 -  val runningN: string val running: string -> T
     1.9    val forkedN: string val forked: T
    1.10    val joinedN: string val joined: T
    1.11    val failedN: string val failed: T
    1.12    val finishedN: string val finished: T
    1.13 -  val disposedN: string val disposed: T
    1.14    val versionN: string
    1.15    val execN: string
    1.16    val assignN: string val assign: int -> T
    1.17 @@ -318,13 +315,11 @@
    1.18  
    1.19  val taskN = "task";
    1.20  
    1.21 -val (unprocessedN, unprocessed) = markup_elem "unprocessed";
    1.22 -val (runningN, running) = markup_string "running" taskN;
    1.23  val (forkedN, forked) = markup_elem "forked";
    1.24  val (joinedN, joined) = markup_elem "joined";
    1.25 +
    1.26  val (failedN, failed) = markup_elem "failed";
    1.27  val (finishedN, finished) = markup_elem "finished";
    1.28 -val (disposedN, disposed) = markup_elem "disposed";
    1.29  
    1.30  
    1.31  (* interactive documents *)
     2.1 --- a/src/Pure/General/markup.scala	Sun Aug 15 23:13:56 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Mon Aug 16 00:07:28 2010 +0200
     2.3 @@ -193,13 +193,10 @@
     2.4  
     2.5    val TASK = "task"
     2.6  
     2.7 -  val UNPROCESSED = "unprocessed"
     2.8 -  val RUNNING = "running"
     2.9    val FORKED = "forked"
    2.10    val JOINED = "joined"
    2.11    val FAILED = "failed"
    2.12    val FINISHED = "finished"
    2.13 -  val DISPOSED = "disposed"
    2.14  
    2.15  
    2.16    /* interactive documents */
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/toplevel.scala	Mon Aug 16 00:07:28 2010 +0200
     3.3 @@ -0,0 +1,31 @@
     3.4 +/*  Title:      Pure/Isar/toplevel.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Isabelle/Isar toplevel transactions.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Toplevel
    3.14 +{
    3.15 +  sealed abstract class Status
    3.16 +  case class Forked(forks: Int) extends Status
    3.17 +  case object Unprocessed extends Status
    3.18 +  case object Finished extends Status
    3.19 +  case object Failed extends Status
    3.20 +
    3.21 +  def command_status(markup: List[Markup]): Status =
    3.22 +  {
    3.23 +    val forks = (0 /: markup) {
    3.24 +      case (i, Markup(Markup.FORKED, _)) => i + 1
    3.25 +      case (i, Markup(Markup.JOINED, _)) => i - 1
    3.26 +      case (i, _) => i
    3.27 +    }
    3.28 +    if (forks != 0) Forked(forks)
    3.29 +    else if (markup.exists(_.name == Markup.FAILED)) Failed
    3.30 +    else if (markup.exists(_.name == Markup.FINISHED)) Finished
    3.31 +    else Unprocessed
    3.32 +  }
    3.33 +}
    3.34 +
     4.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 15 23:13:56 2010 +0200
     4.2 +++ b/src/Pure/PIDE/command.scala	Mon Aug 16 00:07:28 2010 +0200
     4.3 @@ -14,14 +14,6 @@
     4.4  
     4.5  object Command
     4.6  {
     4.7 -  object Status extends Enumeration
     4.8 -  {
     4.9 -    val UNPROCESSED = Value("UNPROCESSED")
    4.10 -    val FINISHED = Value("FINISHED")
    4.11 -    val FAILED = Value("FAILED")
    4.12 -    val UNDEFINED = Value("UNDEFINED")
    4.13 -  }
    4.14 -
    4.15    case class HighlightInfo(kind: String, sub_kind: Option[String]) {
    4.16      override def toString = kind
    4.17    }
    4.18 @@ -35,8 +27,7 @@
    4.19  
    4.20    case class State(
    4.21      val command: Command,
    4.22 -    val status: Command.Status.Value,
    4.23 -    val forks: Int,
    4.24 +    val status: List[Markup],
    4.25      val reverse_results: List[XML.Tree],
    4.26      val markup: Markup_Text)
    4.27    {
    4.28 @@ -90,15 +81,7 @@
    4.29      def accumulate(message: XML.Tree): Command.State =
    4.30        message match {
    4.31          case XML.Elem(Markup(Markup.STATUS, _), elems) =>
    4.32 -          (this /: elems)((state, elem) =>
    4.33 -            elem match {
    4.34 -              case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED)
    4.35 -              case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED)
    4.36 -              case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED)
    4.37 -              case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1)
    4.38 -              case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1)
    4.39 -              case _ => System.err.println("Ignored status message: " + elem); state
    4.40 -            })
    4.41 +          copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
    4.42  
    4.43          case XML.Elem(Markup(Markup.REPORT, _), elems) =>
    4.44            (this /: elems)((state, elem) =>
    4.45 @@ -184,6 +167,5 @@
    4.46  
    4.47    /* accumulated results */
    4.48  
    4.49 -  val empty_state: Command.State =
    4.50 -    Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source))
    4.51 +  val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
    4.52  }
     5.1 --- a/src/Pure/build-jars	Sun Aug 15 23:13:56 2010 +0200
     5.2 +++ b/src/Pure/build-jars	Mon Aug 16 00:07:28 2010 +0200
     5.3 @@ -36,6 +36,7 @@
     5.4    Isar/keyword.scala
     5.5    Isar/outer_syntax.scala
     5.6    Isar/parse.scala
     5.7 +  Isar/toplevel.scala
     5.8    Isar/token.scala
     5.9    PIDE/command.scala
    5.10    PIDE/document.scala
     6.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 15 23:13:56 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Aug 16 00:07:28 2010 +0200
     6.3 @@ -28,14 +28,13 @@
     6.4    {
     6.5      val state = snapshot.state(command)
     6.6      if (snapshot.is_outdated) new Color(240, 240, 240)
     6.7 -    else if (state.forks > 0) new Color(255, 228, 225)
     6.8 -    else if (state.forks < 0) Color.red
     6.9      else
    6.10 -      state.status match {
    6.11 -        case Command.Status.UNPROCESSED => new Color(255, 228, 225)
    6.12 -        case Command.Status.FINISHED => new Color(234, 248, 255)
    6.13 -        case Command.Status.FAILED => new Color(255, 193, 193)
    6.14 -        case Command.Status.UNDEFINED => Color.red
    6.15 +      Toplevel.command_status(state.status) match {
    6.16 +        case Toplevel.Forked(i) if i > 0 => new Color(255, 228, 225)
    6.17 +        case Toplevel.Finished => new Color(234, 248, 255)
    6.18 +        case Toplevel.Failed => new Color(255, 193, 193)
    6.19 +        case Toplevel.Unprocessed => new Color(255, 228, 225)
    6.20 +        case _ => Color.red
    6.21        }
    6.22    }
    6.23