--- 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
}