# HG changeset patch
# User immler@in.tum.de
# Date 1228069139 -3600
# Node ID f0e1608a774f42969bf06bed4ea519c574f9b81b
# Parent  a02d46bca7e4eb0ad2fe2c0e1b9c4550f8160006
basic tree structure for sidekick

diff -r a02d46bca7e4 -r f0e1608a774f src/Tools/jEdit/nbproject/project.properties
--- 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
diff -r a02d46bca7e4 -r f0e1608a774f src/Tools/jEdit/plugin/IsabellePlugin.props
--- 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
diff -r a02d46bca7e4 -r f0e1608a774f src/Tools/jEdit/plugin/services.xml
--- 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>
diff -r a02d46bca7e4 -r f0e1608a774f src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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
diff -r a02d46bca7e4 -r f0e1608a774f src/Tools/jEdit/src/prover/Command.scala
--- 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)
     }
   }
 
diff -r a02d46bca7e4 -r f0e1608a774f src/Tools/jEdit/src/prover/IsabelleSKParser.scala
--- /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
+      }
+    }
+
+}
diff -r a02d46bca7e4 -r f0e1608a774f src/Tools/jEdit/src/prover/RelativeAsset.scala
--- /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)
+
+}