# HG changeset patch
# User wenzelm
# Date 1230580915 -3600
# Node ID e2aa32bb73c0e3e39a90db7325b124e379c7c623
# Parent  19bd801975a3dfd826531d5e96823906a19bf430
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);

diff -r 19bd801975a3 -r e2aa32bb73c0 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Dec 29 20:50:38 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Dec 29 21:01:55 2008 +0100
@@ -1,5 +1,5 @@
 /*
- * Information on command-phase left of scrollbar (with panel)
+ * Information on command status left of scrollbar (with panel)
  *
  * @author Fabian Immler, TU Munich
  */
@@ -63,10 +63,10 @@
       val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
       val y = lineToY(line1)
       val height = lineToY(line2) - y - 1
-      val (light, dark) = command.phase match {
-        case Command.Phase.UNPROCESSED => (Color.yellow, new Color(128,128,0))
-        case Command.Phase.FINISHED => (Color.green, new Color(0, 128, 0))
-        case Command.Phase.FAILED => (Color.red, new Color(128,0,0))
+      val (light, dark) = command.status match {
+        case Command.Status.UNPROCESSED => (Color.yellow, new Color(128,128,0))
+        case Command.Status.FINISHED => (Color.green, new Color(0, 128, 0))
+        case Command.Status.FAILED => (Color.red, new Color(128,0,0))
       }
 
       gfx.setColor(light)
diff -r 19bd801975a3 -r e2aa32bb73c0 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Dec 29 20:50:38 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Dec 29 21:01:55 2008 +0100
@@ -11,7 +11,6 @@
 
 import isabelle.proofdocument.Text
 import isabelle.prover.{Prover, Command}
-import isabelle.prover.Command.Phase
 
 import java.awt.Graphics2D
 import java.awt.event.{ActionEvent, ActionListener}
@@ -29,10 +28,10 @@
   def choose_color(state: Command): Color = {
     if (state == null) Color.red
     else
-      state.phase match {
-        case Phase.UNPROCESSED => new Color(255, 228, 225)
-        case Phase.FINISHED => new Color(234, 248, 255)
-        case Phase.FAILED => new Color(255, 192, 192)
+      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, 192, 192)
         case _ => Color.red
       }
   }
@@ -148,8 +147,8 @@
 
   def repaint(cmd: Command) =
   {
-    val phase = cmd.phase
-    if (text_area != null && phase != Phase.REMOVE && phase != Phase.REMOVED) {
+    val status = cmd.status
+    if (text_area != null && status != Command.Status.REMOVE && status != Command.Status.REMOVED) {
       val start = text_area.getLineOfOffset(to_current(cmd.start))
       val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
       text_area.invalidateLineRange(start, stop)
diff -r 19bd801975a3 -r e2aa32bb73c0 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Dec 29 20:50:38 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Mon Dec 29 21:01:55 2008 +0100
@@ -19,7 +19,7 @@
 
 
 object Command {
-  object Phase extends Enumeration {
+  object Status extends Enumeration {
     val UNPROCESSED = Value("UNPROCESSED")
     val FINISHED = Value("FINISHED")
     val REMOVE = Value("REMOVE")
@@ -42,18 +42,18 @@
   }
 
 
-  /* command phase */
+  /* command status */
 
-  private var p = Command.Phase.UNPROCESSED
-  def phase = p
-  def phase_=(p_new: Command.Phase.Value) = {
-    if (p_new == Command.Phase.UNPROCESSED) {
+  private var _status = Command.Status.UNPROCESSED
+  def status = _status
+  def status_=(st: Command.Status.Value) = {
+    if (st == Command.Status.UNPROCESSED) {
       // delete markup
       for (child <- root_node.children) {
         child.children = Nil
       }
     }
-    p = p_new
+    _status = st
   }
 
 
diff -r 19bd801975a3 -r e2aa32bb73c0 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Dec 29 20:50:38 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Dec 29 21:01:55 2008 +0100
@@ -53,7 +53,7 @@
     }
     else {
       val tree = YXML.parse_failsafe(isabelle_symbols.decode(r.result))
-      if (st == null || (st.phase != Command.Phase.REMOVED && st.phase != Command.Phase.REMOVE)) {
+      if (st == null || (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)) {
         r.kind match {
 
           case IsabelleProcess.Kind.STATUS =>
@@ -65,17 +65,17 @@
                     //{{{
                     // command status
                     case XML.Elem(Markup.FINISHED, _, _) =>
-                      st.phase = Command.Phase.FINISHED
+                      st.status = Command.Status.FINISHED
                       command_change(st)
                     case XML.Elem(Markup.UNPROCESSED, _, _) =>
-                      st.phase = Command.Phase.UNPROCESSED
+                      st.status = Command.Status.UNPROCESSED
                       command_change(st)
                     case XML.Elem(Markup.FAILED, _, _) =>
-                      st.phase = Command.Phase.FAILED
+                      st.status = Command.Status.FAILED
                       command_change(st)
                     case XML.Elem(Markup.DISPOSED, _, _) =>
                       document.prover.commands.removeKey(st.id)
-                      st.phase = Command.Phase.REMOVED
+                      st.status = Command.Status.REMOVED
                       command_change(st)
 
                     // command and keyword declarations
@@ -107,8 +107,8 @@
             //}}}
 
           case IsabelleProcess.Kind.ERROR if st != null =>
-            if (st.phase != Command.Phase.REMOVED && st.phase != Command.Phase.REMOVE)
-              st.phase = Command.Phase.FAILED
+            if (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)
+              st.status = Command.Status.FAILED
             st.add_result(tree)
             command_change(st)
 
@@ -153,7 +153,7 @@
   }
 
   private def send(cmd: Command) {
-    cmd.phase = Command.Phase.UNPROCESSED
+    cmd.status = Command.Status.UNPROCESSED
     commands.put(cmd.id, cmd)
 
     val props = new Properties
@@ -166,7 +166,7 @@
   }
 
   def remove(cmd: Command) {
-    cmd.phase = Command.Phase.REMOVE
+    cmd.status = Command.Status.REMOVE
     process.remove_command(cmd.id)
   }
 }