--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sun Dec 07 15:01:37 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sun Dec 07 15:36:24 2008 +0100
@@ -40,7 +40,7 @@
if (state == null)
panel.setDocument(null : Document)
else
- panel.setDocument(state.document, UserAgent.baseURL)
+ panel.setDocument(state.results_xml, UserAgent.baseURL)
})
}
}
--- a/src/Tools/jEdit/src/prover/Command.scala Sun Dec 07 15:01:37 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Sun Dec 07 15:36:24 2008 +0100
@@ -26,7 +26,7 @@
def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
}
-class Command(val first : Token[Command], val last : Token[Command]) {
+class Command(val document : Document, val first : Token[Command], val last : Token[Command]) {
import Command._
{
@@ -45,10 +45,10 @@
//offsets relative to first.start!
class Status(val kind : String,val start : Int, val stop : Int ) { }
var statuses = Nil : List[Status]
- def statusesxml = XML.Elem("statuses", List(), statuses.map (s => XML.Text(s.kind + ": " + s.start + "-" + s.stop + "\n")))
+ def statuses_xml = XML.Elem("statuses", List(), statuses.map (s => XML.Text(s.kind + ": " + s.start + "-" + s.stop + "\n")))
def idString = java.lang.Long.toString(id, 36)
- def document = XML.document(results match {
+ def results_xml = XML.document(results match {
case Nil => XML.Elem("message", List(), List())
case List(elem) => elem
case _ =>
@@ -60,7 +60,7 @@
}
val root_node = {
- val content = Plugin.plugin.prover.document.getContent(this)
+ val content = document.getContent(this)
val ra = new RelativeAsset(this, 0, stop - start, "command", content)
new DefaultMutableTreeNode(ra)
}
@@ -99,26 +99,42 @@
}
def addStatus(tree : XML.Tree) {
- val (markup_info, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
+ val (state, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
case _ => null}
-
- //process attributes:
- var markup_begin = -1
- var markup_end = -1
- for((n, a) <- attr) {
- if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - 1
- if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - 1
- }
- if(markup_begin > -1 && markup_end > -1){
- statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
- val markup_content = content.substring(markup_begin, markup_end)
- val asset = new RelativeAsset(this, markup_begin, markup_end, markup_info, markup_content)
- val new_node = new DefaultMutableTreeNode(asset)
- insert_node(new_node, root_node)
+ if (phase != Phase.REMOVED && phase != Phase.REMOVE) {
+ state match {
+ case "finished" =>
+ phase = Phase.FINISHED
+ case "unprocessed" =>
+ phase = Phase.UNPROCESSED
+ case "failed" =>
+ phase = Phase.FAILED
+ case "removed" =>
+ // TODO: never lose information on command + id ??
+ //document.prover.commands.removeKey(st.idString)
+ phase = Phase.REMOVED
+ case _ =>
+ //process attributes:
+ var markup_begin = -1
+ var markup_end = -1
+ for((n, a) <- attr) {
+ if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - 1
+ if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - 1
+ }
+ if(markup_begin > -1 && markup_end > -1){
+ statuses = new Status(state, markup_begin, markup_end) :: statuses
+ val markup_content = content.substring(markup_begin, markup_end)
+ val asset = new RelativeAsset(this, markup_begin, markup_end, state, markup_content)
+ val new_node = new DefaultMutableTreeNode(asset)
+ insert_node(new_node, root_node)
+ } else {
+ System.err.println("addStatus - ignored: " + tree)
+ }
+ }
}
}
- def content = Plugin.plugin.prover.document.getContent(this)
+ def content = document.getContent(this)
def next = if (last.next != null) last.next.command else null
def previous = if (first.previous != null) first.previous.command else null
--- a/src/Tools/jEdit/src/prover/Document.scala Sun Dec 07 15:01:37 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala Sun Dec 07 15:36:24 2008 +0100
@@ -10,7 +10,7 @@
val removedCommands : List[Command])
}
-class Document(text : Text, prover : Prover) extends ProofDocument[Command](text)
+class Document(text : Text, val prover : Prover) extends ProofDocument[Command](text)
{
val structuralChanges = new EventSource[Document.StructureChange]()
@@ -117,7 +117,7 @@
if (scan.kind.equals(Token.Kind.COMMAND_START) && cmdStart != null && !finished) {
if (! overrun) {
- addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
+ addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
cmdStart = scan
cmdStop = scan
}
@@ -140,7 +140,7 @@
}
if (cmdStart != null)
- addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
+ addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
// relink commands
addedCommands = addedCommands.reverse
--- a/src/Tools/jEdit/src/prover/Prover.scala Sun Dec 07 15:01:37 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sun Dec 07 15:36:24 2008 +0100
@@ -106,32 +106,7 @@
case IsabelleProcess.Kind.STATUS =>
st.addStatus(tree)
- val state = tree match { case Elem("message", _,
- Elem (name, _, _) :: _) => name
- case _ => null }
-
- if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE) {
- state match {
- case "finished" =>
- st.phase = Phase.FINISHED
- fireChange()
-
- case "unprocessed" =>
- st.phase = Phase.UNPROCESSED
- fireChange()
-
- case "failed" =>
- st.phase = Phase.FAILED
- fireChange()
-
- case "removed" =>
- commands.removeKey(st.idString)
- st.phase = Phase.REMOVED
- fireChange()
-
- case _ =>
- }
- }
+ fireChange()
case _ =>
}
}