mixfix annotations may use cartouches;
authorwenzelm
Thu Jan 03 16:42:15 2019 +0100 (10 months ago)
changeset 695806f755e3cd95d
parent 69579 edea246cedb3
child 69581 4560d1f6c493
mixfix annotations may use cartouches;
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Pure/Isar/parse.ML
     1.1 --- a/NEWS	Thu Jan 03 16:13:57 2019 +0100
     1.2 +++ b/NEWS	Thu Jan 03 16:42:15 2019 +0100
     1.3 @@ -31,6 +31,9 @@
     1.4  * Infix operators that begin or end with a "*" can now be paranthesized
     1.5  without additional spaces, eg "(*)" instead of "( * )".
     1.6  
     1.7 +* Mixfix annotations may use cartouches instead of old-style double
     1.8 +quotes, e.g. (infixl \<open>+\<close> 60).
     1.9 +
    1.10  * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
    1.11  need to provide a closed expression -- without trailing semicolon. Minor
    1.12  INCOMPATIBILITY.
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Thu Jan 03 16:13:57 2019 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Thu Jan 03 16:42:15 2019 +0100
     2.3 @@ -284,15 +284,15 @@
     2.4          @'binder' @{syntax template} prio? @{syntax nat} |
     2.5          @'structure') ')'
     2.6      ;
     2.7 -    @{syntax template}: string
     2.8 +    @{syntax template}: (string | cartouche)
     2.9      ;
    2.10      prios: '[' (@{syntax nat} + ',') ']'
    2.11      ;
    2.12      prio: '[' @{syntax nat} ']'
    2.13    \<close>}
    2.14  
    2.15 -  The string given as \<open>template\<close> may include literal text, spacing, blocks,
    2.16 -  and arguments (denoted by ``\<open>_\<close>''); the special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as
    2.17 +  The mixfix \<open>template\<close> may include literal text, spacing, blocks, and
    2.18 +  arguments (denoted by ``\<open>_\<close>''); the special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as
    2.19    ``\<open>\<index>\<close>'') represents an index argument that specifies an implicit @{keyword
    2.20    "structure"} reference (see also \secref{sec:locale}). Only locally fixed
    2.21    variables may be declared as @{keyword "structure"}.
     3.1 --- a/src/Pure/Isar/parse.ML	Thu Jan 03 16:13:57 2019 +0100
     3.2 +++ b/src/Pure/Isar/parse.ML	Thu Jan 03 16:42:15 2019 +0100
     3.3 @@ -328,7 +328,7 @@
     3.4  
     3.5  local
     3.6  
     3.7 -val mfix = input string;
     3.8 +val mfix = input (string || cartouche);
     3.9  
    3.10  val mixfix_ =
    3.11    mfix -- !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000)