# HG changeset patch
# User wenzelm
# Date 1396293231 -7200
# Node ID 075397022503c83ddd78160541e0f6e9b866eac9
# Parent  bfd13102eb541fda5a9fc36b291a78aab07719f2
cumulative NEWS;

diff -r bfd13102eb54 -r 075397022503 NEWS
--- a/NEWS	Mon Mar 31 20:45:30 2014 +0200
+++ b/NEWS	Mon Mar 31 21:13:51 2014 +0200
@@ -43,25 +43,59 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
+* Improved syntactic and semantic completion mechanism:
+
+  - No completion for Isar keywords that have already been recognized
+    by the prover, e.g. ":" within accepted Isar syntax looses its
+    meaning as abbreviation for symbol "\<in>".
+
+  - Completion context provides information about embedded languages
+    of Isabelle: keywords are only completed for outer syntax, symbols
+    or antiquotations for languages that support them.  E.g. no symbol
+    completion for ML source, but within ML strings, comments,
+    antiquotations.
+
+  - Support for semantic completion based on failed name space lookup.
+    The error produced by the prover contains information about
+    alternative names that are accessible in a particular position.
+    This may be used with explicit completion (C+b) or implicit
+    completion after some delay.
+
+  - Semantic completions may get extended by appending a suffix of
+    underscores to an already recognized name, e.g. "foo_" to complete
+    "foo" or "foobar" if these are known in the context.  The special
+    identifier "__" serves as a wild-card in this respect: it
+    completes to the full collection of names from the name space
+    (truncated according to the system option "completion_limit").
+
+  - Syntax completion of the editor and semantic completion of the
+    prover are merged.  Since the latter requires a full round-trip of
+    document update to arrive, the default for option
+    jedit_completion_delay has been changed to 0.5s to improve the
+    user experience.
+
+  - Option jedit_completion_immediate may now get used with
+    jedit_completion_delay > 0, to complete symbol abbreviations
+    aggressively while benefiting from combined syntactic and semantic
+    completion.
+
+  - Support for simple completion templates (with single
+    place-holder), e.g. "`" for text cartouche, or "@{" for
+    antiquotation.
+
+  - Improved treatment of completion vs. various forms of jEdit text
+    selection (multiple selections, rectangular selections,
+    rectangular selection as "tall caret").
+
+  - More reliable treatment of GUI events vs. completion popups: avoid
+    loosing keystrokes with slow / remote graphics displays.
+
 * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
 Open text buffers take precedence over copies within the file-system.
 
 * Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
 auxiliary ML files.
 
-* Improved completion based on context information about embedded
-languages: keywords are only completed for outer syntax, symbols or
-antiquotations for languages that support them.  E.g. no symbol
-completion for ML source, but within ML strings, comments,
-antiquotations.
-
-* Semantic completions may get extended by appending a suffix of
-underscores to an already recognized name, e.g. "foo_" to complete
-"foo" or "foobar" if these are known in the context.  The special
-identifier "__" serves as a wild-card in this respect: it completes to
-the full collection of names from the name space (truncated according
-to the system option "completion_limit").
-
 * Document panel: simplied interaction where every single mouse click
 (re)opens document via desktop environment or as jEdit buffer.