Re: [isabelle-dev] JEdit: type constraints no longer printed by default
There might be corner cases where the change of the display leads to odd effects. Are there concrete incidents already that need to be reconsidered before the release? We use Syntax.string_of_term when creating Isar proof scripts in Sledgehammer and rely on Type.contstraint to introduce type annotations in terms (this does not work with show_markup set to true). Also, we got the error Malformed YXML: multiple results in certain situations. Both problems are solved as of 0583db803066, simply by setting show_markup to false in Sledgehammer. Steffen ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] JEdit: type constraints no longer printed by default
In af8ecf09a58c, type constraints are no longer printed by default in JEdit:
ML {*
@{term f}
| Type.constraint @{typ nat = nat}
| Syntax.string_of_term @{context}
| writeln
*}
# f
Is this the intended behaviour? It used to be different a couple of month ago.
I don't know when it changed exacyly, but I think changeset a6814de45b69 might
be responsible for the change.
When setting show_markup to false, the behaviour is like it was in the past:
ML {*
@{term f}
| Type.constraint @{typ nat = nat}
| Syntax.string_of_term (@{context} | Config.put show_markup false)
| writeln
*}
# f∷nat ⇒ nat
Regards,
Steffen___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit: zoom with cmd++
The problem is still there on Mountain Lion with an American keyboard.
However, rebinding the kebyoard shortcut locally as you suggested does the
trick - thanks for the tip!
Here is an ugly hack (based on the KeyEventDemo you provided) that would solve
the problem:
KeyEvent e_ = null;
// pressing a key twice in 5 ms or less is probably impossible
final long eps = 5;
/** Handle the key pressed event from the text field. */
public void keyPressed(final KeyEvent e) {
final boolean process = e_ == null || e.getKeyCode() != e_.getKeyCode()
|| (e.getWhen() - e_.getWhen()) eps;
e_ = e;
if (process) {
displayInfo(e, KEY PRESSED: );
}
}
Steffen
On 07.01.2013, at 11:07, Makarius makar...@sketis.net wrote:
On Sat, 22 Dec 2012, Makarius wrote:
On Wed, 19 Dec 2012, Steffen Juilf Smolka wrote:
in a39250169636, it is possible to increase/decrease the font size in jedit
with cmd++/cmd+- on MacOS (probably ctrl++/ctrl+- on other
plattforms) (nice feature!). However, pressing cmd++ increases the font
size twice on my machine (cmd+- works fine).
That was one such convenience that I managed to get working after 20min
Windows and Linux, followed by 2 weeks of tinkering on Mac OS X. But that
is not finished yet, and there are remaining problems to treat CTRL, ALT,
COMMAND modifiers properly: it can cause duplication or triplication of key
events.
See also the mail thread on Mac OS X support on Oracle Java 7 that Fabian
Immler has started recently
http://sourceforge.net/mailarchive/message.php?msg_id=30165793
It touches some of the internal issues, including a slightly odd workaround
by myself to modify an older workaround to make it half-working again under
Java 7.
This needs more systematic investigation, by instrumenting the jEdit sources
to produce detailed traces for all critical points where the MacOSX specific
key handling happens. Then it needs to be compared for Java 6 vs. Java 7,
to reconstruct the ideas behind it, which nobody seems to remember on
jedit-devel.
I've spent yet more time on the Mac OS X keyboard problem, which resulted
in change 76ae4e6318fb so far -- you will need the jedit_build update from
the later e7b2cfcef94c to try it yourself.
This now works on all machines I had tried at that point: Windows + Linux +
Mac OS X Mountain Lion, all with German keyboard. Trying it again with Mac
OS X Snow Leopard and English keyboard, I still see the triplication of
COMMAND-EQUALS for the Meta + key, though. Testing that with the low-level
Java key handler that is attached here, it actually shows 3 KEY_PRESSED
events produced by jdk-7u9 on that machine.
So we should blame Oracle or Apple for that ...
If someone comes up with a workaround nonetheless, I will look at it once
more.
Note that by rebinding the keyboard shortcut yourself locally, it will turn
the 3 keystrokes happily into just one editor action.
MakariusKeyEventDemo.java
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] priority queues
Thanks. I used an ordered list as a temporary solution, but now replaced it with a table to avoid linear complexity (when adding new elements to the queue). Steffen On 24.10.2012, at 17:26, Lukas Bulwahn bulw...@in.tum.de wrote: I think priority queues are roughly ordered lists (the priority is the ordering). So, you could have a look at Pure/General/ord_list.ML Lukas On 10/24/2012 05:21 PM, Steffen Juilf Smolka wrote: Hi, is there an implementation of priority queues in the isabelle library? Steffen ___ 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
Re: [isabelle-dev] jEdit: tooltips don't have proper size
First the running gag on isabelle-dev: the new ... or the latest ... is
ill-defined. You have to refer to *the* changeset of the repository version
you are presently testing.
Sorry, I'll keep that in mind.
Concerning Source Code Pro font: I tried it some weeks ago when there was
an announcement somewhere, but dismissed it rather quickly. On JVM/Linux its
rendering quality appeared quite weak, and too many of our standard Isabelle
symbols are missing.
I'm quite happy with the font on MacOS, and the missing symbols haven't been a
problem so far since I usually work in ML{* *}. By the way, the tooltips are
really a great help when programming!
(This can be checked by opening $ISABELLE_HOME_USER/etc/symbols with
UTF-8-Isabelle encoding.)
Ah, good to know!
Steffen
On 27.10.2012, at 16:42, Makarius makar...@sketis.net wrote:
On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
It seems there is a little (but annoying) issue with the new tooltips in
Isabelle/jEdit when using a font other than IsabelleText. I'm using the
Source Code Pro font and the tooltips are always just a little too small so
that part of the text is hidden/cut off. Of course an easy fix would be to
go back to using IsabelleText...
First the running gag on isabelle-dev: the new ... or the latest ... is
ill-defined. You have to refer to *the* changeset of the repository version
you are presently testing.
Nonetheless, I can guess what you mean and to which version range it might
refer: something close to my own latest version of my laptop, which is
8b50286c36d3. (This reference here is important for the mail archive of the
list, because in some weeks or months nobody remembers what was current in
the past.)
These fine points of sizing the Rich_Text_Area are not fully worked out yet,
and the next release is still many weeks ahead.
I will take your observation is a slight increase of the priority to address
it before the release, but this is not sure since many really important
things still need to happen elsewhere.
Concerning Source Code Pro font: I tried it some weeks ago when there was
an announcement somewhere, but dismissed it rather quickly. On JVM/Linux its
rendering quality appeared quite weak, and too many of our standard Isabelle
symbols are missing. (This can be checked by opening
$ISABELLE_HOME_USER/etc/symbols with UTF-8-Isabelle encoding.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: tooltips don't have proper size
Hi, It seems there is a little (but annoying) issue with the new tooltips in Isabelle/jEdit when using a font other than IsabelleText. I'm using the Source Code Pro font and the tooltips are always just a little too small so that part of the text is hidden/cut off. Of course an easy fix would be to go back to using IsabelleText... Best Regards Steffen ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] priority queues
Hi, is there an implementation of priority queues in the isabelle library? Steffen ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
