NEWS
changeset 68073 fad29d2a17a5
parent 68072 493b818e8e10
parent 68067 b91c4acc1aaf
child 68080 17f79ae49401
     1.1 --- a/NEWS	Wed May 02 13:49:38 2018 +0200
     1.2 +++ b/NEWS	Thu May 03 15:07:14 2018 +0200
     1.3 @@ -110,7 +110,8 @@
     1.4  notably bibtex database files and ML files.
     1.5  
     1.6  * Action "isabelle.draft" is similar to "isabelle.preview", but shows a
     1.7 -plain-text document draft.
     1.8 +plain-text document draft. Both are available via the menu "Plugins /
     1.9 +Isabelle".
    1.10  
    1.11  * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
    1.12  is only used if there is no conflict with existing Unicode sequences in
    1.13 @@ -196,8 +197,38 @@
    1.14  
    1.15  *** HOL ***
    1.16  
    1.17 -* Abstract bit operations as part of Main: push_bit, push_take,
    1.18 -push_drop.
    1.19 +* Clarified relationship of characters, strings and code generation:
    1.20 +
    1.21 +  * Type "char" is now a proper datatype of 8-bit values.
    1.22 +
    1.23 +  * Conversions "nat_of_char" and "char_of_nat" are gone; use more
    1.24 +    general conversions "of_char" and "char_of" with suitable
    1.25 +    type constraints instead.
    1.26 +
    1.27 +  * The zero character is just written "CHR 0x00", not
    1.28 +    "0" any longer.
    1.29 +
    1.30 +  * Type "String.literal" (for code generation) is now isomorphic
    1.31 +    to lists of 7-bit (ASCII) values; concrete values can be written
    1.32 +    as "STR ''...''" for sequences of printable characters and
    1.33 +    "STR 0x..." for one single ASCII code point given
    1.34 +    as hexadecimal numeral.
    1.35 +
    1.36 +  * Type "String.literal" supports concatenation "... + ..."
    1.37 +    for all standard target languages.
    1.38 +
    1.39 +  * Theory Library/Code_Char is gone; study the explanations concerning
    1.40 +    "String.literal" in the tutorial on code generation to get an idea
    1.41 +    how target-language string literals can be converted to HOL string
    1.42 +    values and vice versa.
    1.43 +
    1.44 +  * Imperative-HOL: operation "raise" directly takes a value of type
    1.45 +    "String.literal" as argument, not type "string".
    1.46 +
    1.47 +INCOMPATIBILITY.
    1.48 +
    1.49 +* Abstract bit operations as part of Main: push_bit, take_bit,
    1.50 +drop_bit.
    1.51  
    1.52  * New, more general, axiomatization of complete_distrib_lattice. 
    1.53  The former axioms:
    1.54 @@ -317,6 +348,20 @@
    1.55  been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
    1.56  instead of former 32/64 variants. INCOMPATIBILITY.
    1.57  
    1.58 +* Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be
    1.59 +phased out due to unclear preference of 32bit vs. 64bit architecture.
    1.60 +Explicit GNU bash expressions are now preferred, for example (with
    1.61 +quotes):
    1.62 +
    1.63 +  #Posix executables (Unix or Cygwin), with preference for 64bit
    1.64 +  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    1.65 +
    1.66 +  #native Windows or Unix executables, with preference for 64bit
    1.67 +  "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
    1.68 +
    1.69 +  #native Windows (32bit) or Unix executables (preference for 64bit)
    1.70 +  "${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}"
    1.71 +
    1.72  * Command-line tool "isabelle build" supports new options:
    1.73    - option -B NAME: include session NAME and all descendants
    1.74    - option -S: only observe changes of sources, not heap images