Email Gateway (Aug 22 2022 at 15:21): Email Gateway (Aug 22 2022 at 15:21):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Hi,
I have thought of a small feature for entering symbols. If you have a system
of theories with your own notation, you use a handful of symbols.
In the symbols windows, there could be a tab that shows your infix symbols,
but that would require to process the read theories, and a question would
arise: to what extent, down to the HOL library?
An easier solution would be to have a "recently used" tab in the symbols
window that would show the ones you started to use. It could ease entering
your own notation.
What do you think of this? Is there a builtin solution for this problem?
Email Gateway (Aug 22 2022 at 15:21):From: Lawrence Paulson <lp15@cam.ac.uk>
This sounds like a good idea to me, though I don’t know how difficult it would be to implement.
Larry
Email Gateway (Aug 22 2022 at 15:22):From: Makarius <makarius@sketis.net>
On 05/04/17 15:54, Gergely Buday wrote:
If you have a system
of theories with your own notation, you use a handful of symbols.In the symbols windows, there could be a tab that shows your infix symbols,
but that would require to process the read theories, and a question would
arise: to what extent, down to the HOL library?
Technically, it is very difficult to extract information from the inner
syntax in the IDE. E.g. what to do with local syntax in local contexts
(locales, bundles etc.)
In contrast, that is already supported for outer syntax: see the
explanation of 'abbrevs' in the NEWS and the isar-ref manual. This
allows some variants of "input methods" for theory libraries, but care
is required in designing abbreviations for important Isabelle sessions
(like HOL, HOL-Library etc.). Presently I use 'abbrevs' mainly for
isolated examples, e.g. when preparing exercise sessions with funny
syntax like a bold lambda.
An easier solution would be to have a "recently used" tab in the symbols
window that would show the ones you started to use. It could ease entering
your own notation.
Some "recently used" functionality is already available in the
completion dialog. This is relevant for highly ambiguous abbrevs such as
"<." and ".>" for exotic arrows.
It should be feasible to make a tab out of recently used abbrevs in the
Symbols panel, but I've not seen a need for that so far.
Specific notation often consists of more than one symbol, and the theory
'abbrevs' header addresses exactly that. Note that the "abbrevs" tab in
the Symbols panel is actually context-sensitive, depending on the theory
of the main text buffer.
Makarius
Last updated: Apr 18 2024 at 01:05 UTC