Email Gateway (Aug 18 2022 at 19:54): Email Gateway (Aug 18 2022 at 19:54):From: Timothy Bourke <tim@tbrk.org>
I was trying the jEdit interface in Isabelle 2012 for the first time
today. To me, the vision and its execution are superb.
But, I had one or two questions over very minor details:
I understand that the output panel synchronizes with the line
selected in the edit panel. But sometimes I seem to lose the goal
display when entering a new line.
For instance, if I type
lemma "A & B"
apply _^H
where ^H is a backspace, the goal is updated to:
Unknown proof method: "_"
Is something on my computer misconfigured? Should the current goal
(i.e., the one associated with the previous line) normally always
be visible when editing a subsequent line?
I had to manually add shortcuts for "-->" and "/\", but I noticed
that "and" at least works for the latter. Is this expected
behaviour? Are these new shortcuts recommended over the old ones?
Tim.
signature.asc
Email Gateway (Aug 18 2022 at 19:54):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Hi Timothy,
On 05/23/2012 03:23 PM, Timothy Bourke wrote:
I was trying the jEdit interface in Isabelle 2012 for the first time
today. To me, the vision and its execution are superb.But, I had one or two questions over very minor details:
I understand that the output panel synchronizes with the line
selected in the edit panel. But sometimes I seem to lose the goal
display when entering a new line.For instance, if I type
lemma "A& B"
apply _^Hwhere ^H is a backspace, the goal is updated to:
Unknown proof method: "_"
Is something on my computer misconfigured? Should the current goal
(i.e., the one associated with the previous line) normally always
be visible when editing a subsequent line?
This happens from time to time and has nothing to do with your computer.
The asynchronous document model is just a delicate matter, I would guess.I had to manually add shortcuts for "-->" and "/\", but I noticed
that "and" at least works for the latter. Is this expected
behaviour? Are these new shortcuts recommended over the old ones?
What exactly do you mean by "shortcuts". You can get most of the logical
symbols by just typing their ASCII approximation. As soon as the
approximation fits a symbol a popup will show up where you can choose
(maybe between several different symbols). E.g.,
After typing "-->" I have a popup containing just ⟶, and after typing /\
I get ∧. For some symbols there are also convenient
"word"-abbreviations, like "forall" for ∀ etc.
What do you mean by "and" works for the latter. The word "and" should
not expand to the symbol "∧".
cheers
chris
Email Gateway (Aug 18 2022 at 19:54):From: Timothy Bourke <tim@tbrk.org>
On May 23 at 16:41 +0900, Christian Sternagel wrote:
On 05/23/2012 03:23 PM, Timothy Bourke wrote:
- I had to manually add shortcuts for "-->" and "/\", but I noticed
that "and" at least works for the latter. Is this expected
behaviour? Are these new shortcuts recommended over the old ones?What exactly do you mean by "shortcuts". You can get most of the
logical symbols by just typing their ASCII approximation. As soon as
the approximation fits a symbol a popup will show up where you can
choose (maybe between several different symbols). E.g.,
After typing "-->" I have a popup containing just ⟶, and after
typing /\ I get ∧. For some symbols there are also convenient
"word"-abbreviations, like "forall" for ∀ etc.
Sorry, I meant "abbreviations". For --> and /\, it's possible that I
mixed something up.
What do you mean by "and" works for the latter. The word "and"
should not expand to the symbol "∧".
It does for me! (and also "or").
Tim.
signature.asc
Email Gateway (Aug 18 2022 at 19:54):From: Makarius <makarius@sketis.net>
The auto update follows the command span of the caret, which means the
user needs to know what a command span is (former PG users still do, but
it will soon be forgotten).
There are situations where the Output view does not follow as expected, it
requires a separate "Update" by the button. This is one of the many
boundary cases of the editor event model and the continous updates of the
prover document model disagree about the time/space continuum. There used
to be many NPEs from jEdit in the past, but a few anomalies are still left
over.
Above you probably have yet another boundary case: if the command is the
last one in the buffer, jEdit makes a special case for the text address in
the buffer -- it strips of the last newline. Thus your caret actually
points to nowhere, and the display is conservative in not updating itself.
In reality you usually have at least an 'end' command following.
In the next round if refinements, the relation of the Output panel(s) --
there can be multiple -- to the source needs to be made more explicit, and
the connection to editor events made more robust. Recently on Google maps
I've seen some nice ways to indicate the boundary of an area (municipality
etc.) as the search result. It should also be made easy to type in one
spot while watching output from another spot.
Makarius
Email Gateway (Aug 18 2022 at 19:54):From: Makarius <makarius@sketis.net>
jEdit has its own terminlogy here:
* "Shortcut" means command sequence to invoke an "action"; there is also
a tiny command line that can be opened via C-RETURN to retrieve
recent actions according to their name, not the key sequence.
Isabelle/jEdit provides very few shortcuts by default -- in jEdit it
is uncommon to have plugins define a lot of key sequences.
* "Abbreviation" is a mapping from certain word or symbolic text
fragments to arbitrary text. It is easy to add such abbreviations on
the fly, also in a mode-specific manner. There are separate key
sequences (jEdit actions) to define and use abbreviations.
Isabelle/jEdit does not do anything by default here. It is up to the
user to define jEdit abbreviations on demand.
* The Isabelle/jEdit completion popup works via the Sidekick plugin,
with special wiring to accomodate Isabelle symbols or keyword syntax.
See the Plugin options for Sidekick for a number of properties that
can be changed here.
The completion table is provided by Isabelle/Scala, also the
syntactic rules for word boundaries etc. Both the table of outer
syntax keywords and the information of etc/symbols are taken as a
starting point. For symbols you can complete the symbol name (e.g.
"forall"), actual symbol (e.g. "\<forall>") or optional symbol
abbreviation (e.g. "!"). There are some boundary cases when there is
an overlap with keywords, e.g. "and".
In principle you can define further symbol mappings and abbreviations in
ISABELLE_HOME_USER/etc/symbols, but some care is required to avoid
fundamental changes of the unicode rendering, otherwise copy-pasted
material cannot be exchanged with other people via email etc.
Makarius
Email Gateway (Aug 18 2022 at 19:55):From: Makarius <makarius@sketis.net>
Let's say it does not expand. I am unsure if it should or not. The
behaviour stems from the overlap of symbol name with outer keyword.
Anyway, completion should become more context sensitive at some point.
Within a term, "and" does not have any special meaning.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC