Re: [isabelle] jEdit: cursor movement and goal display
On Wed, 23 May 2012, Timothy Bourke wrote:
On May 23 at 16:41 +0900, Christian Sternagel wrote:
On 05/23/2012 03:23 PM, Timothy Bourke wrote:
2. 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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and