dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
search field for symbols
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Nov 21 11:08:56 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Nov 21 10:51:12 2012 +0100
@@ -35,6 +35,7 @@
"src/scala_console.scala"
"src/sendback.scala"
"src/session_dockable.scala"
+ "src/symbols_dockable.scala"
"src/syslog_dockable.scala"
"src/text_overview.scala"
"src/token_markup.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Wed Nov 21 11:08:56 2012 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Wed Nov 21 10:51:12 2012 +0100
@@ -40,13 +40,14 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.graphview-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
+plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.graphview-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.symbols-panel isabelle.syslog-panel
isabelle.session-panel.label=Prover Session panel
isabelle.output-panel.label=Output panel
isabelle.graphview-panel.label=Graphview panel
isabelle.raw-output-panel.label=Raw Output panel
isabelle.protocol-panel.label=Protocol panel
isabelle.readme-panel.label=README panel
+isabelle.symbols-panel.label=Symbols panel
isabelle.syslog-panel.label=Syslog panel
#dockables
@@ -58,6 +59,7 @@
isabelle-protocol.title=Protocol
isabelle-readme.title=README
isabelle-syslog.title=Syslog
+isabelle-symbols.title=Symbols
#SideKick
mode.isabelle-options.folding=sidekick
--- a/src/Tools/jEdit/src/actions.xml Wed Nov 21 11:08:56 2012 +0100
+++ b/src/Tools/jEdit/src/actions.xml Wed Nov 21 10:51:12 2012 +0100
@@ -37,6 +37,11 @@
wm.addDockableWindow("isabelle-protocol");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.symbols-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-symbols");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.input-sub">
<CODE>
isabelle.jedit.Isabelle.input_sub(textArea);
--- a/src/Tools/jEdit/src/dockables.xml Wed Nov 21 11:08:56 2012 +0100
+++ b/src/Tools/jEdit/src/dockables.xml Wed Nov 21 10:51:12 2012 +0100
@@ -26,4 +26,7 @@
<DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
new isabelle.jedit.Protocol_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
+ new isabelle.jedit.Symbols_Dockable(view, position);
+ </DOCKABLE>
</DOCKABLES>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Nov 21 10:51:12 2012 +0100
@@ -0,0 +1,69 @@
+/* Title: Tools/jEdit/src/symbols_dockable.scala
+ Author: Fabian Immler
+
+Dockable window for Symbol Palette.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Font
+import org.gjt.sp.jedit.View
+
+import scala.swing.event.ValueChanged
+import scala.swing.{Action, Button, FlowPanel, TabbedPane, TextField, BorderPanel, Label}
+
+class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+
+ private val max_results = 50
+
+ val searchspace = for (val (group, symbols) <- Symbol.groups; val sym <- symbols)
+ yield (sym, (sym.toLowerCase + get_name(Symbol.decode(sym)).toLowerCase))
+
+ def get_name(c: String): String =
+ if (c.length >= 1) Character.getName(c.codePointAt(0)) else "??"
+
+ private class Symbol_Component(val symbol: String) extends Button
+ {
+ val dec = Symbol.decode(symbol)
+ font =
+ new Font(Isabelle.font_family(), Font.PLAIN, Isabelle.font_size("jedit_font_scale").round)
+ action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
+ tooltip = symbol + " - " + get_name(dec)
+ }
+
+ val group_tabs = new TabbedPane {
+ pages ++= (for (val (group, symbols) <- Symbol.groups) yield
+ {
+ new TabbedPane.Page(if (group == "") "Other" else group,
+ new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) },
+ ("" /: (symbols take 10 map Symbol.decode))(_ + _ + " "))
+ }).toList.sortWith(_.title.toUpperCase <= _.title.toUpperCase)
+ pages += new TabbedPane.Page("Search", new BorderPanel {
+ val search = new TextField(10)
+ val results_panel = new FlowPanel
+ add(search, BorderPanel.Position.North)
+ add(results_panel, BorderPanel.Position.Center)
+ listenTo(search)
+ var last = search.text
+ reactions += { case ValueChanged(`search`) =>
+ if (search.text != last) {
+ last = search.text
+ results_panel.contents.clear
+ val results =
+ (searchspace filter (search.text.toLowerCase.split("\\s+") forall _._2.contains)
+ take (max_results + 1)).toList
+ for ((sym, _) <- results)
+ results_panel.contents += new Symbol_Component(sym)
+ if (results.length > max_results) results_panel.contents += new Label("...")
+ results_panel.revalidate
+ results_panel.repaint
+ }
+ }
+ }, "Search Symbols")
+ }
+ set_content(group_tabs)
+}