NEWS
changeset 56342 075397022503
parent 56303 4cc3f4db3447
child 56369 2704ca85be98
     1.1 --- a/NEWS	Mon Mar 31 20:45:30 2014 +0200
     1.2 +++ b/NEWS	Mon Mar 31 21:13:51 2014 +0200
     1.3 @@ -43,25 +43,59 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 +* Improved syntactic and semantic completion mechanism:
     1.8 +
     1.9 +  - No completion for Isar keywords that have already been recognized
    1.10 +    by the prover, e.g. ":" within accepted Isar syntax looses its
    1.11 +    meaning as abbreviation for symbol "\<in>".
    1.12 +
    1.13 +  - Completion context provides information about embedded languages
    1.14 +    of Isabelle: keywords are only completed for outer syntax, symbols
    1.15 +    or antiquotations for languages that support them.  E.g. no symbol
    1.16 +    completion for ML source, but within ML strings, comments,
    1.17 +    antiquotations.
    1.18 +
    1.19 +  - Support for semantic completion based on failed name space lookup.
    1.20 +    The error produced by the prover contains information about
    1.21 +    alternative names that are accessible in a particular position.
    1.22 +    This may be used with explicit completion (C+b) or implicit
    1.23 +    completion after some delay.
    1.24 +
    1.25 +  - Semantic completions may get extended by appending a suffix of
    1.26 +    underscores to an already recognized name, e.g. "foo_" to complete
    1.27 +    "foo" or "foobar" if these are known in the context.  The special
    1.28 +    identifier "__" serves as a wild-card in this respect: it
    1.29 +    completes to the full collection of names from the name space
    1.30 +    (truncated according to the system option "completion_limit").
    1.31 +
    1.32 +  - Syntax completion of the editor and semantic completion of the
    1.33 +    prover are merged.  Since the latter requires a full round-trip of
    1.34 +    document update to arrive, the default for option
    1.35 +    jedit_completion_delay has been changed to 0.5s to improve the
    1.36 +    user experience.
    1.37 +
    1.38 +  - Option jedit_completion_immediate may now get used with
    1.39 +    jedit_completion_delay > 0, to complete symbol abbreviations
    1.40 +    aggressively while benefiting from combined syntactic and semantic
    1.41 +    completion.
    1.42 +
    1.43 +  - Support for simple completion templates (with single
    1.44 +    place-holder), e.g. "`" for text cartouche, or "@{" for
    1.45 +    antiquotation.
    1.46 +
    1.47 +  - Improved treatment of completion vs. various forms of jEdit text
    1.48 +    selection (multiple selections, rectangular selections,
    1.49 +    rectangular selection as "tall caret").
    1.50 +
    1.51 +  - More reliable treatment of GUI events vs. completion popups: avoid
    1.52 +    loosing keystrokes with slow / remote graphics displays.
    1.53 +
    1.54  * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
    1.55  Open text buffers take precedence over copies within the file-system.
    1.56  
    1.57  * Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
    1.58  auxiliary ML files.
    1.59  
    1.60 -* Improved completion based on context information about embedded
    1.61 -languages: keywords are only completed for outer syntax, symbols or
    1.62 -antiquotations for languages that support them.  E.g. no symbol
    1.63 -completion for ML source, but within ML strings, comments,
    1.64 -antiquotations.
    1.65 -
    1.66 -* Semantic completions may get extended by appending a suffix of
    1.67 -underscores to an already recognized name, e.g. "foo_" to complete
    1.68 -"foo" or "foobar" if these are known in the context.  The special
    1.69 -identifier "__" serves as a wild-card in this respect: it completes to
    1.70 -the full collection of names from the name space (truncated according
    1.71 -to the system option "completion_limit").
    1.72 -
    1.73  * Document panel: simplied interaction where every single mouse click
    1.74  (re)opens document via desktop environment or as jEdit buffer.
    1.75