# HG changeset patch
# User immler
# Date 1353491472 -3600
# Node ID 4ff5d795ed0841b6ef052436c1c049feeecbce50
# Parent  bc82d25af543dfafbb3eaf470ec6b3f35b9c22bf
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
search field for symbols

diff -r bc82d25af543 -r 4ff5d795ed08 src/Tools/jEdit/lib/Tools/jedit
--- 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"
diff -r bc82d25af543 -r 4ff5d795ed08 src/Tools/jEdit/src/Isabelle.props
--- 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
diff -r bc82d25af543 -r 4ff5d795ed08 src/Tools/jEdit/src/actions.xml
--- 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);
diff -r bc82d25af543 -r 4ff5d795ed08 src/Tools/jEdit/src/dockables.xml
--- 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
diff -r bc82d25af543 -r 4ff5d795ed08 src/Tools/jEdit/src/symbols_dockable.scala
--- /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)
+}