--- a/src/Tools/jEdit/nbproject/project.properties Sat Nov 29 19:31:09 2008 +0100
+++ b/src/Tools/jEdit/nbproject/project.properties Sun Nov 30 19:18:59 2008 +0100
@@ -32,7 +32,9 @@
javac.classpath=\
${libs.Flying-Saucer.classpath}:\
${reference.jEdit.build}:\
- ${libs.Isabelle-Pure.classpath}
+ ${libs.Isabelle-Pure.classpath}:\
+ ${libs.Sidekick.classpath}:\
+ ${libs.ErrorList.classpath}
# Space-separated list of extra javac options
javac.compilerargs=
javac.deprecation=false
--- a/src/Tools/jEdit/plugin/IsabellePlugin.props Sat Nov 29 19:31:09 2008 +0100
+++ b/src/Tools/jEdit/plugin/IsabellePlugin.props Sun Nov 30 19:18:59 2008 +0100
@@ -24,3 +24,6 @@
options.isabelle.font-size.title=Font Size
options.isabelle.font-size=14
+plugin.isabelle.jedit.Plugin.depend.1=plugin sidekick.SideKickPlugin 0.7.6
+sidekick.parser.isabelle.label=Isabelle
+mode.text.sidekick.parser=isabelle
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/services.xml Sat Nov 29 19:31:09 2008 +0100
+++ b/src/Tools/jEdit/plugin/services.xml Sun Nov 30 19:18:59 2008 +0100
@@ -1,6 +1,9 @@
<?xml version="1.0"?>
<!DOCTYPE SERVICES SYSTEM "services.dtd">
<SERVICES>
+ <SERVICE CLASS="sidekick.SideKickParser" NAME="isabelle">
+ new isabelle.prover.IsabelleSKParser();
+ </SERVICE>
<SERVICE NAME="isabelle" CLASS="org.gjt.sp.jedit.io.VFS">
new isabelle.jedit.VFS();
</SERVICE>
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sat Nov 29 19:31:09 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Nov 30 19:18:59 2008 +0100
@@ -66,7 +66,7 @@
}
}
-class TheoryView(prover : Prover, buffer : JEditBuffer)
+class TheoryView(prover : Prover, val buffer : JEditBuffer)
extends TextAreaExtension with Text with BufferListener {
import TheoryView._
import Text.Changed
--- a/src/Tools/jEdit/src/prover/Command.scala Sat Nov 29 19:31:09 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Sun Nov 30 19:18:59 2008 +0100
@@ -1,7 +1,12 @@
package isabelle.prover
import isabelle.proofdocument.Token
+import isabelle.jedit.Plugin
import isabelle.{ YXML, XML }
+import sidekick.{SideKickParsedData}
+import sidekick.enhanced.SourceAsset
+import javax.swing.text.Position
+import javax.swing.tree.DefaultMutableTreeNode
object Command {
object Phase extends Enumeration {
@@ -53,8 +58,47 @@
def addResult(tree : XML.Tree) {
results = results ::: List(tree)
}
+
+ val root_node = {
+ val content = Plugin.plugin.prover.document.getContent(this)
+ val ra = new RelativeAsset(this, 0, stop - start, "command", content)
+ System.err.println(start + "-" + stop + ": " + content)
+ new DefaultMutableTreeNode(ra)
+ }
- def addStatus(tree : XML.Tree) {
+ // does cand fit into node?
+ private def fitting(cand : DefaultMutableTreeNode, node : DefaultMutableTreeNode) : boolean = {
+ val node_asset = node.getUserObject.asInstanceOf[RelativeAsset]
+ val n_start = node_asset.rel_start
+ val n_end = node_asset.rel_end
+ val cand_asset = cand.getUserObject.asInstanceOf[RelativeAsset]
+ val c_start = cand_asset.rel_start
+ val c_end = cand_asset.rel_end
+ return c_start >= n_start && c_end <= n_end
+ }
+
+ def insert_node(new_node : DefaultMutableTreeNode, node : DefaultMutableTreeNode) {
+ assert(fitting(new_node, node))
+ val children = node.children
+ while (children.hasMoreElements){
+ val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode]
+ if(fitting(new_node, child)) {
+ insert_node(new_node, child)
+ }
+ }
+ if(new_node.getParent == null){
+ while(children.hasMoreElements){
+ val child = children.nextElement.asInstanceOf[DefaultMutableTreeNode]
+ if(fitting(child, new_node)) {
+ node.remove(child.asInstanceOf[DefaultMutableTreeNode])
+ new_node.add(child)
+ }
+ }
+ node.add(new_node)
+ }
+ }
+
+ def addStatus(tree : XML.Tree) {
val (markup_info, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
case _ => null}
@@ -66,7 +110,11 @@
if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
}
if(markup_begin > -1 && markup_end > -1){
- statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
+ statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
+ val content = Plugin.plugin.prover.document.getContent(this).substring(markup_begin, markup_end)
+ val asset = new RelativeAsset(this, markup_begin, markup_end, markup_info, content)
+ val new_node = new DefaultMutableTreeNode(asset)
+ insert_node(new_node, root_node)
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/prover/IsabelleSKParser.scala Sun Nov 30 19:18:59 2008 +0100
@@ -0,0 +1,42 @@
+/*
+ * IsabelleSKParser.scala
+ *
+ * To change this template, choose Tools | Template Manager
+ * and open the template in the editor.
+ */
+
+package isabelle.prover
+
+import isabelle.jedit.Plugin
+import sidekick.{SideKickParser, SideKickParsedData, IAsset}
+import org.gjt.sp.jedit.Buffer
+import javax.swing.tree.DefaultMutableTreeNode
+import errorlist.DefaultErrorSource;
+
+class IsabelleSKParser() extends SideKickParser("isabelle") {
+
+ override def parse(b : Buffer,
+ errorSource : DefaultErrorSource)
+ : SideKickParsedData = {
+ if(Plugin.plugin == null || Plugin.plugin.theoryView == null
+ || Plugin.plugin.theoryView.buffer == null
+ || !Plugin.plugin.theoryView.buffer.equals(b))
+ {
+ val data = new SideKickParsedData("WARNING:")
+ data.root.add(new DefaultMutableTreeNode("can only parse buffer which is activated via IsabellePlugin -> activate"))
+ data
+ } else{
+ val plugin = Plugin.plugin
+ val prover = plugin.prover
+ val buffer = Plugin.plugin.theoryView.buffer.asInstanceOf[Buffer]
+ val document = prover.document
+ val data = new SideKickParsedData(buffer.getPath)
+ //TODO: catch npe s
+ for(command <- document.commands){
+ data.root.add(command.root_node)
+ }
+ data
+ }
+ }
+
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/prover/RelativeAsset.scala Sun Nov 30 19:18:59 2008 +0100
@@ -0,0 +1,48 @@
+/*
+ * RelativeAsset.scala
+ *
+ * To change this template, choose Tools | Template Manager
+ * and open the template in the editor.
+ */
+
+package isabelle.prover
+
+import sidekick.enhanced.SourceAsset
+import javax.swing._
+import javax.swing.text.Position
+
+class RelativeAsset(base : Command, var rel_start : Int, var rel_end : Int, cons_name : String, desc : String)
+ extends SourceAsset {
+
+class MyPos(val o : Int) extends Position {
+ override def getOffset = o
+}
+ {
+ setStart(new MyPos(base.start + rel_start))
+ setEnd(new MyPos(base.start + rel_end))
+ setName(cons_name)
+ setShort(cons_name)
+ setLong(desc)
+
+ }
+ /**
+ * Set the start position
+ */
+ override def setStart(start : Position) { rel_start = start.getOffset - base.start }
+
+ /**
+ * Returns the starting position.
+ */
+ override def getStart : Position = new MyPos(base.start + rel_start)
+
+ /**
+ * Set the end position
+ */
+ override def setEnd(end : Position) { rel_end = end.getOffset - base.start }
+
+ /**
+ * Returns the end position.
+ */
+ override def getEnd : Position = new MyPos(base.start + rel_end)
+
+}