[isabelle-dev] NEWS: Improved completion mechanism
* Improved completion mechanism, which is now managed by the Isabelle/jEdit plugin instead of SideKick. - Various Isabelle plugin options to control popup behaviour and immediate insertion into buffer. - Light-weight popup, which avoids explicit window (more reactive and more robust). Interpreted key events: TAB, ESCAPE, UP, DOWN, PAGE_UP, PAGE_DOWN. All other key events are passed to the jEdit text area unchanged. - Explicit completion via standard jEdit shortcut C+b, which has been remapped to action isabelle.complete (fall-back on regular complete-word for non-Isabelle buffers). - Implicit completion via keyboard input on text area, with popup or immediate insertion into buffer. - Implicit completion of plain words requires at least 3 characters (was 2 before). - Immediate completion ignores plain words; it requires 1 characters of symbol abbreviation to complete, otherwise fall-back on completion popup. - Isabelle Symbols are only completed in backslashed forms, e.g. \forall or \forall that both produce the Isabelle symbol \forall in its Unicode rendering. - Refined table of Isabelle symbol abbreviations (see $ISABELLE_HOME/etc/symbols). This refers to Isabelle/d0e4c8f73541. It is an intermediate somewhat stable stepping-stone -- it remains to be seen which of the other ideas on my list can be worked out before the release (it is getting quite close now). If there are any oddities in the new setup, or really bad things of the old one that are still there, please let me know about it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Popups in Java/Swing
This is a side-track of the completion (and tooltip renovation) story. After many years of struggling with various possibilities for popup windows in Java/Swing and their many portability problems (evil window managers etc.), I have recently tried the official http://docs.oracle.com/javase/7/docs/api/javax/swing/PopupFactory.html This is a short description as javadoc on the surface, but there are big and complex sources behind it: http://www.docjar.com/html/api/javax/swing/PopupFactory.java.html It seems to workaround various Swing design problems, with lots of explicit runtime matching of object types. Thus it works a bit better than plain JWindow, but Apple/Oracle managed to bomb that approach nonetheless (bad focus, no copy-paste). The result of studying the sources of javax.swing.PopupFactory to produce my own version is now this: http://isabelle.in.tum.de/repos/isabelle/file/31f956f42e8d/src/Tools/jEdit/src/popup.scala It is hard to tell if this is a joke or if it is funny. The main lesson learned concerning Java/Swing: * The smoking chimneys of javax.swing.PopupFactory won't do any good. * Plain javax.swing.JLayeredPane does all the work. Lets see if this is really the case -- in everyday use of the new completion mechanism (and tooltips) on all these exotic platforms. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] numpad doesn't work
On Thu, 29 Aug 2013, Ondřej Kunčar wrote: This refers to 3c26a7042d8e. The numpad stopped working in JEdit. Reproducible on my machine and also on Dmitriy's machine. We use Linux. What exactly means stopped working? Can you give another changeset where it still works, whatever that means here? Note that I have recently changed many Isabelle/jEdit keyboard shortcuts. This might cause some confusion with the persistent $ISABELLE_HOME_USER/jedit/keymaps/ -- deleting that directory makes a fresh start (and looses personal keybindings, if you have any). Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] numpad doesn't work
On 08/30/2013 02:21 PM, Makarius wrote: On Thu, 29 Aug 2013, Ondřej Kunčar wrote: This refers to 3c26a7042d8e. The numpad stopped working in JEdit. Reproducible on my machine and also on Dmitriy's machine. We use Linux. What exactly means stopped working? Can you give another changeset where it still works, whatever that means here? Note that I have recently changed many Isabelle/jEdit keyboard shortcuts. This might cause some confusion with the persistent $ISABELLE_HOME_USER/jedit/keymaps/ -- deleting that directory makes a fresh start (and looses personal keybindings, if you have any). Makarius What do I exactly mean? Let me tell you what the numpad is. It is a part of a keyboard and it has various keys. If you press one of the keys, you get a corresponding symbol in an input on your display. Usually the same symbol that is on the key. This is the only feature of the numpad that I know. And this is the feature that is broken: if I press a key from the numpad, I don't get any symbol on my display in the main editing area in JEdit. It doesn't work for me, Dmitriy, Jasmin, Tobias and Lars. That already means a couple of different systems: Linux (different distribution), Mac OS. Removing $ISABELLE_HOME_USER/jedit/keymaps/ didn't help. It still doesn't work in c31c0c311cf0. It works for example in ca237b9e4542. Just a personal question: did you try to use the numpad on your keyboard before you sent your reply? Ondrej ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] numpad doesn't work
On Fri, 30 Aug 2013, Ondřej Kunčar wrote: What do I exactly mean? Let me tell you what the numpad is. It is a part of a keyboard and it has various keys. If you press one of the keys, you get a corresponding symbol in an input on your display. A numpad is far more complex than that. It has various modifiers, and generally odd meaning of keys, with or without these modifiers. I have been through long struggles with key events on various systems, keyboards etc. Nothing what you think it is is actually there at the bottom. Key handling has become a big challange on modern computers. This is no joke at all. Just a personal question: did you try to use the numpad on your keyboard before you sent your reply? No. These days a numpad is relatively rare on keyboards. (I have one at the big laptop at home, but it has quite different behaviour than the more regular numpads on old-style stand-alone keyboards.) Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Improved completion mechanism
Dear Makarius, First note that for me keyboard input to Isabelle/jEdit typically hangs every 10 minutes or so, depending on how fast I type (but this is an old and known issue). In Isabelle2013 the completion popup was not triggered when deleting characters (with backspace). Now this is the case and it seems to cause more frequent hangs for me (since deleting is typically done very fast). Is this behavior intentional, and if yes, what is the gain? cheers chris On 08/30/2013 08:52 PM, Makarius wrote: * Improved completion mechanism, which is now managed by the Isabelle/jEdit plugin instead of SideKick. - Various Isabelle plugin options to control popup behaviour and immediate insertion into buffer. - Light-weight popup, which avoids explicit window (more reactive and more robust). Interpreted key events: TAB, ESCAPE, UP, DOWN, PAGE_UP, PAGE_DOWN. All other key events are passed to the jEdit text area unchanged. - Explicit completion via standard jEdit shortcut C+b, which has been remapped to action isabelle.complete (fall-back on regular complete-word for non-Isabelle buffers). - Implicit completion via keyboard input on text area, with popup or immediate insertion into buffer. - Implicit completion of plain words requires at least 3 characters (was 2 before). - Immediate completion ignores plain words; it requires 1 characters of symbol abbreviation to complete, otherwise fall-back on completion popup. - Isabelle Symbols are only completed in backslashed forms, e.g. \forall or \forall that both produce the Isabelle symbol \forall in its Unicode rendering. - Refined table of Isabelle symbol abbreviations (see $ISABELLE_HOME/etc/symbols). This refers to Isabelle/d0e4c8f73541. It is an intermediate somewhat stable stepping-stone -- it remains to be seen which of the other ideas on my list can be worked out before the release (it is getting quite close now). If there are any oddities in the new setup, or really bad things of the old one that are still there, please let me know about it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: re-checking of main buffer
Just an observation. Assuming that the grayish background highlighting really indicates prover activity in the background, I recently noticed that sometimes a re-check of the whole buffer is done in situations where this is (as far as I see) not necessary. For example, having lemma ... by auto lemma ... by auto when I select the second by auto (typically S+Home, since the courser is positioned directly behind it after just having typed it) and then replace the selected region by something different, the whole buffer is highlighted (thus re-chekced or re-parsed?). This is not the only such situation, but one that I could reproduce reliably. Note also that -- just making a subjective evaluation by feeling -- that this re-checking happens more frequently in a1cd4126a1c4 (and possibly earlier) than in Isabelle2013. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
