# HG changeset patch
# User wenzelm
# Date 1251992882 -7200
# Node ID 80b0add08eef9c5f1ef01be37acd993b45815bfe
# Parent  0e1d098940a7b2a19146ebad2f7b94b1ac8ff4b0
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
tuned;

diff -r 0e1d098940a7 -r 80b0add08eef src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Thu Sep 03 17:26:25 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Thu Sep 03 17:48:02 2009 +0200
@@ -11,10 +11,15 @@
 import scala.collection.immutable.TreeSet
 
 import javax.swing.tree.DefaultMutableTreeNode
+import javax.swing.text.Position
+import javax.swing.Icon
 
 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
 import errorlist.DefaultErrorSource
-import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
+import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
+
+import isabelle.prover.{Command, MarkupNode}
+import isabelle.proofdocument.ProofDocument
 
 
 class IsabelleSideKickParser extends SideKickParser("isabelle")
@@ -33,9 +38,28 @@
     val prover_setup = Isabelle.prover_setup(buffer)
     if (prover_setup.isDefined) {
       val document = prover_setup.get.theory_view.current_document()
-      for (command <- document.commands)
-        data.root.add(command.markup_root(document).swing_node(document))
+      for (command <- document.commands if !stopped) {
+        data.root.add(command.markup_root(document).
+          swing_tree(document)((node: MarkupNode, cmd: Command, doc: ProofDocument) =>
+            {
+              implicit def int2pos(offset: Int): Position =
+                new Position { def getOffset = offset; override def toString = offset.toString }
 
+              new DefaultMutableTreeNode(new IAsset {
+                override def getIcon: Icon = null
+                override def getShortString: String = node.content
+                override def getLongString: String = node.info.toString
+                override def getName: String = node.id
+                override def setName(name: String) = ()
+                override def setStart(start: Position) = ()
+                override def getStart: Position = node.abs_start(doc)
+                override def setEnd(end: Position) = ()
+                override def getEnd: Position = node.abs_stop(doc)
+                override def toString =
+                  node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
+              })
+            }))
+      }
       if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
     }
     else data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
diff -r 0e1d098940a7 -r 80b0add08eef src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Thu Sep 03 17:26:25 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Thu Sep 03 17:48:02 2009 +0200
@@ -6,12 +6,11 @@
 
 package isabelle.prover
 
+
+import javax.swing.tree.DefaultMutableTreeNode
+
 import isabelle.proofdocument.ProofDocument
 
-import sidekick.IAsset
-import javax.swing._
-import javax.swing.text.Position
-import javax.swing.tree._
 
 abstract class MarkupInfo
 case class RootInfo() extends MarkupInfo
@@ -24,49 +23,28 @@
     override def toString = (file, line, command_id, offset).toString
   }
 
-object MarkupNode {
-
-  def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument)
-      : DefaultMutableTreeNode = {
-
-    implicit def int2pos(offset: Int): Position =
-      new Position { def getOffset = offset; override def toString = offset.toString }
-
-    object RelativeAsset extends IAsset {
-      override def getIcon: Icon = null
-      override def getShortString: String = node.content
-      override def getLongString: String = node.info.toString
-      override def getName: String = node.id
-      override def setName(name: String) = ()
-      override def setStart(start: Position) = ()
-      override def getStart: Position = node.abs_start(doc)
-      override def setEnd(end: Position) = ()
-      override def getEnd: Position = node.abs_stop(doc)
-      override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
-    }
-
-    new DefaultMutableTreeNode(RelativeAsset)
-  }
-}
 
 class MarkupNode(val base: Command, val start: Int, val stop: Int,
   val children: List[MarkupNode],
   val id: String, val content: String, val info: MarkupInfo)
 {
 
-  def swing_node(doc: ProofDocument): DefaultMutableTreeNode = {
-    val node = MarkupNode.markup2default_node (this, base, doc)
-    children.map(node add _.swing_node(doc))
+  def swing_tree(doc: ProofDocument)
+    (make_node: (MarkupNode, Command, ProofDocument) => DefaultMutableTreeNode):
+      DefaultMutableTreeNode =
+  {
+    val node = make_node(this, base, doc)
+    children.foreach(node add _.swing_tree(doc)(make_node))
     node
   }
 
   def abs_start(doc: ProofDocument) = base.start(doc) + start
   def abs_stop(doc: ProofDocument) = base.start(doc) + stop
 
-  def set_children(newchildren: List[MarkupNode]): MarkupNode =
-    new MarkupNode(base, start, stop, newchildren, id, content, info)
+  def set_children(new_children: List[MarkupNode]): MarkupNode =
+    new MarkupNode(base, start, stop, new_children, id, content, info)
 
-  private def add(child: MarkupNode) =
+  private def add(child: MarkupNode) =   // FIXME avoid sort?
     set_children ((child :: children) sort ((a, b) => a.start < b.start))
 
   def remove(nodes: List[MarkupNode]) = set_children(children diff nodes)
@@ -79,7 +57,8 @@
     all
   }
 
-  def leafs: List[MarkupNode] = {
+  def leafs: List[MarkupNode] =
+  {
     if (children == Nil) return List(this)
     else return children flatMap (_.leafs)
   }
@@ -103,13 +82,15 @@
     }
   }
 
-  def filter(p: MarkupNode => Boolean): List[MarkupNode] = {
+  def filter(p: MarkupNode => Boolean): List[MarkupNode] =
+  {
     val filtered = children.flatMap(_.filter(p))
     if (p(this)) List(this set_children(filtered))
     else filtered
   }
 
-  def +(new_child: MarkupNode): MarkupNode = {
+  def + (new_child: MarkupNode): MarkupNode =
+  {
     if (new_child fitting_into this) {
       var inserted = false
       val new_children =
@@ -123,7 +104,8 @@
         (this remove fitting) add ((new_child /: fitting) (_ + _))
       }
       else this set_children new_children
-    } else {
+    }
+    else {
       System.err.println("ignored nonfitting markup: " + new_child)
       this
     }