--- 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
--- 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
}
}
}
--- 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
--- 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)
--- 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>