--- a/NEWS Sat Jun 28 15:35:30 2014 +0200
+++ b/NEWS Sat Jun 28 15:50:48 2014 +0200
@@ -46,62 +46,31 @@
separate environments. See also ~~/src/Tools/SML/Examples.thy for
some examples.
+* Updated and extended manuals: "codegen", "datatypes",
+"implementation", "jedit", "system".
+
*** 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.
-
- - Support for path completion within the formal text, based on
- file-system content.
-
- - 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.
+* Document panel: simplied interaction where every single mouse click
+(re)opens document via desktop environment or as jEdit buffer.
+
+* Support for Navigator plugin (with toolbar buttons).
+
+* Improved syntactic and semantic completion mechanism, with simple
+templates, completion language context, name-space completion,
+file-name completion, spell-checker completion.
+
+* Refined GUI popup for completion: more robust key/mouse event
+handling and propagation to enclosing text area -- avoid loosing
+keystrokes with slow / remote graphics displays.
+
+* Refined insertion of completion items wrt. jEdit text: multiple
+selections, rectangular selections, rectangular selection as "tall
+caret".
* Integrated spell-checker for document text, comments etc. with
-completion popup and context-menu. See also "Plugin Options /
-Isabelle / General / Spell Checker" for some system options.
+completion popup and context-menu.
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
Open text buffers take precedence over copies within the file-system.
@@ -109,9 +78,6 @@
* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
auxiliary ML files.
-* Document panel: simplied interaction where every single mouse click
-(re)opens document via desktop environment or as jEdit buffer.
-
* More general "Query" panel supersedes "Find" panel, with GUI access
to commands 'find_theorems' and 'find_consts', as well as print
operations for the context. Minor incompatibility in keyboard
@@ -125,11 +91,9 @@
process, without requiring old-fashioned command-line invocation of
"isabelle jedit -m MODE".
-* New panel: Simplifier trace. Provides an interactive view of the
-simplification process, enabled by the newly-introduced
-"simplifier_trace" declaration.
-
-* Support for Navigator plugin (with toolbar buttons).
+* New Simplifier Trace panel provides an interactive view of the
+simplification process, enabled by the "simplifier_trace" attribute
+within the context.
* More support for remote files (e.g. http) using standard Java
networking operations instead of jEdit virtual file-systems.