# HG changeset patch
# User wenzelm
# Date 1357331087 -3600
# Node ID 72624ff45676ea48730ba02f3675d5c678d0b9e0
# Parent 07ecb6716df2f7baefb4a208bd9fdda7318b4a55# Parent 883963f45ac92d7459746035a24503a91ae2fc73
merged
diff -r 07ecb6716df2 -r 72624ff45676 Admin/components/components.sha1
--- a/Admin/components/components.sha1 Fri Jan 04 20:04:59 2013 +0100
+++ b/Admin/components/components.sha1 Fri Jan 04 21:24:47 2013 +0100
@@ -18,6 +18,7 @@
7b012f725ec1cc102dc259df178d511cc7890bba jedit_build-20120813.tar.gz
8e1d36f5071e3def2cb281f7fefe9f52352cb88f jedit_build-20120903.tar.gz
8fa0c67f59beba369ab836562eed4e56382f672a jedit_build-20121201.tar.gz
+06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
diff -r 07ecb6716df2 -r 72624ff45676 Admin/components/main
--- a/Admin/components/main Fri Jan 04 20:04:59 2013 +0100
+++ b/Admin/components/main Fri Jan 04 21:24:47 2013 +0100
@@ -3,7 +3,7 @@
e-1.6
exec_process-1.0.3
jdk-7u9
-jedit_build-20121201
+jedit_build-20130104
jfreechart-1.0.14
kodkodi-1.5.2
polyml-5.5.0
diff -r 07ecb6716df2 -r 72624ff45676 NEWS
--- a/NEWS Fri Jan 04 20:04:59 2013 +0100
+++ b/NEWS Fri Jan 04 21:24:47 2013 +0100
@@ -96,6 +96,10 @@
adjust the main text area font size, and its derivatives for output,
tooltips etc. Cf. keyboard shortcuts C-PLUS and C-MINUS.
+* More reactive completion popup by default: use \t (TAB) instead of
+\n (NEWLINE) to minimize intrusion into regular flow of editing. See
+also "Plugin Options / SideKick / General / Code Completion Options".
+
* Implicit check and build dialog of the specified logic session
image. For example, HOL, HOLCF, HOL-Nominal can be produced on
demand, without bundling big platform-dependent heap images in the
diff -r 07ecb6716df2 -r 72624ff45676 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Jan 04 20:04:59 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jan 04 21:24:47 2013 +0100
@@ -203,6 +203,7 @@
JEDIT_JARS=(
"$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
+ "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
diff -r 07ecb6716df2 -r 72624ff45676 src/Tools/jEdit/patches/jedit/completion
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit/completion Fri Jan 04 21:24:47 2013 +0100
@@ -0,0 +1,15 @@
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java 2012-11-17 16:41:58.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java 2013-01-04 14:25:57.095172180 +0100
+@@ -113,9 +113,9 @@
+ list.setCellRenderer(new CellRenderer());
+ list.addKeyListener(keyHandler);
+ list.addMouseListener(new MouseHandler());
++ list.setFocusTraversalKeysEnabled(false);
+
+ JPanel content = new JPanel(new BorderLayout());
+- content.setFocusTraversalKeysEnabled(false);
+ // stupid scrollbar policy is an attempt to work around
+ // bugs people have been seeing with IBM's JDK -- 7 Sep 2000
+ JScrollPane scroller = new JScrollPane(list,
+
diff -r 07ecb6716df2 -r 72624ff45676 src/Tools/jEdit/patches/jedit/macos
--- a/src/Tools/jEdit/patches/jedit/macos Fri Jan 04 20:04:59 2013 +0100
+++ b/src/Tools/jEdit/patches/jedit/macos Fri Jan 04 21:24:47 2013 +0100
@@ -13,26 +13,31 @@
{
os = VMS;
diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
---- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 2012-11-17 16:42:29.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2012-12-01 21:55:48.000000000 +0100
-@@ -109,6 +109,7 @@
- * used to handle a modifier key press in conjunction with an alphabet
- * key. On by default on MacOS.
- */
-+ public static boolean ALTERNATIVE_DISPATCHER0 = false;
- public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
+--- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 2012-11-17 16:42:29.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2013-01-04 20:00:25.698332853 +0100
+@@ -109,7 +109,7 @@
+ * used to handle a modifier key press in conjunction with an alphabet
+ * key. On by default on MacOS.
+ */
+- public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
++ public static boolean ALTERNATIVE_DISPATCHER = false;
- /**
-diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventTranslator.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventTranslator.java
---- 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventTranslator.java 2012-11-17 16:41:58.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventTranslator.java 2012-12-01 21:56:04.000000000 +0100
-@@ -79,7 +79,7 @@
- || (keyCode >= KeyEvent.VK_A
- && keyCode <= KeyEvent.VK_Z))
- {
-- if(Debug.ALTERNATIVE_DISPATCHER)
-+ if(Debug.ALTERNATIVE_DISPATCHER0)
- return null;
- else
- {
+ /**
+ * If true, A+ shortcuts are disabled. If you use this, you should also
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 5.0.0/jEdit-patched/org/gjt/sp/jed
+it/gui/KeyEventWorkaround.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2012-11-17 16:41:58.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-01-04 20:04:43.02632209
+2 +0100
+@@ -297,8 +297,8 @@
+
+ if(!Debug.ALTERNATIVE_DISPATCHER)
+ {
+- if(((modifiers & InputEvent.CTRL_MASK) != 0
+- ^ (modifiers & InputEvent.ALT_MASK) != 0)
++ if((modifiers & InputEvent.CTRL_MASK) != 0 && (modifiers & InputEvent.ALT_MASK) == 0
++ || (modifiers & InputEvent.CTRL_MASK) == 0 && (modifiers & InputEvent.ALT_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED
+ || (modifiers & InputEvent.META_MASK) != 0)
+ {
+ return null;
diff -r 07ecb6716df2 -r 72624ff45676 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Fri Jan 04 20:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Fri Jan 04 21:24:47 2013 +0100
@@ -16,8 +16,9 @@
plugin.isabelle.jedit.Plugin.depend.0=jdk 1.7
plugin.isabelle.jedit.Plugin.depend.1=jedit 05.00.00.00
plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.0
-plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.0
+plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.1
plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.4
+plugin.isabelle.jedit.Plugin.depend.5=plugin gatchan.highlight.HighlightPlugin 1.9.10
#options
plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
diff -r 07ecb6716df2 -r 72624ff45676 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Jan 04 20:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Jan 04 21:24:47 2013 +0100
@@ -20,8 +20,7 @@
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
import errorlist.DefaultErrorSource
-import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion,
- SideKickCompletionPopup, IAsset}
+import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
object Isabelle_Sidekick
diff -r 07ecb6716df2 -r 72624ff45676 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props Fri Jan 04 20:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Fri Jan 04 21:24:47 2013 +0100
@@ -205,7 +205,7 @@
line-end.shortcut=END
line-home.shortcut=HOME
lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
-plugin.MacOSXPlugin.altDispatcher=true
+plugin.MacOSXPlugin.altDispatcher=false
plugin.MacOSXPlugin.disableOption=true
print.font=IsabelleText
restore.remote=false
@@ -213,9 +213,9 @@
sidekick-tree.dock-position=right
sidekick.auto-complete-popup-get-focus=true
sidekick.buffer-save-parse=true
-sidekick.complete-delay=300
+sidekick.complete-delay=0
sidekick.complete-instant.toggle=false
-sidekick.complete-popup.accept-characters=\\n\\t
+sidekick.complete-popup.accept-characters=\\t
sidekick.complete-popup.insert-characters=
sidekick.splitter.location=721
systrayicon=false
diff -r 07ecb6716df2 -r 72624ff45676 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Jan 04 20:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Jan 04 21:24:47 2013 +0100
@@ -10,9 +10,8 @@
import isabelle._
-import java.awt.{Color, Font, FontMetrics, Toolkit}
-import java.awt.event.{ActionListener, ActionEvent, KeyEvent}
-import javax.swing.{KeyStroke, JComponent}
+import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
+import java.awt.event.{KeyEvent, KeyAdapter}
import org.gjt.sp.jedit.{jEdit, View, Registers}
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
@@ -159,22 +158,24 @@
}
- /* keyboard actions */
+ /* key handling */
- private val action_listener = new ActionListener {
- def actionPerformed(e: ActionEvent) {
- e.getActionCommand match {
- case "copy" => Registers.copy(text_area, '$')
+ addKeyListener(new KeyAdapter {
+ override def keyPressed(evt: KeyEvent)
+ {
+ evt.getKeyCode match {
+ case KeyEvent.VK_C
+ if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
+ Registers.copy(text_area, '$')
+ case KeyEvent.VK_ESCAPE =>
+ Window.getWindows foreach {
+ case c: Pretty_Tooltip => c.dispose
+ case _ =>
+ }
case _ =>
}
}
- }
-
- registerKeyboardAction(action_listener, "copy",
- KeyStroke.getKeyStroke(KeyEvent.VK_COPY, 0), JComponent.WHEN_FOCUSED)
- registerKeyboardAction(action_listener, "copy",
- KeyStroke.getKeyStroke(KeyEvent.VK_C,
- Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()), JComponent.WHEN_FOCUSED)
+ })
/* init */
diff -r 07ecb6716df2 -r 72624ff45676 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri Jan 04 20:04:59 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Jan 04 21:24:47 2013 +0100
@@ -10,8 +10,8 @@
import isabelle._
import java.awt.{Color, Point, BorderLayout, Window, Dimension}
-import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
-import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent, KeyStroke}
+import java.awt.event.{WindowEvent, WindowAdapter}
+import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent}
import javax.swing.border.LineBorder
import scala.swing.{FlowPanel, Label}
@@ -37,7 +37,6 @@
window.setUndecorated(true)
window.setFocusableWindowState(true)
- window.setAutoRequestFocus(true)
window.addWindowFocusListener(new WindowAdapter {
override def windowLostFocus(e: WindowEvent) {
@@ -47,24 +46,8 @@
}
})
- private val action_listener = new ActionListener {
- def actionPerformed(e: ActionEvent) {
- e.getActionCommand match {
- case "close_all" =>
- Window.getWindows foreach {
- case c: Pretty_Tooltip => c.dispose
- case _ =>
- }
- case _ =>
- }
- }
- }
-
window.setContentPane(new JPanel(new BorderLayout) {
setBackground(rendering.tooltip_color)
- registerKeyboardAction(action_listener, "close_all",
- KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
-
override def getFocusTraversalKeysEnabled(): Boolean = false
})
window.getRootPane.setBorder(new LineBorder(Color.BLACK))
@@ -77,9 +60,6 @@
Rendering.font_size("jedit_tooltip_font_scale").round)
pretty_text_area.update(rendering.snapshot, results, body)
- pretty_text_area.registerKeyboardAction(action_listener, "close_all",
- KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
-
window.add(pretty_text_area)
@@ -136,6 +116,7 @@
}
window.setVisible(true)
+ pretty_text_area.requestFocus
pretty_text_area.refresh()
}