[isabelle-dev] NEWS: improved syntactic and semantic completion mechanism
makarius at sketis.net
Wed May 21 22:35:01 CEST 2014
On Wed, 21 May 2014, Lars Noschinski wrote:
> I have recently written some proof with some german plain text. This
> triggered a lot of completion popups, suggesting to correct german to
> english words (which is to be expected). Unfortunately, the completion
> popup does not disappear when I continue typing the next word. Then, at
> the end of the line, i press RETURN TAB (to get to the correct
> indentation level again) which then completes the word -- this seems to
> be timing related, as a single RETURN <pause> closes the completion
I did not see this so far, because I am using a different combination of
the many options and modes of completion. This is physics and not
mathematics, so it is inevitable to get odd effects.
The particular problem with spell-checking is that it combines the
machanics of syntactic and semantic completion. All this degenerates more
and more into a diffuse "do what I mean" mechanism, but MS might call it
As a counter-movement, see now:
date: Wed May 21 22:06:10 2014 +0200
spell-checker completion is restricted to explicit mode, to avoid odd
effects with immediate edits vs. delayed language context markup, and
occasional delays due to dictionary lookup of many variants;
Maybe that is better, but I need to type more text myself, to see how it
Concerning the missing German dictionary: it is easy to include additional
dictionaries as plain word lists. Users can do that via
JORTHO_DICTIONARIES in the settings environment.
If someone wants to prepare some high-quality dictionaries for inclusion
in the jortho component, e.g. from the aspell distribution or Libre
Office, I need a reproducible proof how they were composed. See also
$JORTHO_HOME/README for the English variants.
I could also need an expert on English languages, to say if the present
jortho-1.0-2 dictionaries actually make sense.
More information about the isabelle-dev