merged
authorwenzelm
Fri Jan 04 21:24:47 2013 +0100 (2013-01-04)
changeset 5073172624ff45676
parent 50723 07ecb6716df2
parent 50730 883963f45ac9
child 50732 b2e7490a1b3d
merged
NEWS
     1.1 --- a/Admin/components/components.sha1	Fri Jan 04 20:04:59 2013 +0100
     1.2 +++ b/Admin/components/components.sha1	Fri Jan 04 21:24:47 2013 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4  7b012f725ec1cc102dc259df178d511cc7890bba  jedit_build-20120813.tar.gz
     1.5  8e1d36f5071e3def2cb281f7fefe9f52352cb88f  jedit_build-20120903.tar.gz
     1.6  8fa0c67f59beba369ab836562eed4e56382f672a  jedit_build-20121201.tar.gz
     1.7 +06e9be2627ebb95c45a9bcfa025d2eeef086b408  jedit_build-20130104.tar.gz
     1.8  8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
     1.9  6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
    1.10  5f95c96bb99927f3a026050f85bd056f37a9189e  kodkodi-1.5.2.tar.gz
     2.1 --- a/Admin/components/main	Fri Jan 04 20:04:59 2013 +0100
     2.2 +++ b/Admin/components/main	Fri Jan 04 21:24:47 2013 +0100
     2.3 @@ -3,7 +3,7 @@
     2.4  e-1.6
     2.5  exec_process-1.0.3
     2.6  jdk-7u9
     2.7 -jedit_build-20121201
     2.8 +jedit_build-20130104
     2.9  jfreechart-1.0.14
    2.10  kodkodi-1.5.2
    2.11  polyml-5.5.0
     3.1 --- a/NEWS	Fri Jan 04 20:04:59 2013 +0100
     3.2 +++ b/NEWS	Fri Jan 04 21:24:47 2013 +0100
     3.3 @@ -96,6 +96,10 @@
     3.4  adjust the main text area font size, and its derivatives for output,
     3.5  tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS.
     3.6  
     3.7 +* More reactive completion popup by default: use \t (TAB) instead of
     3.8 +\n (NEWLINE) to minimize intrusion into regular flow of editing.  See
     3.9 +also "Plugin Options / SideKick / General / Code Completion Options".
    3.10 +
    3.11  * Implicit check and build dialog of the specified logic session
    3.12  image.  For example, HOL, HOLCF, HOL-Nominal can be produced on
    3.13  demand, without bundling big platform-dependent heap images in the
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Jan 04 20:04:59 2013 +0100
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Jan 04 21:24:47 2013 +0100
     4.3 @@ -203,6 +203,7 @@
     4.4  JEDIT_JARS=(
     4.5    "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
     4.6    "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
     4.7 +  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar"
     4.8    "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
     4.9    "$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
    4.10    "$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/jEdit/patches/jedit/completion	Fri Jan 04 21:24:47 2013 +0100
     5.3 @@ -0,0 +1,15 @@
     5.4 +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.5 +--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java	2012-11-17 16:41:58.000000000 +0100
     5.6 ++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java	2013-01-04 14:25:57.095172180 +0100
     5.7 +@@ -113,9 +113,9 @@
     5.8 + 		list.setCellRenderer(new CellRenderer());
     5.9 + 		list.addKeyListener(keyHandler);
    5.10 + 		list.addMouseListener(new MouseHandler());
    5.11 ++		list.setFocusTraversalKeysEnabled(false);
    5.12 + 
    5.13 + 		JPanel content = new JPanel(new BorderLayout());
    5.14 +-		content.setFocusTraversalKeysEnabled(false);
    5.15 + 		// stupid scrollbar policy is an attempt to work around
    5.16 + 		// bugs people have been seeing with IBM's JDK -- 7 Sep 2000
    5.17 + 		JScrollPane scroller = new JScrollPane(list,
    5.18 +
     6.1 --- a/src/Tools/jEdit/patches/jedit/macos	Fri Jan 04 20:04:59 2013 +0100
     6.2 +++ b/src/Tools/jEdit/patches/jedit/macos	Fri Jan 04 21:24:47 2013 +0100
     6.3 @@ -13,26 +13,31 @@
     6.4   			{
     6.5   				os = VMS;
     6.6  diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
     6.7 ---- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java	2012-11-17 16:42:29.000000000 +0100
     6.8 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java	2012-12-01 21:55:48.000000000 +0100
     6.9 -@@ -109,6 +109,7 @@
    6.10 - 	 * used to handle a modifier key press in conjunction with an alphabet
    6.11 - 	 * key. <b>On by default on MacOS.</b>
    6.12 - 	 */
    6.13 -+	public static boolean ALTERNATIVE_DISPATCHER0 = false;
    6.14 - 	public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
    6.15 +--- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java     2012-11-17 16:42:29.000000000 +0100
    6.16 ++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java     2013-01-04 20:00:25.698332853 +0100
    6.17 +@@ -109,7 +109,7 @@
    6.18 +         * used to handle a modifier key press in conjunction with an alphabet
    6.19 +         * key. <b>On by default on MacOS.</b>
    6.20 +         */
    6.21 +-       public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
    6.22 ++       public static boolean ALTERNATIVE_DISPATCHER = false;
    6.23   
    6.24 - 	/**
    6.25 -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
    6.26 ---- 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventTranslator.java	2012-11-17 16:41:58.000000000 +0100
    6.27 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventTranslator.java	2012-12-01 21:56:04.000000000 +0100
    6.28 -@@ -79,7 +79,7 @@
    6.29 - 				|| (keyCode >= KeyEvent.VK_A
    6.30 - 				&& keyCode <= KeyEvent.VK_Z))
    6.31 - 			{
    6.32 --				if(Debug.ALTERNATIVE_DISPATCHER)
    6.33 -+				if(Debug.ALTERNATIVE_DISPATCHER0)
    6.34 - 					return null;
    6.35 - 				else
    6.36 - 				{
    6.37 +        /**
    6.38 +         * If true, A+ shortcuts are disabled. If you use this, you should also
    6.39 +diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 5.0.0/jEdit-patched/org/gjt/sp/jed
    6.40 +it/gui/KeyEventWorkaround.java
    6.41 +--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java    2012-11-17 16:41:58.000000000 +0100
    6.42 ++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java    2013-01-04 20:04:43.02632209
    6.43 +2 +0100
    6.44 +@@ -297,8 +297,8 @@
    6.45 + 
    6.46 +                        if(!Debug.ALTERNATIVE_DISPATCHER)
    6.47 +                        {
    6.48 +-                               if(((modifiers & InputEvent.CTRL_MASK) != 0
    6.49 +-                                       ^ (modifiers & InputEvent.ALT_MASK) != 0)
    6.50 ++                               if((modifiers & InputEvent.CTRL_MASK) != 0 && (modifiers & InputEvent.ALT_MASK) == 0
    6.51 ++                                       || (modifiers & InputEvent.CTRL_MASK) == 0 && (modifiers & InputEvent.ALT_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED
    6.52 +                                        || (modifiers & InputEvent.META_MASK) != 0)
    6.53 +                                {
    6.54 +                                        return null;
    6.55  
     7.1 --- a/src/Tools/jEdit/src/Isabelle.props	Fri Jan 04 20:04:59 2013 +0100
     7.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Fri Jan 04 21:24:47 2013 +0100
     7.3 @@ -16,8 +16,9 @@
     7.4  plugin.isabelle.jedit.Plugin.depend.0=jdk 1.7
     7.5  plugin.isabelle.jedit.Plugin.depend.1=jedit 05.00.00.00
     7.6  plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.0
     7.7 -plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.0
     7.8 +plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.1
     7.9  plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.4
    7.10 +plugin.isabelle.jedit.Plugin.depend.5=plugin gatchan.highlight.HighlightPlugin 1.9.10
    7.11  
    7.12  #options
    7.13  plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
     8.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Jan 04 20:04:59 2013 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Jan 04 21:24:47 2013 +0100
     8.3 @@ -20,8 +20,7 @@
     8.4  
     8.5  import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
     8.6  import errorlist.DefaultErrorSource
     8.7 -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion,
     8.8 -  SideKickCompletionPopup, IAsset}
     8.9 +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
    8.10  
    8.11  
    8.12  object Isabelle_Sidekick
     9.1 --- a/src/Tools/jEdit/src/jEdit.props	Fri Jan 04 20:04:59 2013 +0100
     9.2 +++ b/src/Tools/jEdit/src/jEdit.props	Fri Jan 04 21:24:47 2013 +0100
     9.3 @@ -205,7 +205,7 @@
     9.4  line-end.shortcut=END
     9.5  line-home.shortcut=HOME
     9.6  lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
     9.7 -plugin.MacOSXPlugin.altDispatcher=true
     9.8 +plugin.MacOSXPlugin.altDispatcher=false
     9.9  plugin.MacOSXPlugin.disableOption=true
    9.10  print.font=IsabelleText
    9.11  restore.remote=false
    9.12 @@ -213,9 +213,9 @@
    9.13  sidekick-tree.dock-position=right
    9.14  sidekick.auto-complete-popup-get-focus=true
    9.15  sidekick.buffer-save-parse=true
    9.16 -sidekick.complete-delay=300
    9.17 +sidekick.complete-delay=0
    9.18  sidekick.complete-instant.toggle=false
    9.19 -sidekick.complete-popup.accept-characters=\\n\\t
    9.20 +sidekick.complete-popup.accept-characters=\\t
    9.21  sidekick.complete-popup.insert-characters=
    9.22  sidekick.splitter.location=721
    9.23  systrayicon=false
    10.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jan 04 20:04:59 2013 +0100
    10.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jan 04 21:24:47 2013 +0100
    10.3 @@ -10,9 +10,8 @@
    10.4  
    10.5  import isabelle._
    10.6  
    10.7 -import java.awt.{Color, Font, FontMetrics, Toolkit}
    10.8 -import java.awt.event.{ActionListener, ActionEvent, KeyEvent}
    10.9 -import javax.swing.{KeyStroke, JComponent}
   10.10 +import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
   10.11 +import java.awt.event.{KeyEvent, KeyAdapter}
   10.12  
   10.13  import org.gjt.sp.jedit.{jEdit, View, Registers}
   10.14  import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
   10.15 @@ -159,22 +158,24 @@
   10.16    }
   10.17  
   10.18  
   10.19 -  /* keyboard actions */
   10.20 +  /* key handling */
   10.21  
   10.22 -  private val action_listener = new ActionListener {
   10.23 -    def actionPerformed(e: ActionEvent) {
   10.24 -      e.getActionCommand match {
   10.25 -        case "copy" => Registers.copy(text_area, '$')
   10.26 +  addKeyListener(new KeyAdapter {
   10.27 +    override def keyPressed(evt: KeyEvent)
   10.28 +    {
   10.29 +      evt.getKeyCode match {
   10.30 +        case KeyEvent.VK_C
   10.31 +        if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
   10.32 +          Registers.copy(text_area, '$')
   10.33 +        case KeyEvent.VK_ESCAPE =>
   10.34 +          Window.getWindows foreach {
   10.35 +            case c: Pretty_Tooltip => c.dispose
   10.36 +            case _ =>
   10.37 +          }
   10.38          case _ =>
   10.39        }
   10.40      }
   10.41 -  }
   10.42 -
   10.43 -  registerKeyboardAction(action_listener, "copy",
   10.44 -    KeyStroke.getKeyStroke(KeyEvent.VK_COPY, 0), JComponent.WHEN_FOCUSED)
   10.45 -  registerKeyboardAction(action_listener, "copy",
   10.46 -    KeyStroke.getKeyStroke(KeyEvent.VK_C,
   10.47 -      Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()), JComponent.WHEN_FOCUSED)
   10.48 +  })
   10.49  
   10.50  
   10.51    /* init */
    11.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jan 04 20:04:59 2013 +0100
    11.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jan 04 21:24:47 2013 +0100
    11.3 @@ -10,8 +10,8 @@
    11.4  import isabelle._
    11.5  
    11.6  import java.awt.{Color, Point, BorderLayout, Window, Dimension}
    11.7 -import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
    11.8 -import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent, KeyStroke}
    11.9 +import java.awt.event.{WindowEvent, WindowAdapter}
   11.10 +import javax.swing.{SwingUtilities, JDialog, JPanel, JComponent}
   11.11  import javax.swing.border.LineBorder
   11.12  
   11.13  import scala.swing.{FlowPanel, Label}
   11.14 @@ -37,7 +37,6 @@
   11.15  
   11.16    window.setUndecorated(true)
   11.17    window.setFocusableWindowState(true)
   11.18 -  window.setAutoRequestFocus(true)
   11.19  
   11.20    window.addWindowFocusListener(new WindowAdapter {
   11.21      override def windowLostFocus(e: WindowEvent) {
   11.22 @@ -47,24 +46,8 @@
   11.23      }
   11.24    })
   11.25  
   11.26 -  private val action_listener = new ActionListener {
   11.27 -    def actionPerformed(e: ActionEvent) {
   11.28 -      e.getActionCommand match {
   11.29 -        case "close_all" =>
   11.30 -          Window.getWindows foreach {
   11.31 -            case c: Pretty_Tooltip => c.dispose
   11.32 -            case _ =>
   11.33 -          }
   11.34 -        case _ =>
   11.35 -      }
   11.36 -    }
   11.37 -  }
   11.38 -
   11.39    window.setContentPane(new JPanel(new BorderLayout) {
   11.40      setBackground(rendering.tooltip_color)
   11.41 -    registerKeyboardAction(action_listener, "close_all",
   11.42 -      KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
   11.43 -
   11.44      override def getFocusTraversalKeysEnabled(): Boolean = false
   11.45    })
   11.46    window.getRootPane.setBorder(new LineBorder(Color.BLACK))
   11.47 @@ -77,9 +60,6 @@
   11.48      Rendering.font_size("jedit_tooltip_font_scale").round)
   11.49    pretty_text_area.update(rendering.snapshot, results, body)
   11.50  
   11.51 -  pretty_text_area.registerKeyboardAction(action_listener, "close_all",
   11.52 -    KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
   11.53 -
   11.54    window.add(pretty_text_area)
   11.55  
   11.56  
   11.57 @@ -136,6 +116,7 @@
   11.58    }
   11.59  
   11.60    window.setVisible(true)
   11.61 +  pretty_text_area.requestFocus
   11.62    pretty_text_area.refresh()
   11.63  }
   11.64