--- a/src/Tools/jEdit/src/prover/Command.scala Sun Dec 28 20:31:13 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Sun Dec 28 20:35:34 2008 +0100
@@ -7,13 +7,17 @@
package isabelle.prover
-import isabelle.proofdocument.Token
-import isabelle.jedit.Plugin
-import isabelle.{ YXML, XML }
-import sidekick.{SideKickParsedData, IAsset}
+
import javax.swing.text.Position
import javax.swing.tree.DefaultMutableTreeNode
+import isabelle.proofdocument.Token
+import isabelle.jedit.{Isabelle, Plugin}
+import isabelle.{YXML, XML}
+
+import sidekick.{SideKickParsedData, IAsset}
+
+
object Command {
object Phase extends Enumeration {
val UNPROCESSED = Value("UNPROCESSED")
@@ -22,76 +26,78 @@
val REMOVED = Value("REMOVED")
val FAILED = Value("FAILED")
}
-
- private var nextId : Long = 0
- def generateId : Long = {
- nextId = nextId + 1
- return nextId
- }
-
- def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
}
-class Command(val document : Document, val first : Token[Command], val last : Token[Command]) {
- import Command._
+
+class Command(val document: Document, val first: Token[Command], val last: Token[Command])
+{
+ val id = Isabelle.plugin.id()
{
var t = first
- while(t != null) {
+ while (t != null) {
t.command = this
t = if (t == last) null else t.next
}
}
-
- val id : Long = generateId
+
- private var p = Phase.UNPROCESSED
+ /* command phase */
+
+ private var p = Command.Phase.UNPROCESSED
def phase = p
- def phase_=(p_new : Phase.Value) = {
- if(p_new == Phase.UNPROCESSED){
- //delete inner syntax
- for(child <- root_node.children){
+ def phase_=(p_new: Command.Phase.Value) = {
+ if (p_new == Command.Phase.UNPROCESSED) {
+ // delete markup
+ for (child <- root_node.children) {
child.children = Nil
}
}
p = p_new
}
-
- var results = Nil : List[XML.Tree]
+
- def idString = java.lang.Long.toString(id, 36)
+ /* accumulated results */
+
+ var results: List[XML.Tree] = Nil
+
def results_xml = XML.document(
results match {
case Nil => XML.Elem("message", Nil, Nil)
case List(elem) => elem
- case _ =>
- XML.Elem("messages", List(), List(results.first, results.last))
+ case _ => XML.Elem("messages", Nil, List(results.first, results.last))
}, "style")
- def addResult(tree : XML.Tree) {
+ def add_result(tree: XML.Tree) {
results = results ::: List(tree) // FIXME canonical reverse order
}
-
- val root_node =
- new MarkupNode(this, 0, stop - start, idString, "Command", document.getContent(this))
+
- def node_from(kind : String, begin : Int, end : Int) : MarkupNode = {
- val markup_content = /*content.substring(begin, end)*/ ""
- new MarkupNode(this, begin, end, idString, kind, markup_content)
- }
+ /* content */
- def content = document.getContent(this)
+ def content(): String = 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
- def start = first start
- def stop = last stop
-
- def properStart = start
- def properStop = {
+ def start = first.start
+ def stop = last.stop
+
+ def proper_start = start
+ def proper_stop = {
var i = last
while (i != first && i.kind.equals(Token.Kind.COMMENT))
i = i.previous
i.stop
- }
-}
\ No newline at end of file
+ }
+
+
+ /* markup tree */
+
+ val root_node =
+ new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content())
+
+ def node_from(kind: String, begin: Int, end: Int) = {
+ val markup_content = /*content.substring(begin, end)*/ ""
+ new MarkupNode(this, begin, end, id, kind, markup_content)
+ }
+}
--- a/src/Tools/jEdit/src/prover/Document.scala Sun Dec 28 20:31:13 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala Sun Dec 28 20:35:34 2008 +0100
@@ -33,7 +33,7 @@
}
}
- def getContent(cmd : Command) = text.content(cmd.properStart, cmd.properStop)
+ def getContent(cmd : Command) = text.content(cmd.proper_start, cmd.proper_stop)
def getNextCommandContaining(pos : Int) : Command = {
for( cmd <- commands()) { if (pos < cmd.stop) return cmd }
--- a/src/Tools/jEdit/src/prover/Prover.scala Sun Dec 28 20:31:13 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sun Dec 28 20:35:34 2008 +0100
@@ -111,7 +111,7 @@
st.phase = Phase.FAILED
fireChange(st)
case Elem("removed", _, _) =>
- document.prover.commands.removeKey(st.idString)
+ document.prover.commands.removeKey(st.id)
st.phase = Phase.REMOVED
fireChange(st)
case _ =>
@@ -134,19 +134,19 @@
case IsabelleProcess.Kind.ERROR =>
if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
st.phase = Phase.FAILED
- st.addResult(tree)
+ st.add_result(tree)
fireChange(st)
case IsabelleProcess.Kind.WRITELN =>
- st.addResult(tree)
+ st.add_result(tree)
fireChange(st)
case IsabelleProcess.Kind.PRIORITY =>
- st.addResult(tree)
+ st.add_result(tree)
fireChange(st)
case IsabelleProcess.Kind.WARNING =>
- st.addResult(tree)
+ st.add_result(tree)
fireChange(st)
case IsabelleProcess.Kind.STATUS =>
@@ -184,11 +184,11 @@
}
private def send(cmd : Command) {
- commands.put(cmd.idString, cmd)
+ commands.put(cmd.id, cmd)
- val props = new Properties()
- props.setProperty("id", cmd.idString)
- props.setProperty("offset", Integer.toString(1))
+ val props = new Properties
+ props.setProperty("id", cmd.id)
+ props.setProperty("offset", "1")
val content = isabelle_symbols.encode(document.getContent(cmd))
process.output_sync("Isar.command "
@@ -198,15 +198,15 @@
process.output_sync("Isar.insert "
+ encode_string(if (cmd.previous == null) ""
- else cmd.previous.idString)
+ else cmd.previous.id)
+ " "
- + encode_string(cmd.idString))
+ + encode_string(cmd.id))
cmd.phase = Phase.UNPROCESSED
}
def remove(cmd : Command) {
cmd.phase = Phase.REMOVE
- process.output_sync("Isar.remove " + encode_string(cmd.idString))
+ process.output_sync("Isar.remove " + encode_string(cmd.id))
}
}
\ No newline at end of file