1.1 --- a/src/Tools/jEdit/src/Isabelle.props Tue Aug 07 20:28:35 2012 +0200
1.2 +++ b/src/Tools/jEdit/src/Isabelle.props Tue Aug 07 21:38:24 2012 +0200
1.3 @@ -67,9 +67,15 @@
1.4 isabelle-syslog.title=Syslog
1.5
1.6 #SideKick
1.7 +mode.isabelle.sidekick.showStatusWindow.label=true
1.8 sidekick.parser.isabelle.label=Isabelle
1.9 mode.isabelle.sidekick.parser=isabelle
1.10 +mode.isabelle-options.sidekick.parser=isabelle-options
1.11 +mode.isabelle-root.sidekick.parser=isabelle-root
1.12 mode.ml.sidekick.parser=isabelle
1.13
1.14 +mode.isabelle.customSettings=true
1.15 +mode.isabelle.folding=sidekick
1.16 +
1.17 #Hyperlinks
1.18 mode.isabelle.hyperlink.source=isabelle
2.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 07 20:28:35 2012 +0200
2.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 07 21:38:24 2012 +0200
2.3 @@ -48,14 +48,15 @@
2.4 }
2.5
2.6
2.7 -abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
2.8 +class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
2.9 + extends SideKickParser(name)
2.10 {
2.11 /* parsing */
2.12
2.13 @volatile protected var stopped = false
2.14 override def stop() = { stopped = true }
2.15
2.16 - def parser(data: SideKickParsedData, model: Document_Model): Unit
2.17 + def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
2.18
2.19 def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
2.20 {
2.21 @@ -66,12 +67,16 @@
2.22 val root = data.root
2.23 data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
2.24
2.25 - Swing_Thread.now { Document_Model(buffer) } match {
2.26 - case Some(model) =>
2.27 - parser(data, model)
2.28 - if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
2.29 - case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
2.30 - }
2.31 + val syntax = get_syntax
2.32 + val ok =
2.33 + if (syntax.isDefined) {
2.34 + val ok = parser(buffer, syntax.get, data)
2.35 + if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
2.36 + else ok
2.37 + }
2.38 + else false
2.39 + if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
2.40 +
2.41 data
2.42 }
2.43
2.44 @@ -87,15 +92,14 @@
2.45
2.46 val buffer = pane.getBuffer
2.47 Isabelle.buffer_lock(buffer) {
2.48 - Document_Model(buffer) match {
2.49 + get_syntax match {
2.50 case None => null
2.51 - case Some(model) =>
2.52 + case Some(syntax) =>
2.53 val line = buffer.getLineOfOffset(caret)
2.54 val start = buffer.getLineStartOffset(line)
2.55 val text = buffer.getSegment(start, caret - start)
2.56
2.57 - val completion = model.session.recent_syntax().completion
2.58 - completion.complete(text) match {
2.59 + syntax.completion.complete(text) match {
2.60 case None => null
2.61 case Some((word, cs)) =>
2.62 val ds =
2.63 @@ -128,14 +132,13 @@
2.64 }
2.65
2.66
2.67 -class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
2.68 +class Isabelle_Sidekick_Default
2.69 + extends Isabelle_Sidekick("isabelle", Isabelle.session.get_recent_syntax)
2.70 {
2.71 import Thy_Syntax.Structure
2.72
2.73 - def parser(data: SideKickParsedData, model: Document_Model)
2.74 + override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
2.75 {
2.76 - val syntax = model.session.recent_syntax()
2.77 -
2.78 def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
2.79 entry match {
2.80 case Structure.Block(name, body) =>
2.81 @@ -157,37 +160,54 @@
2.82 case _ => Nil
2.83 }
2.84
2.85 - val text = Isabelle.buffer_text(model.buffer)
2.86 - val structure = Structure.parse(syntax, model.name, text)
2.87 -
2.88 - make_tree(0, structure) foreach (node => data.root.add(node))
2.89 - }
2.90 -}
2.91 -
2.92 -
2.93 -class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
2.94 -{
2.95 - def parser(data: SideKickParsedData, model: Document_Model)
2.96 - {
2.97 - val root = data.root
2.98 - val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
2.99 - for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
2.100 - snapshot.state.command_state(snapshot.version, command).markup
2.101 - .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
2.102 - {
2.103 - val range = info.range + command_start
2.104 - val content = command.source(info.range).replace('\n', ' ')
2.105 - val info_text =
2.106 - Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
2.107 -
2.108 - new DefaultMutableTreeNode(
2.109 - new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
2.110 - override def getShortString: String = content
2.111 - override def getLongString: String = info_text
2.112 - override def toString = quote(content) + " " + range.toString
2.113 - })
2.114 - })
2.115 + Isabelle.buffer_node_name(buffer) match {
2.116 + case Some(node_name) =>
2.117 + val text = Isabelle.buffer_text(buffer)
2.118 + val structure = Structure.parse(syntax, node_name, text)
2.119 + make_tree(0, structure) foreach (node => data.root.add(node))
2.120 + true
2.121 + case None => false
2.122 }
2.123 }
2.124 }
2.125
2.126 +
2.127 +class Isabelle_Sidekick_Options
2.128 + extends Isabelle_Sidekick("isabelle-options", Some(Options.options_syntax))
2.129 +
2.130 +
2.131 +class Isabelle_Sidekick_Root
2.132 + extends Isabelle_Sidekick("isabelle-root", Some(Build.root_syntax))
2.133 +
2.134 +
2.135 +class Isabelle_Sidekick_Raw
2.136 + extends Isabelle_Sidekick("isabelle-raw", Isabelle.session.get_recent_syntax)
2.137 +{
2.138 + override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
2.139 + {
2.140 + Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
2.141 + case Some(snapshot) =>
2.142 + val root = data.root
2.143 + for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
2.144 + snapshot.state.command_state(snapshot.version, command).markup
2.145 + .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
2.146 + {
2.147 + val range = info.range + command_start
2.148 + val content = command.source(info.range).replace('\n', ' ')
2.149 + val info_text =
2.150 + Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
2.151 +
2.152 + new DefaultMutableTreeNode(
2.153 + new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
2.154 + override def getShortString: String = content
2.155 + override def getLongString: String = info_text
2.156 + override def toString = quote(content) + " " + range.toString
2.157 + })
2.158 + })
2.159 + }
2.160 + true
2.161 + case None => false
2.162 + }
2.163 + }
2.164 +}
2.165 +
3.1 --- a/src/Tools/jEdit/src/jEdit.props Tue Aug 07 20:28:35 2012 +0200
3.2 +++ b/src/Tools/jEdit/src/jEdit.props Tue Aug 07 21:38:24 2012 +0200
3.3 @@ -180,14 +180,11 @@
3.4 isabelle-output.dock-position=bottom
3.5 isabelle-output.height=174
3.6 isabelle-output.width=412
3.7 +isabelle-readme.dock-position=bottom
3.8 isabelle-session.dock-position=bottom
3.9 -isabelle-readme.dock-position=bottom
3.10 line-end.shortcut=END
3.11 line-home.shortcut=HOME
3.12 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
3.13 -mode.isabelle.customSettings=true
3.14 -mode.isabelle.folding=sidekick
3.15 -mode.isabelle.sidekick.showStatusWindow.label=true
3.16 print.font=IsabelleText
3.17 restore.remote=false
3.18 restore=false
4.1 --- a/src/Tools/jEdit/src/plugin.scala Tue Aug 07 20:28:35 2012 +0200
4.2 +++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 07 21:38:24 2012 +0200
4.3 @@ -193,22 +193,24 @@
4.4 }
4.5 }
4.6
4.7 + def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
4.8 + {
4.9 + val name = buffer_name(buffer)
4.10 + Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
4.11 + }
4.12 +
4.13 def init_model(buffer: Buffer)
4.14 {
4.15 swing_buffer_lock(buffer) {
4.16 val opt_model =
4.17 - {
4.18 - val name = buffer_name(buffer)
4.19 - Thy_Header.thy_name(name) match {
4.20 - case Some(theory) =>
4.21 - val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
4.22 + buffer_node_name(buffer) match {
4.23 + case Some(node_name) =>
4.24 document_model(buffer) match {
4.25 case Some(model) if model.name == node_name => Some(model)
4.26 case _ => Some(Document_Model.init(session, buffer, node_name))
4.27 }
4.28 case None => None
4.29 }
4.30 - }
4.31 if (opt_model.isDefined) {
4.32 for (text_area <- jedit_text_areas(buffer)) {
4.33 if (document_view(text_area).map(_.model) != opt_model)
5.1 --- a/src/Tools/jEdit/src/services.xml Tue Aug 07 20:28:35 2012 +0200
5.2 +++ b/src/Tools/jEdit/src/services.xml Tue Aug 07 21:38:24 2012 +0200
5.3 @@ -8,6 +8,12 @@
5.4 <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
5.5 new isabelle.jedit.Isabelle_Sidekick_Default();
5.6 </SERVICE>
5.7 + <SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
5.8 + new isabelle.jedit.Isabelle_Sidekick_Options();
5.9 + </SERVICE>
5.10 + <SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
5.11 + new isabelle.jedit.Isabelle_Sidekick_Root();
5.12 + </SERVICE>
5.13 <SERVICE NAME="isabelle-raw" CLASS="sidekick.SideKickParser">
5.14 new isabelle.jedit.Isabelle_Sidekick_Raw();
5.15 </SERVICE>