# HG changeset patch
# User wenzelm
# Date 1344368304 -7200
# Node ID 622251b2b0f1d04d3e323bf5d0b07885dabf0fed
# Parent  de26cf3191a3ad921d8ffa0cbd7af2d3ac344d76
clarified Sidekick configuration, including minor modes;

diff -r de26cf3191a3 -r 622251b2b0f1 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Tue Aug 07 20:28:35 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Tue Aug 07 21:38:24 2012 +0200
@@ -67,9 +67,15 @@
 isabelle-syslog.title=Syslog
 
 #SideKick
+mode.isabelle.sidekick.showStatusWindow.label=true
 sidekick.parser.isabelle.label=Isabelle
 mode.isabelle.sidekick.parser=isabelle
+mode.isabelle-options.sidekick.parser=isabelle-options
+mode.isabelle-root.sidekick.parser=isabelle-root
 mode.ml.sidekick.parser=isabelle
 
+mode.isabelle.customSettings=true
+mode.isabelle.folding=sidekick
+
 #Hyperlinks
 mode.isabelle.hyperlink.source=isabelle
diff -r de26cf3191a3 -r 622251b2b0f1 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 07 20:28:35 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 07 21:38:24 2012 +0200
@@ -48,14 +48,15 @@
 }
 
 
-abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
+class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
+  extends SideKickParser(name)
 {
   /* parsing */
 
   @volatile protected var stopped = false
   override def stop() = { stopped = true }
 
-  def parser(data: SideKickParsedData, model: Document_Model): Unit
+  def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
 
   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
   {
@@ -66,12 +67,16 @@
     val root = data.root
     data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
 
-    Swing_Thread.now { Document_Model(buffer) } match {
-      case Some(model) =>
-        parser(data, model)
-        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
-      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
-    }
+    val syntax = get_syntax
+    val ok =
+      if (syntax.isDefined) {
+        val ok = parser(buffer, syntax.get, data)
+        if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
+        else ok
+      }
+      else false
+    if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
+
     data
   }
 
@@ -87,15 +92,14 @@
 
     val buffer = pane.getBuffer
     Isabelle.buffer_lock(buffer) {
-      Document_Model(buffer) match {
+      get_syntax match {
         case None => null
-        case Some(model) =>
+        case Some(syntax) =>
           val line = buffer.getLineOfOffset(caret)
           val start = buffer.getLineStartOffset(line)
           val text = buffer.getSegment(start, caret - start)
 
-          val completion = model.session.recent_syntax().completion
-          completion.complete(text) match {
+          syntax.completion.complete(text) match {
             case None => null
             case Some((word, cs)) =>
               val ds =
@@ -128,14 +132,13 @@
 }
 
 
-class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
+class Isabelle_Sidekick_Default
+  extends Isabelle_Sidekick("isabelle", Isabelle.session.get_recent_syntax)
 {
   import Thy_Syntax.Structure
 
-  def parser(data: SideKickParsedData, model: Document_Model)
+  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
-    val syntax = model.session.recent_syntax()
-
     def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
       entry match {
         case Structure.Block(name, body) =>
@@ -157,36 +160,53 @@
         case _ => Nil
       }
 
-    val text = Isabelle.buffer_text(model.buffer)
-    val structure = Structure.parse(syntax, model.name, text)
-
-    make_tree(0, structure) foreach (node => data.root.add(node))
+    Isabelle.buffer_node_name(buffer) match {
+      case Some(node_name) =>
+        val text = Isabelle.buffer_text(buffer)
+        val structure = Structure.parse(syntax, node_name, text)
+        make_tree(0, structure) foreach (node => data.root.add(node))
+        true
+      case None => false
+    }
   }
 }
 
 
-class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
+class Isabelle_Sidekick_Options
+  extends Isabelle_Sidekick("isabelle-options", Some(Options.options_syntax))
+
+
+class Isabelle_Sidekick_Root
+  extends Isabelle_Sidekick("isabelle-root", Some(Build.root_syntax))
+
+
+class Isabelle_Sidekick_Raw
+  extends Isabelle_Sidekick("isabelle-raw", Isabelle.session.get_recent_syntax)
 {
-  def parser(data: SideKickParsedData, model: Document_Model)
+  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
-    val root = data.root
-    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
-    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
-      snapshot.state.command_state(snapshot.version, command).markup
-        .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
-          {
-            val range = info.range + command_start
-            val content = command.source(info.range).replace('\n', ' ')
-            val info_text =
-              Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
+    Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
+      case Some(snapshot) =>
+        val root = data.root
+        for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
+          snapshot.state.command_state(snapshot.version, command).markup
+            .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
+              {
+                val range = info.range + command_start
+                val content = command.source(info.range).replace('\n', ' ')
+                val info_text =
+                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
 
-            new DefaultMutableTreeNode(
-              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
-                override def getShortString: String = content
-                override def getLongString: String = info_text
-                override def toString = quote(content) + " " + range.toString
+                new DefaultMutableTreeNode(
+                  new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
+                    override def getShortString: String = content
+                    override def getLongString: String = info_text
+                    override def toString = quote(content) + " " + range.toString
+                  })
               })
-          })
+        }
+        true
+      case None => false
     }
   }
 }
diff -r de26cf3191a3 -r 622251b2b0f1 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Tue Aug 07 20:28:35 2012 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Tue Aug 07 21:38:24 2012 +0200
@@ -180,14 +180,11 @@
 isabelle-output.dock-position=bottom
 isabelle-output.height=174
 isabelle-output.width=412
+isabelle-readme.dock-position=bottom
 isabelle-session.dock-position=bottom
-isabelle-readme.dock-position=bottom
 line-end.shortcut=END
 line-home.shortcut=HOME
 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
-mode.isabelle.customSettings=true
-mode.isabelle.folding=sidekick
-mode.isabelle.sidekick.showStatusWindow.label=true
 print.font=IsabelleText
 restore.remote=false
 restore=false
diff -r de26cf3191a3 -r 622251b2b0f1 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 20:28:35 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 21:38:24 2012 +0200
@@ -193,22 +193,24 @@
     }
   }
 
+  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+  {
+    val name = buffer_name(buffer)
+    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+  }
+
   def init_model(buffer: Buffer)
   {
     swing_buffer_lock(buffer) {
       val opt_model =
-      {
-        val name = buffer_name(buffer)
-        Thy_Header.thy_name(name) match {
-          case Some(theory) =>
-            val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
+        buffer_node_name(buffer) match {
+          case Some(node_name) =>
             document_model(buffer) match {
               case Some(model) if model.name == node_name => Some(model)
               case _ => Some(Document_Model.init(session, buffer, node_name))
             }
           case None => None
         }
-      }
       if (opt_model.isDefined) {
         for (text_area <- jedit_text_areas(buffer)) {
           if (document_view(text_area).map(_.model) != opt_model)
diff -r de26cf3191a3 -r 622251b2b0f1 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml	Tue Aug 07 20:28:35 2012 +0200
+++ b/src/Tools/jEdit/src/services.xml	Tue Aug 07 21:38:24 2012 +0200
@@ -8,6 +8,12 @@
 	<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
 		new isabelle.jedit.Isabelle_Sidekick_Default();
 	</SERVICE>
+	<SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
+		new isabelle.jedit.Isabelle_Sidekick_Options();
+	</SERVICE>
+	<SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
+		new isabelle.jedit.Isabelle_Sidekick_Root();
+	</SERVICE>
 	<SERVICE NAME="isabelle-raw" CLASS="sidekick.SideKickParser">
 		new isabelle.jedit.Isabelle_Sidekick_Raw();
 	</SERVICE>