# HG changeset patch
# User wenzelm
# Date 1273345082 -7200
# Node ID dc972354d77cbe476a97ffb90599a2cbf254a6a7
# Parent  275b24cf9c4122bd50b4dcd7485f3192f27e84ef
tuned;

diff -r 275b24cf9c41 -r dc972354d77c src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat May 08 20:14:11 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat May 08 20:58:02 2010 +0200
@@ -29,16 +29,15 @@
 }
 
 
-class Isabelle_Sidekick(name: String,
-    parser: (() => Boolean, SideKickParsedData, Document_Model) => Unit)
-  extends SideKickParser(name)
+abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
 {
   /* parsing */
 
-  @volatile private var stopped = false
-  private def is_stopped(): Boolean = stopped
+  @volatile protected var stopped = false
   override def stop() = { stopped = true }
 
+  def parser(data: SideKickParsedData, model: Document_Model): Unit
+
   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
   {
     import Isabelle_Sidekick.int_to_pos
@@ -52,7 +51,7 @@
 
     Swing_Thread.now { Document_Model(buffer) } match {
       case Some(model) =>
-        parser(is_stopped, data, model)
+        parser(data, model)
         if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
       case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
     }
@@ -89,63 +88,67 @@
 }
 
 
-class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle",
-  ((is_stopped: () => Boolean, data: SideKickParsedData, model: Document_Model) =>
-    {
-      import Isabelle_Sidekick.int_to_pos
+class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
+{
+  def parser(data: SideKickParsedData, model: Document_Model)
+  {
+    import Isabelle_Sidekick.int_to_pos
 
-      val root = data.root
-      val document = model.recent_document()
-      for {
-        (command, command_start) <- document.command_range(0)
-        if command.is_command && !is_stopped()
-      }
-      {
-        val name = command.name
-        val node =
-          new DefaultMutableTreeNode(new IAsset {
-            override def getIcon: Icon = null
-            override def getShortString: String = name
-            override def getLongString: String = name
-            override def getName: String = name
-            override def setName(name: String) = ()
-            override def setStart(start: Position) = ()
-            override def getStart: Position = command_start
-            override def setEnd(end: Position) = ()
-            override def getEnd: Position = command_start + command.length
-            override def toString = name
-          })
-        root.add(node)
-      }
-    }))
+    val root = data.root
+    val document = model.recent_document()
+    for {
+      (command, command_start) <- document.command_range(0)
+      if command.is_command && !is_stopped()
+    }
+    {
+      val name = command.name
+      val node =
+        new DefaultMutableTreeNode(new IAsset {
+          override def getIcon: Icon = null
+          override def getShortString: String = name
+          override def getLongString: String = name
+          override def getName: String = name
+          override def setName(name: String) = ()
+          override def setStart(start: Position) = ()
+          override def getStart: Position = command_start
+          override def setEnd(end: Position) = ()
+          override def getEnd: Position = command_start + command.length
+          override def toString = name
+        })
+      root.add(node)
+    }
+  }
+}
 
 
-class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw",
-  ((is_stopped: () => Boolean, data: SideKickParsedData, model: Document_Model) =>
-    {
-      import Isabelle_Sidekick.int_to_pos
+class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
+{
+  def parser(data: SideKickParsedData, model: Document_Model)
+  {
+    import Isabelle_Sidekick.int_to_pos
 
-      val root = data.root
-      val document = model.recent_document()
-      for ((command, command_start) <- document.command_range(0) if !is_stopped()) {
-        root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
-            {
-              val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
-              val id = command.id
+    val root = data.root
+    val document = model.recent_document()
+    for ((command, command_start) <- document.command_range(0) if !is_stopped()) {
+      root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
+          {
+            val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
+            val id = command.id
 
-              new DefaultMutableTreeNode(new IAsset {
-                override def getIcon: Icon = null
-                override def getShortString: String = content
-                override def getLongString: String = node.info.toString
-                override def getName: String = id
-                override def setName(name: String) = ()
-                override def setStart(start: Position) = ()
-                override def getStart: Position = command_start + node.start
-                override def setEnd(end: Position) = ()
-                override def getEnd: Position = command_start + node.stop
-                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
-              })
-            }))
-      }
-    }))
+            new DefaultMutableTreeNode(new IAsset {
+              override def getIcon: Icon = null
+              override def getShortString: String = content
+              override def getLongString: String = node.info.toString
+              override def getName: String = id
+              override def setName(name: String) = ()
+              override def setStart(start: Position) = ()
+              override def getStart: Position = command_start + node.start
+              override def setEnd(end: Position) = ()
+              override def getEnd: Position = command_start + node.stop
+              override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
+            })
+          }))
+    }
+  }
+}