--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Dec 07 15:39:50 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Dec 07 19:55:01 2008 +0100
@@ -35,17 +35,27 @@
def chooseColor(status : String) : Color = {
//TODO: as properties!
status match {
- case "ident" => new Color(192, 192, 255)
- case "literal" => new Color(192, 255, 255)
- case "fixed_decl" => new Color(192, 192, 192)
- case "prop" => new Color(255, 192 ,255)
- case "typ" => new Color(192, 192, 128)
- case "term" => new Color(192, 128, 192)
- case "method" => new Color(128, 192, 192)
- case "doc_source" => new Color(128, 128, 192)
- case "ML_source" => new Color(128, 192, 128)
- case "local_fact_decl" => new Color(192, 128, 128)
- case _ => Color.red
+ //outer
+ case "ident" | "command" | "keyword" => Color.blue
+ case "verbatim"=> Color.green
+ case "comment" => Color.gray
+ case "control" => Color.white
+ case "malformed" => Color.red
+ case "string" | "altstring" => Color.orange
+ //logical
+ case "tclass" | "tycon" | "fixed_decl" | "fixed"
+ | "const_decl" | "const" | "fact_decl" | "fact"
+ |"dynamic_fact" |"local_fact_decl" | "local_fact"
+ => new Color(255, 0, 255)
+ //inner syntax
+ case "tfree" | "free" => Color.blue
+ case "tvar" | "skolem" | "bound" | "var" => Color.green
+ case "num" | "xnum" | "xstr" | "literal" | "inner_comment" => new Color(255, 128, 128)
+ case "sort" | "typ" | "term" | "prop" | "attribute" | "method" => Color.yellow
+ // embedded source
+ case "doc_source" | "ML_source" | "ML_antic" | "doc_antiq" | "antiq"
+ => new Color(0, 192, 0)
+ case _ => Color.white
}
}
def withView(view : TextArea, f : (TheoryView) => Unit) {
@@ -164,7 +174,7 @@
textArea.getLastPhysicalLine)
}
- def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color){
+ def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color, fill : Boolean){
val fm = textArea.getPainter.getFontMetrics
val startP = textArea.offsetToXY(begin)
val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish)
@@ -174,7 +184,8 @@
if (startP != null && stopP != null) {
gfx.setColor(color)
- gfx.fillRect(startP.x, y, stopP.x - startP.x, height)
+ if(fill){gfx.fillRect(startP.x, y, stopP.x - startP.x, height)}
+ else {gfx.drawRect(startP.x, y, stopP.x - startP.x, height)}
}
}
@@ -189,15 +200,16 @@
while (e != null && toCurrent(e.start) < end) {
val begin = start max toCurrent(e.start)
val finish = end - 1 min toCurrent(e.stop)
- encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e))
+ encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e), true)
// paint details of command
- var dy = 0
- for(status <- e.statuses){
- dy += 1
- val begin = toCurrent(status.start + e.start)
- val finish = toCurrent(status.stop + e.start)
+ var nodes = e.root_node.breadthFirstEnumeration
+ while(nodes.hasMoreElements){
+ val node = nodes.nextElement.asInstanceOf[javax.swing.tree.DefaultMutableTreeNode]
+ val node_asset = node.getUserObject.asInstanceOf[isabelle.prover.RelativeAsset]
+ val begin = toCurrent(node_asset.rel_start + e.start)
+ val finish = toCurrent(node_asset.rel_end + e.start)
if(finish > start && begin < end)
- encolor(gfx, y + dy, fm.getHeight - dy, begin max start, finish min end, chooseColor(status.kind))
+ encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node_asset.getShortDescription), true)
}
e = e.next
}
--- a/src/Tools/jEdit/src/prover/Command.scala Sun Dec 07 15:39:50 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Sun Dec 07 19:55:01 2008 +0100
@@ -38,15 +38,23 @@
}
val id : Long = generateId
- var phase = Phase.UNPROCESSED
+
+ private var p = Phase.UNPROCESSED
+ def phase = p
+ def phase_=(p_new : Phase.Value) = {
+ if(p_new == Phase.UNPROCESSED){
+ //delete inner syntax
+ val children = root_node.children
+ while (children.hasMoreElements){
+ val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode]
+ child.removeAllChildren
+ }
+ }
+ p = p_new
+ }
var results = Nil : List[XML.Tree]
- //offsets relative to first.start!
- class Status(val kind : String,val start : Int, val stop : Int ) { }
- var statuses = Nil : List[Status]
- 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 results_xml = XML.document(results match {
case Nil => XML.Elem("message", List(), List())
@@ -61,7 +69,7 @@
val root_node = {
val content = document.getContent(this)
- val ra = new RelativeAsset(this, 0, stop - start, "command", content)
+ val ra = new RelativeAsset(this, 0, stop - start, "Command", content)
new DefaultMutableTreeNode(ra)
}
@@ -76,7 +84,7 @@
return c_start >= n_start && c_end <= n_end
}
- def insert_node(new_node : DefaultMutableTreeNode, node : DefaultMutableTreeNode) {
+ private def insert_node(new_node : DefaultMutableTreeNode, node : DefaultMutableTreeNode) {
assert(fitting(new_node, node))
val children = node.children
while (children.hasMoreElements){
@@ -97,40 +105,13 @@
}
}
- def addStatus(tree : XML.Tree) {
- val (state, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
- case _ => null}
- 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 add_node(node : DefaultMutableTreeNode) = insert_node(node, root_node)
+
+ def node_from(kind : String, begin : Int, end : Int) : DefaultMutableTreeNode = {
+ val markup_content = /*content.substring(begin, end)*/
+ ""
+ val asset = new RelativeAsset(this, begin, end, kind, markup_content)
+ new DefaultMutableTreeNode(asset)
}
def content = document.getContent(this)
--- a/src/Tools/jEdit/src/prover/Document.scala Sun Dec 07 15:39:50 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala Sun Dec 07 19:55:01 2008 +0100
@@ -14,7 +14,7 @@
{
val structuralChanges = new EventSource[Document.StructureChange]()
- def isStartKeyword(s : String) = prover.commandKeywords.contains(s)
+ def isStartKeyword(s : String) = prover.command_decls.contains(s)
def commands() = new Iterator[Command] {
var current = firstToken
--- a/src/Tools/jEdit/src/prover/Prover.scala Sun Dec 07 15:39:50 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sun Dec 07 19:55:01 2008 +0100
@@ -24,7 +24,8 @@
private var process = null : IsabelleProcess
private var commands = new HashMap[String, Command]
- val commandKeywords = new HashSet[String]
+ val command_decls = new HashSet[String]
+ val keyword_decls = new HashSet[String]
private var initialized = false
val activated = new EventSource[Unit]
@@ -32,7 +33,10 @@
val outputInfo = new EventSource[String]
val allInfo = new EventSource[Result]
var document = null : Document
-
+
+ def fireChange(c : Command) =
+ inUIThread(() => commandInfo.fire(new CommandChangeInfo(c)))
+
var workerThread = new Thread("isabelle.Prover: worker") {
override def run() : Unit = {
while (true) {
@@ -58,16 +62,43 @@
else {
val tree = parse_failsafe(converter.decode(r.result))
tree match {
- case Elem("message", List(("class","status")), decls) =>
- decls map (decl => decl match{
+ //handle all kinds of status messages here
+ case Elem("message", List(("class","status")), elems) =>
+ elems map (elem => elem match{
+ // catch command_start and keyword declarations
case Elem("command_decl", List(("name", name), ("kind", _)), _) =>
- commandKeywords.addEntry(name)
- case Elem("keyword_decl", List(("name", keyw)), _) =>
- () //TODO: with these keywords simplify the token-regex in ProofDocument
- case _ =>
- //TODO: can there be other decls?
- if (st != null)
- handleResult(st, r, tree)
+ command_decls.addEntry(name)
+ case Elem("keyword_decl", List(("name", name)), _) =>
+ keyword_decls.addEntry(name)
+ // expecting markups here
+ case Elem(kind, List(("offset", offset),
+ ("end_offset", end_offset),
+ ("id", id)), List()) =>
+ val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
+ val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1
+
+ val command =
+ // outer syntax: no id in props
+ if(st == null) commands.getOrElse(id, null)
+ // inner syntax: id from props
+ else st
+ command.add_node(command.node_from(kind, begin, end))
+ // Phase changed
+ case Elem("finished", _, _) =>
+ st.phase = Phase.FINISHED
+ fireChange(st)
+ case Elem("unprocessed", _, _) =>
+ st.phase = Phase.UNPROCESSED
+ fireChange(st)
+ case Elem("failed", _, _) =>
+ st.phase = Phase.FAILED
+ fireChange(st)
+ case Elem("removed", _, _) =>
+ // TODO: never lose information on command + id ??
+ //document.prover.commands.removeKey(st.idString)
+ st.phase = Phase.REMOVED
+ fireChange(st)
+ case _ =>
})
case _ =>
//TODO
@@ -81,8 +112,7 @@
}
def handleResult(st : Command, r : Result, tree : XML.Tree) {
- def fireChange() =
- inUIThread(() => commandInfo.fire(new CommandChangeInfo(st)))
+ //TODO: this is just for testing
allInfo.fire(r)
r.kind match {
@@ -90,23 +120,23 @@
if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
st.phase = Phase.FAILED
st.addResult(tree)
- fireChange()
+ fireChange(st)
case IsabelleProcess.Kind.WRITELN =>
st.addResult(tree)
- fireChange()
+ fireChange(st)
case IsabelleProcess.Kind.PRIORITY =>
st.addResult(tree)
- fireChange()
+ fireChange(st)
case IsabelleProcess.Kind.WARNING =>
st.addResult(tree)
- fireChange()
+ fireChange(st)
case IsabelleProcess.Kind.STATUS =>
- st.addStatus(tree)
- fireChange()
+ System.err.println("handleResult - Ignored: " + tree)
+
case _ =>
}
}
@@ -126,7 +156,7 @@
private def inUIThread(runnable : () => Unit) {
SwingUtilities invokeAndWait new Runnable() {
- override def run() { runnable() }
+ override def run() { runnable () }
}
}