NEWS

 Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
 and 'SML_export' allow to exchange toplevel bindings between the two
 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.
 
 * 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
 shortcuts etc.: replace action isabelle-find by isabelle-query.

 * Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
 General") allows to specify additional print modes for the prover
 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.
 
 * Improved Console/Scala plugin: more uniform scala.Console output,