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