# HG changeset patch # User immler@in.tum.de # Date 1228676101 -3600 # Node ID 5b8b89b7e5974a5328f58d1693086e0a335c5054 # Parent 2d40e4067c37bf9274c68439676726acb1ee29e7 interpretation of STATUS messages in one place, deleting inner syntax diff -r 2d40e4067c37 -r 5b8b89b7e597 src/Tools/jEdit/src/jedit/TheoryView.scala --- 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 } diff -r 2d40e4067c37 -r 5b8b89b7e597 src/Tools/jEdit/src/prover/Command.scala --- 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) diff -r 2d40e4067c37 -r 5b8b89b7e597 src/Tools/jEdit/src/prover/Document.scala --- 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 diff -r 2d40e4067c37 -r 5b8b89b7e597 src/Tools/jEdit/src/prover/Prover.scala --- 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 () } } }