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 MHonArc.