updated NEWS -- removed material that is already in the manual;
authorwenzelm
Sat Jun 28 15:50:48 2014 +0200 (2014-06-28)
changeset 5742396f970d1522b
parent 57422 2f4948579905
child 57424 966b12f636b9
updated NEWS -- removed material that is already in the manual;
NEWS
     1.1 --- a/NEWS	Sat Jun 28 15:35:30 2014 +0200
     1.2 +++ b/NEWS	Sat Jun 28 15:50:48 2014 +0200
     1.3 @@ -46,62 +46,31 @@
     1.4  separate environments.  See also ~~/src/Tools/SML/Examples.thy for
     1.5  some examples.
     1.6  
     1.7 +* Updated and extended manuals: "codegen", "datatypes",
     1.8 +"implementation", "jedit", "system".
     1.9 +
    1.10  
    1.11  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.12  
    1.13 -* Improved syntactic and semantic completion mechanism:
    1.14 -
    1.15 -  - No completion for Isar keywords that have already been recognized
    1.16 -    by the prover, e.g. ":" within accepted Isar syntax looses its
    1.17 -    meaning as abbreviation for symbol "\<in>".
    1.18 -
    1.19 -  - Completion context provides information about embedded languages
    1.20 -    of Isabelle: keywords are only completed for outer syntax, symbols
    1.21 -    or antiquotations for languages that support them.  E.g. no symbol
    1.22 -    completion for ML source, but within ML strings, comments,
    1.23 -    antiquotations.
    1.24 -
    1.25 -  - Support for semantic completion based on failed name space lookup.
    1.26 -    The error produced by the prover contains information about
    1.27 -    alternative names that are accessible in a particular position.
    1.28 -    This may be used with explicit completion (C+b) or implicit
    1.29 -    completion after some delay.
    1.30 -
    1.31 -  - Semantic completions may get extended by appending a suffix of
    1.32 -    underscores to an already recognized name, e.g. "foo_" to complete
    1.33 -    "foo" or "foobar" if these are known in the context.  The special
    1.34 -    identifier "__" serves as a wild-card in this respect: it
    1.35 -    completes to the full collection of names from the name space
    1.36 -    (truncated according to the system option "completion_limit").
    1.37 -
    1.38 -  - Syntax completion of the editor and semantic completion of the
    1.39 -    prover are merged.  Since the latter requires a full round-trip of
    1.40 -    document update to arrive, the default for option
    1.41 -    jedit_completion_delay has been changed to 0.5s to improve the
    1.42 -    user experience.
    1.43 -
    1.44 -  - Option jedit_completion_immediate may now get used with
    1.45 -    jedit_completion_delay > 0, to complete symbol abbreviations
    1.46 -    aggressively while benefiting from combined syntactic and semantic
    1.47 -    completion.
    1.48 -
    1.49 -  - Support for simple completion templates (with single
    1.50 -    place-holder), e.g. "`" for text cartouche, or "@{" for
    1.51 -    antiquotation.
    1.52 -
    1.53 -  - Support for path completion within the formal text, based on
    1.54 -    file-system content.
    1.55 -
    1.56 -  - Improved treatment of completion vs. various forms of jEdit text
    1.57 -    selection (multiple selections, rectangular selections,
    1.58 -    rectangular selection as "tall caret").
    1.59 -
    1.60 -  - More reliable treatment of GUI events vs. completion popups: avoid
    1.61 -    loosing keystrokes with slow / remote graphics displays.
    1.62 +* Document panel: simplied interaction where every single mouse click
    1.63 +(re)opens document via desktop environment or as jEdit buffer.
    1.64 +
    1.65 +* Support for Navigator plugin (with toolbar buttons).
    1.66 +
    1.67 +* Improved syntactic and semantic completion mechanism, with simple
    1.68 +templates, completion language context, name-space completion,
    1.69 +file-name completion, spell-checker completion.
    1.70 +
    1.71 +* Refined GUI popup for completion: more robust key/mouse event
    1.72 +handling and propagation to enclosing text area -- avoid loosing
    1.73 +keystrokes with slow / remote graphics displays.
    1.74 +
    1.75 +* Refined insertion of completion items wrt. jEdit text: multiple
    1.76 +selections, rectangular selections, rectangular selection as "tall
    1.77 +caret".
    1.78  
    1.79  * Integrated spell-checker for document text, comments etc. with
    1.80 -completion popup and context-menu.  See also "Plugin Options /
    1.81 -Isabelle / General / Spell Checker" for some system options.
    1.82 +completion popup and context-menu.
    1.83  
    1.84  * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
    1.85  Open text buffers take precedence over copies within the file-system.
    1.86 @@ -109,9 +78,6 @@
    1.87  * Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
    1.88  auxiliary ML files.
    1.89  
    1.90 -* Document panel: simplied interaction where every single mouse click
    1.91 -(re)opens document via desktop environment or as jEdit buffer.
    1.92 -
    1.93  * More general "Query" panel supersedes "Find" panel, with GUI access
    1.94  to commands 'find_theorems' and 'find_consts', as well as print
    1.95  operations for the context.  Minor incompatibility in keyboard
    1.96 @@ -125,11 +91,9 @@
    1.97  process, without requiring old-fashioned command-line invocation of
    1.98  "isabelle jedit -m MODE".
    1.99  
   1.100 -* New panel: Simplifier trace.  Provides an interactive view of the
   1.101 -simplification process, enabled by the newly-introduced
   1.102 -"simplifier_trace" declaration.
   1.103 -
   1.104 -* Support for Navigator plugin (with toolbar buttons).
   1.105 +* New Simplifier Trace panel provides an interactive view of the
   1.106 +simplification process, enabled by the "simplifier_trace" attribute
   1.107 +within the context.
   1.108  
   1.109  * More support for remote files (e.g. http) using standard Java
   1.110  networking operations instead of jEdit virtual file-systems.