Re: [isabelle] Two configuration questions

On Mon, 10 Feb 2014, Van Staden Stephan wrote:

2. Auto completion used to show a drop-down box with the sigma character
   when I typed "sig". Similarly, it used to show an existential
   quantifier when I typed "exists". This does not work anymore. How can
   I turn it on again?

The last two sentences are the typical user-reflex to get back to something familiar as quick as possible, and missing the main points of improvements that happened in the meantime.

Whenever there is a user-relevant change, the NEWS file is the first point to look. It is easily available via the Documentation panel, entry "NEWS", in particular it says:

  * Improved completion mechanism, which is now managed by the
  Isabelle/jEdit plugin instead of SideKick.  Refined table of Isabelle
  symbol abbreviations (see $ISABELLE_HOME/etc/symbols).

Moreover, it is vital to look around what is new, otherwise important NEWS are missed like this one:

  * New manual "jedit" for Isabelle/jEdit, see isabelle doc or
  Documentation panel.

That manual also has some section on completion, but it still demands some study and experimentation to see how the mechanism actually works. That time is well-invested, though, since typing stuff into the text-buffer is done all the time, and knowing its options and possibilities helps to become more productive.

That does not mean that it is the final word to completion in Isabelle/jEdit. I have already further ideas in the back-hand, and more might emerge from experience reports by people who have worked with it for some time, leaving old things behind and looking towards new things.


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