Re: [isabelle] Symbol Shortcuts vs. LaTeX code



On Mon, 28 Apr 2014, Joachim Breitner wrote:

I’m currently in the phase where I make my theories nicely looking, and I’m adding text. This means that I’m writing LaTeX code in text {* .. *} blocks, and suddenly the automatic completion of abbreviations are very annoying: I can’t enter, say \cite{foo}, without getting ∘te{foo}.

In Isabelle2013-2 the completion mechanism still lacks any context, so what is good behaviour within the term language can easily become bad behaviour in LaTeX source.

Some weeks ago, I have revisited the whole complex of completion once again, and added a "language context" to address the above, but it is so smart that it has other side-effects. This will still take a few more weeks / months to consolidate for Isabelle2014 this summer.


Since this is (I believe) a common use case I wonder if I am overlooking something – can I make Isabelle/jEdit be smarter about this?

Depends how much you want to invest. The mechanism reacts on key events after filtering for the ones that insert plain text, ultimately it looks at the buffer content independently how that was produce. So if you can insert text without any critical key event, it will end up in the buffer without completion. You can see this with plain C+c to copy from the main cliboard register (there are several such registers). It does not help though, to insert a \ by special means and then continue typing normally.

Alternatively, you can undo the accidental completion of \ci and then continue typing, although there is an extra selection showing up that needs to be canceled via ESC first. (I need to check if this is normal jEdit behaviour, or an accident on the side of Isabelle/jEdit completion.)


I guess I can disable auto completion in the options, but that’s 6 mouse clicks in the midst of a keyboard-only workflow, so I’d consider that a work-around, no better than typing cite C-← \ C-).

It is sufficient to disable the option "jedit_completion_immediate". Then you still have the popup-TAB mechanism for the term language.

Further hints on shortening GUI access paths are available on this recent thread: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-April/msg00144.html

There might be even more possibilities via macros and/or BeanShell scripting, but I am myself not an expert of all jEdit features.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.