[isabelle-dev] <-> and <-->

[Christian Sternagel]

+1 for <--> (since it would agree, as Tobias pointed out, with the 
established =>, ==>, ->, -->).

Concerning convenience of input and automatic replacement:

I would not use automatic replacement at all, since it is at least as 
often a problem as it is of help (e.g., ML code inside theories "=>" in 
case statements, the mentioned "~~/" for imports, and I am sure that 
there are many other examples [LaTeX inside @text blocks]).

Still it is very convenient if one can just type and does not have to 
click (or browse with the keyboard) any popups.

In jEdit you can do the following (see also 
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-November/msg00089.html 
):

Under "Plugins -> Plugin Options -> Sidekick -> General" set "Show 
completion popups where possible" and "Automatic completion popups get 
focus" and use "\n" as "Accept character for completion popup" and "" 
(the empty string) as "Accept characters to insert after completion".

The resulting behavior is as follows:
If you type faster than indicated by the "After popup trigger keystroke, 
wait (seconds)" option the text stays just as you type it (of course you 
can set this option such that the popup always appears).
Otherwise, the popup appears as soon as you have completed a symbol that 
can be replaced, e.g., "=>", and have waited long enough. If you want to 
replace the ASCII input by the first symbol (usually the one you want) 
you just have to type <enter>, if you want to stay with the ASCII 
variant just go along by typing either space (if the line still 
continues this is the natural thing to do) or pressing <escape> once.

This means that you just have to press 1 additional key (i.e., <enter>) 
when you want replacement and just keep on typing as usual otherwise (of 
course, you could as well reverse this behavior, as you prefer).

I found this setup rather convenient.

cheers

chris


On 04/18/2012 02:51 AM, Makarius wrote:
> On Tue, 17 Apr 2012, Alexander Krauss wrote:
>
>> On 04/17/2012 05:41 PM, Tobias Nipkow wrote:
>>> This is what I would call unwieldy: instead of typing<--> or<-> (and
>>> having them converted to the appropriate symbols) you always type<->,
>>> but then you have to select from a menue. I don't see the progress.
>>
>> Could not agree more. These arrows are very common, and I want to be
>> able to type them without menu interaction. The selection idea is the
>> equivalent of "instead of having to use the shift key, you simply type
>> the letter and then select from the menu whether you want the capital
>> or the small letter".
>>
>> Of course we should not forget that the eager replacement done by
>> PG/Emacs is also problematic: try to type ~~/src and see how many
>> keystrokes you need :-)
>
> We all know these bad jokes of both Emacs and jEdit. But the general
> problem of mathematical input has been studied by other people before --
> I often see snippets of that at the CICM conference. Even just for plain
> JVM-based IDE-style editing there are better solutions than the Sidekick
> popup that I am still using in Isabelle/jEdit (which was easy to set up
> in 30min).
>
> Anybody who feels like contributing constructively, should do a survey
> of the possibilities on the JVM platform and propose an suitable
> improvement of the Isabelle/jEdit completion mechanism. Ideally with a
> little Scala implementation.
>
>
> Concerning the situation in Isabelle/ProofGeneral right now: it is
> unmaintained so nothing can move there for this release.
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev