1.1 --- a/src/Tools/jEdit/plugin/services.xml Fri May 07 22:38:13 2010 +0200
1.2 +++ b/src/Tools/jEdit/plugin/services.xml Fri May 07 23:44:10 2010 +0200
1.3 @@ -6,7 +6,10 @@
1.4 new isabelle.jedit.Isabelle_Encoding();
1.5 </SERVICE>
1.6 <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
1.7 - new isabelle.jedit.Isabelle_Sidekick();
1.8 + new isabelle.jedit.Isabelle_Sidekick_Default();
1.9 + </SERVICE>
1.10 + <SERVICE NAME="isabelle-raw" CLASS="sidekick.SideKickParser">
1.11 + new isabelle.jedit.Isabelle_Sidekick_Raw();
1.12 </SERVICE>
1.13 <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
1.14 new isabelle.jedit.Isabelle_Hyperlinks();
2.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri May 07 22:38:13 2010 +0200
2.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri May 07 23:44:10 2010 +0200
2.3 @@ -1,5 +1,5 @@
2.4 /*
2.5 - * SideKick parser for Isabelle proof documents
2.6 + * SideKick parsers for Isabelle proof documents
2.7 *
2.8 * @author Fabian Immler, TU Munich
2.9 * @author Makarius
2.10 @@ -22,17 +22,26 @@
2.11 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
2.12
2.13
2.14 -class Isabelle_Sidekick extends SideKickParser("isabelle")
2.15 +object Isabelle_Sidekick
2.16 +{
2.17 + implicit def int_to_pos(offset: Int): Position =
2.18 + new Position { def getOffset = offset; override def toString = offset.toString }
2.19 +}
2.20 +
2.21 +
2.22 +class Isabelle_Sidekick(name: String,
2.23 + parser: (() => Boolean, SideKickParsedData, Document_Model) => Unit)
2.24 + extends SideKickParser(name)
2.25 {
2.26 /* parsing */
2.27
2.28 @volatile private var stopped = false
2.29 + private def is_stopped(): Boolean = stopped
2.30 override def stop() = { stopped = true }
2.31
2.32 def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
2.33 {
2.34 - implicit def int_to_pos(offset: Int): Position =
2.35 - new Position { def getOffset = offset; override def toString = offset.toString }
2.36 + import Isabelle_Sidekick.int_to_pos
2.37
2.38 stopped = false
2.39
2.40 @@ -43,34 +52,14 @@
2.41
2.42 Swing_Thread.now { Document_Model(buffer) } match {
2.43 case Some(model) =>
2.44 - val document = model.recent_document()
2.45 - for ((command, command_start) <- document.command_range(0) if !stopped) {
2.46 - root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
2.47 - {
2.48 - val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
2.49 - val id = command.id
2.50 -
2.51 - new DefaultMutableTreeNode(new IAsset {
2.52 - override def getIcon: Icon = null
2.53 - override def getShortString: String = content
2.54 - override def getLongString: String = node.info.toString
2.55 - override def getName: String = id
2.56 - override def setName(name: String) = ()
2.57 - override def setStart(start: Position) = ()
2.58 - override def getStart: Position = command_start + node.start
2.59 - override def setEnd(end: Position) = ()
2.60 - override def getEnd: Position = command_start + node.stop
2.61 - override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
2.62 - })
2.63 - }))
2.64 - }
2.65 + parser(is_stopped, data, model)
2.66 if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
2.67 case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
2.68 }
2.69 data
2.70 }
2.71
2.72 -
2.73 +
2.74 /* completion */
2.75
2.76 override def supportsCompletion = true
2.77 @@ -98,3 +87,65 @@
2.78 }
2.79 }
2.80 }
2.81 +
2.82 +
2.83 +class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle",
2.84 + ((is_stopped: () => Boolean, data: SideKickParsedData, model: Document_Model) =>
2.85 + {
2.86 + import Isabelle_Sidekick.int_to_pos
2.87 +
2.88 + val root = data.root
2.89 + val document = model.recent_document()
2.90 + for {
2.91 + (command, command_start) <- document.command_range(0)
2.92 + if command.is_command && !is_stopped()
2.93 + }
2.94 + {
2.95 + val name = command.name
2.96 + val node =
2.97 + new DefaultMutableTreeNode(new IAsset {
2.98 + override def getIcon: Icon = null
2.99 + override def getShortString: String = name
2.100 + override def getLongString: String = name
2.101 + override def getName: String = name
2.102 + override def setName(name: String) = ()
2.103 + override def setStart(start: Position) = ()
2.104 + override def getStart: Position = command_start
2.105 + override def setEnd(end: Position) = ()
2.106 + override def getEnd: Position = command_start + command.length
2.107 + override def toString = name
2.108 + })
2.109 + root.add(node)
2.110 + }
2.111 + }))
2.112 +
2.113 +
2.114 +class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw",
2.115 + ((is_stopped: () => Boolean, data: SideKickParsedData, model: Document_Model) =>
2.116 + {
2.117 + import Isabelle_Sidekick.int_to_pos
2.118 +
2.119 + val root = data.root
2.120 + val document = model.recent_document()
2.121 + for ((command, command_start) <- document.command_range(0) if !is_stopped()) {
2.122 + root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
2.123 + {
2.124 + val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
2.125 + val id = command.id
2.126 +
2.127 + new DefaultMutableTreeNode(new IAsset {
2.128 + override def getIcon: Icon = null
2.129 + override def getShortString: String = content
2.130 + override def getLongString: String = node.info.toString
2.131 + override def getName: String = id
2.132 + override def setName(name: String) = ()
2.133 + override def setStart(start: Position) = ()
2.134 + override def getStart: Position = command_start + node.start
2.135 + override def setEnd(end: Position) = ()
2.136 + override def getEnd: Position = command_start + node.stop
2.137 + override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
2.138 + })
2.139 + }))
2.140 + }
2.141 + }))
2.142 +