[isabelle-dev] NEWS: improved syntactic and semantic completion mechanism

[Makarius]

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 
> popup.

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 
"intelli-sense".

As a counter-movement, see now:

changeset:   57051:5e30ffe79980
tag:         tip
user:        wenzelm
date:        Wed May 21 22:06:10 2014 +0200
files:       src/Tools/jEdit/src/completion_popup.scala
description:
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 
reacts.


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.


 	Makarius