Email Gateway (Aug 19 2022 at 12:26): Email Gateway (Aug 19 2022 at 12:26):From: Joachim Breitner <breitner@kit.edu>
Hi,
do you really mean “composing”, in the sense of the Compose key, or
rather “dead” key?
For a dead key i would expect that <~><space> will print "~", not "~ " –
why do you need Ctrl-B? What OS by the way?
I have disabled dead keys and use the Compose Key
(https://en.wikipedia.org/wiki/Compose_key) so that <Compose><~><n>
yiels ñ. But that might not be an option if you have to enter a lot of
accents. In that case, you might want to customize jEdit, as suggested
by René¹².
Greetings,
Joachim
¹ Yes, that is <R><e><n><Compose><´><e>.
² No, ¹ is not <Compose><^><1>, although that works as well, but
<AltGr><1>
³ My <Compose> key is <Print>, which Thinkpads have for some reason
between the right AltGr and String. I enable that with
keycode 107 = Multi_key
in my ~/.Xmodmap.
signature.asc
Email Gateway (Aug 19 2022 at 12:26):From: René Neumann <rene.neumann@in.tum.de>
As a matter of fact: The Linux' XCompose input method [1] works fairly
well with Isabelle/jEdit. For example, I use my right windows key as
compose key, allowing me to use Compose + / + \ to enter ∧ in any text.
Same for Compose + g + a for α ... and many more.
Using this in Isabelle/jEdit yields the result I'd expected, i.e. no
visual difference to using jEdits abbreviations here.
Hence, in theory, a sophisticated user could have different levels of
input abbreviations (very often used ones: jEdit, not so often: Compose,
seldomly: explicit completion), where the first ones can even share the
same codes (f.ex. < + = for ≤ and Compose + < + = for ⇐ )
[1] I probably am using the wrong nomenclature here...
smime.p7s
Email Gateway (Aug 19 2022 at 12:26):From: Manuel Eberl <eberlm@in.tum.de>
Using a compose key is definitely a good way to just ignore jEdit's
completion. I have a customised .XCompose file that allows me to write
∀, ∃, ∈, ⟹, ⊆ and so on using the Compose key; this solution has the
advantage that it also works the same way outside of jEdit. I only just
realised that I could simply use my Compose key to solve the whole
Unicode token issue for me, maybe I should give jEdit another try.
Email Gateway (Aug 19 2022 at 12:26):From: Joachim Breitner <breitner@kit.edu>
Hi,
I just tried to switch to the GTK theme and it made the UI feel much
more sluggish. Maybe you can try the default Nimbus theme and compare?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:26):From: Makarius <makarius@sketis.net>
For completeness here are my own remaining reasons for Proof General,
which are really the last bits.
* Use of ispell to spell-check the "text" parts of theories (the
latex-oid formal source).
I think jEdit VoxSpell will do the job after some fine-tuning. In
particular the token language needs to be taken into account to
distinguish informal from formal text.
* Reformatting of plain ASCII or "text" parts with fill-paragraph.
It should be reasonably easy to reshape the jEdit action
format-paragraph to work more like the old Emacs operation. It
especially needs to distinuish a given margin for informal text vs.
the overall "wrap margin" of the source file.
From the above you can guess how I've edited the new Isabelle/jEdit manual
some weeks ago: using Proof General in offline mode.
Hopefully that was the last time that such oddities happened. Once that
the Isabelle document preparation system is integrated into
Isabelle/jEdit, there will be little reasons to look back on ancient
things anyway.
Makarius
Email Gateway (Aug 19 2022 at 12:26):From: Makarius <makarius@sketis.net>
It is new in Isabelle2013-1 as the NEWS tell.
(Arbitrary repository snapshots of Isabelle are off-topic on this mailing
list.)
Makarius
Email Gateway (Aug 19 2022 at 12:26):From: René Neumann <rene.neumann@in.tum.de>
Yeah, I have switched to Nimbus here. It still is not the most
responsive UI, but it is in an acceptable range.
Email Gateway (Aug 19 2022 at 12:26):From: Makarius <makarius@sketis.net>
A few more hints on SideKick in general. Its main purpose is to provide
some simple tree view on text buffers, depending on "edit mode" and
"sidekick parser".
For example, you can use the Documentation panel to open the Isabelle NEWS
file. Then you switch to SideKick and get some clickable outline of that
file, according to its structure.
Makarius
Email Gateway (Aug 19 2022 at 12:26):From: Joachim Breitner <breitner@kit.edu>
Hi,
additional fact: gtk (or GNOME?) disables the usual X11 provided compose
method (which is configurable and more extentensive) by a hard-coded
list which contains, for example ☭ and ¹, but not the ones you mention,
which is unfortunate. This can be overwritten (export
GTK_IM_MODULE="xim" ), but that had other side-effects which I don’t
recall at the moment.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:27):From: Makarius <makarius@sketis.net>
I usually use Nimbus -- it is a good compromise of performance vs.
look-and-feel quality. GTK+ is not only slow, but has occasional
dropouts, e.g. in ListView. The Color Picker is also not quite
up-to-date -- lacking important tabs.
The really old Metal L&F is even faster and more reliable, but is a bit
retro now.
The fastest L&F I've ever seen is native Windows, but native Mac OS X is
also OK.
Makarius
Email Gateway (Aug 19 2022 at 12:27):From: Manuel Eberl <eberlm@in.tum.de>
One rather annoying sideffect is that you cannot use Ctrl + Shift + U to
enter unicode symbols by their code point anymore. I have not yet found
a way to fix this, I use xim as well.
Email Gateway (Aug 19 2022 at 12:27):From: Makarius <makarius@sketis.net>
Here is a probably related note from the last section of the
Isabelle/jEdit manual:
\item \textbf{Problem:} Some Linux / X11 input methods such as IBus
tend to disrupt key event handling of Java/AWT/Swing.
\textbf{Workaround:} Do not use input methods, reset the environment
variable @{verbatim XMODIFIERS} within Isabelle settings (default in
Isabelle2013-1).
It has required almost 1 year until I managed to reproduce this myself and
to find an entry on the IBus tracker, which is still pending, I think.
(The IBus guy did not understand the source of the problem.)
So Linux input methods can be as hostile to Java as window managers. To
me that "platform" has become more and more like a freak show.
People who do have the ambition to iron out such snags, are especially
welcome to provide further hints to the jEdit guys at
http://sourceforge.net/projects/jedit/
My impression is that the quality and coverage is approx. 90% Windows, 9%
Mac OS X, 1% Linux. The little remains of the latter are then potentially
destroyed by Linux packagers (but Isabelle/jEdit does not depend on that).
Makarius
Email Gateway (Aug 19 2022 at 12:27):From: Makarius <makarius@sketis.net>
The non-handling of add-on files, especially ML ones, is one of the main
omissions from the past 5 years of Isabelle/jEdit. Just a few weeks ago,
while cycling through sunny Apulia, I've devised a reasonably simple way
to get there. Lets see if I manage for the next release.
The reason why its not there yet is indeed the coincidence that it mostly
affects people working on Isabelle/HOL itself, which are releatively few,
and it is a relatively tough job anyway. It does not mean that I am not
annoyed myself by the omission.
Some months ago, I had a different and quite pleasant experience with
Isabelle/ML development in Isabelle/jEdit. Doing just plain 'ML' sections
(to avoid the ML file problem) and some 'keywords' in the header, it was
really nice to work out some Isar commands. The only surprise was a
sudden breakdown due to an old version of the command still persisting
while the new version was malformed (rejected by the ML compiler).
The internal command table is still global for historic reasons (Proof
General legacy again) and poking into it can have unexpected effects.
Makarius
Email Gateway (Aug 19 2022 at 12:27):From: Peter Lammich <lammich@in.tum.de>
I just gave the jEdit in 2013-1 a try. Here are my first impressions:
* In PG, I have some open buffers, these are the buffers that I'm
interested in. jEdit opens all dependent theories (approx 50 to 100 in
my typical use-case). So using cycle-buffer or similar functions makes
no sense.
How can I efficiently switch between the theories that I'm currently
editing/interested in, without having to search them among dozens of
uninteresting theories?
* I have no control when theories are processed. I loaded a theory,
and saw in the theory-panel all these purple bars slowly disappearing,
until no purple was left. Also for the theory that was currently
displayed in the main window. However, the theory in the main window was
NOT completely processed. When moving down the cursor, the purple bar
appeared again.
So how can I be sure that my theories are all correct?
Email Gateway (Aug 19 2022 at 12:27):From: Makarius <makarius@sketis.net>
On Tue, 12 Nov 2013, Peter Lammich wrote:
- In PG, I have some open buffers, these are the buffers that I'm
interested in. jEdit opens all dependent theories (approx 50 to 100 in
my typical use-case). So using cycle-buffer or similar functions makes
no sense.How can I efficiently switch between the theories that I'm currently
editing/interested in, without having to search them among dozens of
uninteresting theories?
I've occasionally seen jEdit plugins to organize buffer groups or
"projects", but have not used any myself so far.
- I have no control when theories are processed. I loaded a theory, and
saw in the theory-panel all these purple bars slowly disappearing, until
no purple was left. Also for the theory that was currently displayed in
the main window. However, the theory in the main window was NOT
completely processed. When moving down the cursor, the purple bar
appeared again.
You can give some declarative hints in the "Theories" panel, namely for
global "Continuous checking" and individual "Mark as required for
continuous checking". There are also actions and keyboard shortcuts for
that.
To get a general overview of specific actions and shortcuts of
Isabelle/jEdit, you can go to "Global Options / Shortcuts / Edit
Shortcuts: Plugin: Isabelle".
So how can I be sure that my theories are all correct?
By making a batch build in the old-fashioned manner.
An approximation in Isabelle/jEdit is to look closely at the Theories
panel overview, but with hundreds of theories it might be a bit difficult.
What is missing here is a general "wrapup" of the editor session similar
to the batch build session. This non-uniformity is one of these spots
where Proof General legacy support is in the way.
You have already noticed a subtle breakdown in this department in one of
the release candidates. Doing things once right is better than doing it
3-4 times slightly differently (Isabelle/jEdit, isabelle build, Proof
General, TTY).
Makarius
Email Gateway (Aug 19 2022 at 12:28):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I use ProjectViewer as both a file manager and a project manager, either
of which lets you import folders, flattened or not flattened, or just
add specific files. It has features for projects I don't use yet, like
setting compile and run commands to be run in the console plugin.
ProjectViewer would let you group together a few files, from the 50 to
100, and switch back and forth between them by double-clicking on them
in the ProjectViewer tree.
http://plugins.jedit.org/plugins/?ProjectViewer
In the ProjectViewr panel "Folders" tab, you right-click on the "All
Projects" and click "Add project". A "Create New Project" window opens
where you can change different options, but the basics are a project
name and root directory.
You give the project a name and root directory and click "OK", after
which it takes you to an import window. In your case, if you don't want
to import the 100 files you don't care about, you would hit cancel, and
then add individual files, as I describe below.
At this point, I don't actually use it as a project manager most of the
time, so I right-click on the project name and select "Close group or
project".
Under "All Projects", I can right-click on a project name and "Re-import
files" or "Add files". If I've imported a folder, I can expand the tree
and right-click on a filename and select "Remove from project", but you
have to be careful, because "Delete from disk" is right under that command.
If you've right-clicked on a project name and selected "Open group or
project", then %p, $p, or %p% is the console path variable for the
project root folder. See "Help/jEdit Help/Plugins/Console" for more
details about Console and its interplay with jEdit and other plugins.
Like I say, I use it as a file manager, so I have files open from
different projects, where all project names show up below "All
Projects", because I don't have any project open.
So that it doesn't automatically close the files I want open all the
time, in "Plugin Options/Project Viewer/General Options", I uncheck both
"Close files on project change" and "Remember open project files".
Regards,
GB
Email Gateway (Aug 19 2022 at 12:28):From: Joachim Breitner <breitner@kit.edu>
Hi,
as a suggestion, would it be possible to decouple the question of
whether a theory appears in the Theories panel from the question of
whether a buffer exists for it?
In detail, given Theories A and B, where B imports A. If I import A.thy,
I will be asked if I want to load theory B as well. Obviously I press
Yes. Now B appears in the Theories panel, and will be processes as a
prerequisite for A, but the file B.thy will not be (visibly) opened.
If I now want to edit B.thy as well, I can either double-click on B in
the Theories panel, or File→Open it as usual. When I’m done with it, I
can even close it; it will stay in the Theories panel (as a dependency
of A).
This way, I have full control over what files I have open, and what I
can cycle with Ctrl-PgUp. In fact, I was expecting this behavior when I
first fired up jEdit. Possible, it could also speed up things, as no UI
elements would have be generated for the files that do not have buffers.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:29):From: Makarius <makarius@sketis.net>
That approach was basically at the very start of theory management some
years ago, but it did not work out on the spot so I made the explicit
flooding with jEdit buffers as intermediate solution. This worked better
than anticipated, which explains why it is still there in its relatively
crude way.
In the meantime isabelle build has become a formal part of Isabelle/Scala,
and various jEdit "project" facilities have emerged. So it all needs to
be all revisited to fit it nicely together, such that there is signicant
conceptual progress as well.
Makarius
Email Gateway (Aug 19 2022 at 12:52):From: Makarius <makarius@sketis.net>
On Mon, 11 Nov 2013, Andreas Lochbihler wrote:
People who are still using Proof General should say more explicitly what
are the reasons
for it, apart from old habits.
I use both jEdit and Proof General, but for different purposes. I see the
following advantages of ProofGeneral 3.7.1.1 with XEmacs:
With some years of delay, that is a start. I don't see any fundamental
problems in this list, just accidental behaviour which can be easily tuned
or done differently.
You know yourself that XEmacs / ProofGeneral 3.7.1.1 is totally obsolete.
Current GNU Emacs is at version 24 and Proof General 4.2. I wonder if
there are other remaining users of ProofGeneral 3.7.1.1.
With jEdit, I have to switch to the mouse far more often, in particular
for sledgehammer, find_theorems and to navigate from one theory file to
another.
jEdit has quite smart keyboard shortcuts for many things, but they are
usually quite different from Emacs. Switching files works via the "buffer
switcher", which is keyboard operable (a bit difficult on German layouts,
though). After several weeks of practice, operating jEdit should be much
faster than Emacs.
The Find and Sledgehammer panel are my own responsibility, and they are
new in Isabelle2013-1, so more refinements can be expected. There are
already jEdit actions to open the dockable windows, which also puts the
focus on the main GUI component to activate the tool in question via plain
RETURN. Note that jEdit "actions" can be mapped to keyboard shortcuts by
the user. This is not done by default, to avoid the "Escape Meta Alt
Control Shift" syndrome.
Similarly, I often want to look somewhere else in my theory file (and use
PgUp/PgDn for that); with ProofGeneral, I just type C-c C-. to get back to
where I was before, but I do not know an equally simple way in jEdit.
Isn't that just abuse of the accidental boundary between checked and
unchecked text? This "focus" no longer exists in Isabelle/jEdit anyway,
which is actually one of the main points of the whole approach.
What jEdit (or Isabelle/jEdit) really needs is nice navigation support in
the sense of Firefox or similar. One mainly needs to work out a good
scheme when or how to "commit" positions to the navigation history, and
maybe brush up the existing Navigator plugin.
- XEmacs has less spacing between the lines (this is the main reason why I
still use ProofGeneral 3.7.1.1, GNU Emacs with PG 4.x has a similar spacing
as jEdit), so more of the proof script fits on the screen at the same font
size.
That is a question about fonts. In principle you can use alternative
fonts in jEdit to your liking, although I consider IsabelleText the best
compromise for display quality and glyph coverage.
Note that jEdit has an option for extra vertical line spacing (Global
Options / Text Area). I've never used it myself, but it could work out
reasonably well. If not, it is relatively easy to tune that text
painting, because I am doing it all myself anyway.
In XEmacs you still have bitmap fonts. I wonder if/how it survives a
switch to high-definition displays that have become available in the mass
marked last year. Gladly, Oracle has already managed to catch up, notably
with Apple's Retina in Jdk-7u40, so jEdit is already beyond the dividing
line of current and obsolete applications. My cheap Sony HD display also
works nicely with jEdit fonts.
- The output buffers are not usable with a key board. This is
particularly annoying when I examine diagnostic output as produced by
code_thms, export_code, print_classes, thm <large Named_THM collection>,
etc. In jEdit, I first have to open a new buffer and copy the output
there before I can use search and friends to navigate through.
The Output panel is not a buffer at all, but a dockable window. It
re-uses some of the jEdit buffer display technology, but there is no
attempt to imitate Emacs where "everything is a buffer". The latter
approach sometimes has advantages, sometimes disadvantages. Like Proof
General stayed faithful how Emacs works, Isabelle/jEdit takes jEdit
customs seriously.
Searching in Output panels should not be a fundamental problem. It is
just one of the many small things that did not yet make into
Isabelle/jEdit, because time was spent instead to maintain Proof General.
- After a few hours of work, jEdit reacts slower and slower. This gets
particularly annoying when typing fast. For example, I want that
entering < = TAB produces the \<le> symbol, always. Half of the time, I
am faster than the popup and I get "<= " instead.
I have never heard of that. There might be a serious problem behind it
that needs to be investigated. Problems that are known can be solved
eventually. Secret ones will remain forever.
Makarius
Email Gateway (Aug 19 2022 at 12:52):From: Lawrence Paulson <lp15@cam.ac.uk>
You can put any number of marks in a file. They track edits quite well, and they persist over sessions.
Larry
Email Gateway (Aug 19 2022 at 12:52):From: Makarius <makarius@sketis.net>
Good point.
I am myself not yet aqcuainted with markers. Likewise multiple registers
for copy-paste. There is always something left to learn about jEdit.
Makarius
Email Gateway (Aug 19 2022 at 12:52):From: Makarius <makarius@sketis.net>
On Mon, 11 Nov 2013, René Neumann wrote:
Am 11.11.2013 12:34, schrieb Makarius:
People who are still using Proof General should say more explicitly what
are the reasons for it,I think, I had put it in another mail already, but well:
IIRC, that was for Isabelle2013. So for Isabelle/PIDE 3rd generation.
Now we have Isabelle2013-1 and the 4th generation.
One of the big differences to Proof General is that there are big
differences in each release cycle. You really need to look what is there
everytime afresh.
- jEdit is SLOW, as in: There is a noticeable lag when moving from one
menu to the other per mouse (rendering also consumes 50% to 100% of one
CPU).
What is your hardware like? I usually see 20% total time for the JVM and
approx. 400-800% for Isabelle/ML. That is an old 8 core machine from
2009.
Java has this odd feature that it sometimes "looks slow", but it actually
isn't.
Isabelle/jEdit was started in 2008 to make efficient use of current
hardware (2 cores or more).
- Fonts are not antialiased. I found that setting some obscure
environment variable [1] made it work, but honestly: no AA by default is
a no-go.
Obsolete in Isabelle2013-1 and hardly an issue before, since it was well
documented in the jEdit FAQ how to change such defaults.
- no switching of sessions (at least last time I checked)
Rarely needed, unless you make a convincing point for such a marginal
feature. In Isabelle/jEdit you can load disjoint sessions without
interfering each other.
Proof General legacy support is actually in the way to clean up all that
and make just one way of Isabelle build or Isabelle/jEdit with multiple
sessions.
- (obsolete: my WM fails to show jEdits dialogs. Just noticed that there
is a patch available for it).
What is your WM? There are many Linux guys who just don't want Java
applications on their particular fork. The solution is to use one of the
well-known standard window managers.
- jEdit is too mouse-centric. When I have to use "Ctrl-hover" to get
some information, I won't use it.
You don't even have this functionality in Proof General, so it is hardly
a remaining reason for Proof General.
Again: after some weeks of practice, you will be much faster with jEdit
than Emacs. I always feel encumbered when I have to go back to Emacs for
some reason.
- last time I checked, the 'abbreviation to unicode' conversion that
finally(!!) works great in PG, was somewhat unusable in jEdit.
Can you explain that feature of Proof General. I have never heard of it.
In Isabelle2013-1 the symbol completion mechanism has been generally
brushed up. Better forget what it was in Isabelle2013 or Proof General,
and experiment to see its possibilities. There is also some documentation
in the Isabelle/jEdit manual.
apart from old habits.
And this is also not to be underrated. Over the last two years, I have
compiled a 150 lines .emacs (and I'm only using Emacs for Isabelle) plus
some 'isabelle emacs' startup magic. Hence being urged to spend all this
time again to get the editor in a shape one likes, does not feel good.
Especially when there are NEWS items reading "you have to re-do all your
current jEdit keybinding customizations".
I can't do anything here. You need to be ready to give up old Emacs
things and move on to a brave new world. Isabelle/jEdit is not the
future, it is the present for quite some time already.
Makarius
Email Gateway (Aug 19 2022 at 12:52):From: René Neumann <rene.neumann@in.tum.de>
Am 11.11.2013 18:13, schrieb Makarius:
On Mon, 11 Nov 2013, René Neumann wrote:
Am 11.11.2013 12:34, schrieb Makarius:
People who are still using Proof General should say more explicitly what
are the reasons for it,I think, I had put it in another mail already, but well:
IIRC, that was for Isabelle2013. So for Isabelle/PIDE 3rd generation.
Now we have Isabelle2013-1 and the 4th generation.One of the big differences to Proof General is that there are big
differences in each release cycle. You really need to look what is there
everytime afresh.
- jEdit is SLOW, as in: There is a noticeable lag when moving from one
menu to the other per mouse (rendering also consumes 50% to 100% of
one CPU).What is your hardware like? I usually see 20% total time for the JVM
and approx. 400-800% for Isabelle/ML. That is an old 8 core machine
from 2009.
Quadcore i7. Which should be fast enough... I'm using the gtk-style for
jEdit. Or I would need a high-end GPU ... (intel-whatever here only).
New testing on a second machine (which is slower) does not yield any
lags. Strange. Have to investigate.
- Fonts are not antialiased. I found that setting some obscure
environment variable [1] made it work, but honestly: no AA by default
is a no-go.Obsolete in Isabelle2013-1 and hardly an issue before, since it was well
documented in the jEdit FAQ how to change such defaults.
Thanks. This indeed does work now.
- no switching of sessions (at least last time I checked)
Rarely needed, unless you make a convincing point for such a marginal
feature. In Isabelle/jEdit you can load disjoint sessions without
interfering each other.Proof General legacy support is actually in the way to clean up all that
and make just one way of Isabelle build or Isabelle/jEdit with multiple
sessions.
My use case: Using PG with session X. Then noticing that I had to change
some theory in X. With session switching this was easy: Exit Isabelle,
switch session, restart isabelle (thereby building all of session X, but
for development this is ok).
With jEdit I would have to restart the editor.
- (obsolete: my WM fails to show jEdits dialogs. Just noticed that there
is a patch available for it).What is your WM?
i3
There are many Linux guys who just don't want Java
applications on their particular fork. The solution is to use one of
the well-known standard window managers.
That's not a solution, but a workaround (I'm using the WM I'm using for
good reasons). The problem is not the WM, but Java, as it changed
behavior in Java7 and a new workaround in the WM had to be developed
(again: why Java is not just using existing techniques/libraries and is
doing everything from scratch itself, I do not understand).
But as already written: This problem is obsolete until the next JDK version.
- last time I checked, the 'abbreviation to unicode' conversion that
finally(!!) works great in PG, was somewhat unusable in jEdit.Can you explain that feature of Proof General. I have never heard of it.
Typing e.g. /\ and getting \<and>, or |/ and getting \<^sub>.
But I just ran a fresh download on a previously isabelle-free computer
and it looked better than expected. Hence I'll give it a fresh try at
work (after having patched by WM) and will come back tomorrow (I'll also
ditch the gtk-style)
Email Gateway (Aug 19 2022 at 12:53):From: Makarius <makarius@sketis.net>
On Mon, 11 Nov 2013, René Neumann wrote:
Quadcore i7. Which should be fast enough... I'm using the gtk-style for
jEdit. Or I would need a high-end GPU ... (intel-whatever here only).
The hardware is OK. Since this is Intel hyperthreading, you might want to
experiment with explicit option threads=4 instead of the default 8.
Running on Linux, you can spoil the performance game by graphics drivers,
or other Gtk-specific oddities that I can't pin down. Java/Swing
applications only work well on a moderately configured mainstream Linux
systems. Being aggressively Linux-oid spoils the game. OpenJdk also does
not really help in this respect (the code base is mostly the same as
Oracle's Jdk).
Users of Windows and Mac OS X have an inherent advantage here.
- (obsolete: my WM fails to show jEdits dialogs. Just noticed that there
is a patch available for it).What is your WM?
i3
Never heard of that. Consider it unsupported.
There are many Linux guys who just don't want Java applications on
their particular fork. The solution is to use one of the well-known
standard window managers.That's not a solution, but a workaround (I'm using the WM I'm using for
good reasons). The problem is not the WM, but Java, as it changed
behavior in Java7 and a new workaround in the WM had to be developed
(again: why Java is not just using existing techniques/libraries and is
doing everything from scratch itself, I do not understand).
This is a very old argument of WM guys versus Java guys. They hate each
other for that and accuse the other side of being wrong.
I've recently done some research of relevant AWT sources and corresponding
OpenJdk mailing list threads. I can't tell if and when the situation will
improve. Oracle is fighting at too many fronts at the same time.
For Isabelle/jEdit, I declare this issue as off-topic. Users need to use
a well-known WM -- or join the OpenJdk project to solve the problem
themselves.
- last time I checked, the 'abbreviation to unicode' conversion that
finally(!!) works great in PG, was somewhat unusable in jEdit.Can you explain that feature of Proof General. I have never heard of it.
Typing e.g. /\ and getting \<and>, or |/ and getting \<^sub>.
The completion mechanism of Isabelle2013-1 works quite nicely with such
things. I've spent several weeks just on these details.
Makarius
Email Gateway (Aug 19 2022 at 12:53):From: René Neumann <rene.neumann@in.tum.de>
- (obsolete: my WM fails to show jEdits dialogs. Just noticed that
there
is a patch available for it).What is your WM?
i3
Never heard of that. Consider it unsupported.
I never expected it to be supported. Supporting more than the very
mainstream software systems would be a nightmare, that I understand.
But please also allow me to ignore any 'only supported on'-disclaimers
(else I had a problem with many things).
There are many Linux guys who just don't want Java applications on
their particular fork. The solution is to use one of the well-known
standard window managers.That's not a solution, but a workaround (I'm using the WM I'm using
for good reasons). The problem is not the WM, but Java, as it changed
behavior in Java7 and a new workaround in the WM had to be developed
(again: why Java is not just using existing techniques/libraries and
is doing everything from scratch itself, I do not understand).This is a very old argument of WM guys versus Java guys. They hate each
other for that and accuse the other side of being wrong.
To be honest, the WM guys in question (ie i3 devs) never blamed anyone
in this particular case. It's just that such issues need their time to
be discovered and fixed.
For Isabelle/jEdit, I declare this issue as off-topic. Users need to
use a well-known WM -- or join the OpenJdk project to solve the problem
themselves.
I've never thought Isabelle to be the one in charge here. That's why I,
after noticing this issue, opened a bug report on i3 [1] (a workaround
in the WM is easier than a fix in the JDK). It still counted as a
show-stopper for me regarding jEdit, though. (Which already got fixed, I
just included it in the email (marked 'obsolete'!) as I talked about
this with other users last Friday and wanted my list to be complete :)).
[1] http://bugs.i3wm.org/report/ticket/1069
Email Gateway (Aug 19 2022 at 12:53):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
On 12/11/13 09:17, René Neumann wrote:
- (obsolete: my WM fails to show jEdits dialogs. Just noticed that
there
is a patch available for it).What is your WM?
i3
Never heard of that. Consider it unsupported.
I never expected it to be supported. Supporting more than the very
mainstream software systems would be a nightmare, that I understand.
But please also allow me to ignore any 'only supported on'-disclaimers
(else I had a problem with many things).
I too use PG due to incompatibility between jEdit and my window manager
(Xmonad within Gnome Classic). Like René, I accept that this is a
Java-WM problem, not an Isabelle problem. I'm not really wed to any part
of my software stack so when PG truly stops working I'll make the call
to switch WMs or run jEdit in a VM.
There are many Linux guys who just don't want Java applications on
their particular fork. The solution is to use one of the well-known
standard window managers.That's not a solution, but a workaround (I'm using the WM I'm using
for good reasons). The problem is not the WM, but Java, as it changed
behavior in Java7 and a new workaround in the WM had to be developed
(again: why Java is not just using existing techniques/libraries and
is doing everything from scratch itself, I do not understand).This is a very old argument of WM guys versus Java guys. They hate each
other for that and accuse the other side of being wrong.To be honest, the WM guys in question (ie i3 devs) never blamed anyone
in this particular case. It's just that such issues need their time to
be discovered and fixed.For Isabelle/jEdit, I declare this issue as off-topic. Users need to
use a well-known WM -- or join the OpenJdk project to solve the problem
themselves.I've never thought Isabelle to be the one in charge here. That's why I,
after noticing this issue, opened a bug report on i3 [1] (a workaround
in the WM is easier than a fix in the JDK). It still counted as a
show-stopper for me regarding jEdit, though. (Which already got fixed, I
just included it in the email (marked 'obsolete'!) as I talked about
this with other users last Friday and wanted my list to be complete :)).
- René
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 12:53):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
if it is in interests, here are the reasons why I do not use jEdit:
Automatic Processing
By this I mean that jEdit always processes the proof text at the cursor
position. I know this is supposed to be a feature of jEdit, but I just
find it annoying. I like my prover to be in a fixed state that I can
alter when I want to. Particularly when you have proof text that takes a
long time to process (e.g. due to large terms, I had that in programme
refinement a lot), one does not want jEdit to keep processing stuff that
it should leave alone for the moment.
Unicode Tokens
In Proof General, I type "ALL" and I get a "∀". In jEdit, I type "all",
I get an annoying popup and have to confirm my choice with a key press.
I have tried to get used to this, but I cannot, even after setting the
popup delay to 0 and adding Space and Tab as keys for confirming the
currently selected symbol. This is particularly tedious if one types a
sequence of symbols. In a way, I feel that users who /know/ their
unicode token names by heart are slowed down by unnecessary GUI (the
popup). I'd like to be able to switch it off and fall back to a Proof
General-like mechanism where I can type "ALL", "==>" and "\<alpha>" and
they are immediately converted to the corresponding Unicode token.
I could probably live with the first "problem"; but the second one is
really annoying; I just find that it slows down the speed at which I can
write proofs to great extent.
I am no friend of emacs and Proof General certainly has its problem, so
I have tried to switch to jEdit twice in the past, but the above two
things and the crashes and lags have led me back to Proof General; maybe
these are fixed now and I should try it again.
In this context, what is the point of "Sidekick"? It displays every
"have", every "using", every "by" as a single node?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 12:53):From: René Neumann <rene.neumann@in.tum.de>
This is what I meant in my email with this blurb about 'unicode'.
Email Gateway (Aug 19 2022 at 12:54):From: René Neumann <rene.neumann@in.tum.de>
Plugin Options -> Isabelle -> General -> Completion Immediate
Note to self: RTFM before complaining :)
Email Gateway (Aug 19 2022 at 12:54):From: Manuel Eberl <eberlm@in.tum.de>
I must admit I did not know about this option before; it must be rather
new. However, the behaviour is… odd. It seems to complete as soon as
there is only one alternative left, i.e. "\alp" is turned into "α".
"\ta" is turne into "τ". When one types "\alpha", one gets "αha", when
one types "\tau", one gets "τu". So basically, if one wants to use this
feature, one has to remember what part of the abbreviation will lead to
there being only one possibly completion.
That is not exactly what I had in mind.
(On a related note, I also found that jEdit was quite slow; it takes
over a minute to start up on my laptop; Proof General is /much/ faster.)
Email Gateway (Aug 19 2022 at 12:54):From: Joachim Breitner <breitner@kit.edu>
Hi,
I believe that that will soon enter your procedural memory. I also just
recently switched on this feature and from time to time write Γma, but
it becomes less often quickly. With this, entering fancy symbols becomes
quite nice.
There is still the problem that it relies on unique completions, and
some symbols don’t have short unique prefixes, e.g. \sqsubsete is not a
great win – but then, this symbol has [=, so I just have to get used to
that.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:54):From: Manuel Eberl <eberlm@in.tum.de>
Another problem are codes such as "not", which are still not replaced at
all, since "notation", "note" and so on also exist. I'm afraid I don't
think I can get used to this.
Email Gateway (Aug 19 2022 at 12:54):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Makarius,
I still find myself using Proof General on a daily basis. The main reason for this is that it's much easier to reload ML code in PG than in jEdit. Here's a typical scenario. Suppose I want to debug a failure in "primcorec". Then I do the following:
Open a "Scratch" theory by starting PG with -l HOL-Cardinals (the base image of BNF).
Import "~~/src/HOL/BNF/BNF_GFP" and write a small example that reproduces the problem in "Scratch".
Add debugging commands, fix bugs, etc., in the ML files loaded (directly or indirectly) by "BNF_GFP" using some other editor.
Unprocess and reprocess "Scratch".
Repeat steps 3 and 4 dozens of times.
Isabelle/PG was good at reloading exactly those theories that need to be reloaded, without baby sitting. Trying to achieve the same in jEdit requires a lot of clicking and a bit of thinking (to figure which .thy file has the right "ML_file" command).
I understand my use case is not typical for most users, who do not spend their days writing long pieces of ML code, and I can live with PG to do that. Still, it would be nice if jEdit/PIDE, which is otherwise so smart about so many Isabelle specifics, would reach the level of PG on this one point.
Jasmin
Email Gateway (Aug 19 2022 at 12:54):From: Makarius <makarius@sketis.net>
Have you actually tried Isabelle2013-1 already?
It requires some time to study the NEWS and the corresponding
documentatation (the jedit) manual. And then make a fresh start into this
4th generation Prover IDE implementation.
Makarius
Email Gateway (Aug 19 2022 at 12:54):From: Makarius <makarius@sketis.net>
There is no big point and it can be simply ignored. In 2010 I've made
some quick attempts to wire up Isabelle/jEdit with this generic jEdit
plugin and I did not find time yet to make it more serious. Its main
function at the moment is to provide some outline for section headings.
Occasional unfinished things are no remaining reason for Proof General,
especially since Proof General has nothing like SideKick at all.
I did make the completion serious in Isabelle2013-1, and it is no longer
using SideKick.
Makarius
Email Gateway (Aug 19 2022 at 12:54):From: Joachim Breitner <breitner@kit.edu>
Hi,
for not, I use ~<TAB>. Not consistent with the others, but still fast.
In any case I believe that jEdit is an editor capable of suiting most
uses when it comes to abbreviations, navigation etc. It surely takes
time to find out how things work, and even more how to change the
behavior if it does not work as intended, and what fancy plugins are
available.
Ideally most of the issues that we discussed in this thread about
symbols are actually independent from whether we edit Isabelle theories
or love letters (\he gives ♡ ;-)), so that we can use upstream resources
when solving them.
I’m not sure if this is actually the case, though, as I cannot tell
which editing features are provided by jEdit by default, which are
provided by jEdit but instrumented and configured using the Isabelle
plugin, and which are genuine Isabelle plugin features.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:55):From: bnord <bnord01@gmail.com>
Maybe I'm to stupid.
I find the "not" case still unpleasant.
I can't use "~<TAB>" because it's a composing key so I have to type
"~<space>C-b<TAB>"
"\not" is not unique so have to also press Tab
Benedikt
Email Gateway (Aug 19 2022 at 12:55):From: Makarius <makarius@sketis.net>
On Tue, 12 Nov 2013, Joachim Breitner wrote:
I believe that that will soon enter your procedural memory. I also just
recently switched on this feature and from time to time write Γma, but
it becomes less often quickly. With this, entering fancy symbols becomes
quite nice.
That is sophistication level 1.
There is still the problem that it relies on unique completions, and
some symbols don’t have short unique prefixes, e.g. \sqsubsete is not a
great win – but then, this symbol has [=, so I just have to get used to
that.
At sophistication level 2 you can experiment with your own symbol
abbreviations, by imitating / overriding some entries of
$ISABELLE_HOME/etc/symbols with your own entries in
$ISABELLE_HOME_USER/etc/symbols.
There is an art to make certain groups of symbols non-unique on purpose to
provoke a popup, while others are unique for immediate insertion.
I've played this game at the end of the summer, until I was myself
satisfied with 2-3 rounds of refinement. In the whole history of Isabelle
and Proof General, I have never been that fast typing certain formal
texts. Even more brevity and immediacity of completion is conceivable,
but my next priority is to make context-sensitive completion based on
information by the prover.
I had some concrete ideas how to approach this delicate problem at the end
of the summer, but then got stuck with too many GUI reactivity problems.
You have seen the last bits of that with the key event loss at extreme
typing speed. (Next time I simply avoid switching GUI focus for
completion; it will only require the usual 2-3 weeks of testing to
stabilize again.)
Makarius
Email Gateway (Aug 19 2022 at 12:55):From: René Neumann <rene.neumann@in.tum.de>
You can define your own abbreviations. F.ex. -, for ¬ :)
Do this by putting the following into ~/.isabelle/etc/symbols
\<not> code: 0x0000ac group: logic abbrev: -,
smime.p7s
Email Gateway (Aug 19 2022 at 12:55):From: Makarius <makarius@sketis.net>
On Tue, 12 Nov 2013, Joachim Breitner wrote:
Ideally most of the issues that we discussed in this thread about
symbols are actually independent from whether we edit Isabelle theories
or love letters (\he gives ♡ ;-)), so that we can use upstream
resources when solving them.
This is an important observation. The new Isabelle/jEdit manual describes
the situation as follows:
\medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
could delegate the problem to produce Isabelle symbols in their
Unicode rendering to the underlying operating system and its
\emph{input methods}. Regular jEdit also provides various ways to
work with \emph{abbreviations} to produce certain non-ASCII
characters. Since none of these standard input methods work
satisfactorily for the mathematical characters required for
Isabelle, various specific Isabelle/jEdit mechanisms are provided.
I’m not sure if this is actually the case, though, as I cannot tell
which editing features are provided by jEdit by default, which are
provided by jEdit but instrumented and configured using the Isabelle
plugin, and which are genuine Isabelle plugin features.
The new manual should give some impression what is jEdit and what is
Isabelle/jEdit. It is the first go on such a manual, though, and many
fine points might be missing or difficult to understand.
Makarius
Email Gateway (Aug 19 2022 at 12:55):From: Makarius <makarius@sketis.net>
Looks like the usual confusion due to platform-specific and/or national
keyboard layouts. E.g. on a German Mac it is really hard to type many
basic things. It routinely requires some re-adjustments in one of five
possible departments.
For ¬ in particular, note that it is a plain-old ISO-LATIN-1 character.
Many keyboard layouts have a relatively direct path to it.
Makarius
Last updated: Apr 25 2024 at 01:08 UTC