--- a/NEWS Thu Jan 03 16:13:57 2019 +0100
+++ b/NEWS Thu Jan 03 16:42:15 2019 +0100
@@ -31,6 +31,9 @@
* Infix operators that begin or end with a "*" can now be paranthesized
without additional spaces, eg "(*)" instead of "( * )".
+* Mixfix annotations may use cartouches instead of old-style double
+quotes, e.g. (infixl \<open>+\<close> 60).
+
* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
need to provide a closed expression -- without trailing semicolon. Minor
INCOMPATIBILITY.
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Jan 03 16:13:57 2019 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Jan 03 16:42:15 2019 +0100
@@ -284,15 +284,15 @@
@'binder' @{syntax template} prio? @{syntax nat} |
@'structure') ')'
;
- @{syntax template}: string
+ @{syntax template}: (string | cartouche)
;
prios: '[' (@{syntax nat} + ',') ']'
;
prio: '[' @{syntax nat} ']'
\<close>}
- The string given as \<open>template\<close> may include literal text, spacing, blocks,
- and arguments (denoted by ``\<open>_\<close>''); the special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as
+ The mixfix \<open>template\<close> may include literal text, spacing, blocks, and
+ arguments (denoted by ``\<open>_\<close>''); the special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as
``\<open>\<index>\<close>'') represents an index argument that specifies an implicit @{keyword
"structure"} reference (see also \secref{sec:locale}). Only locally fixed
variables may be declared as @{keyword "structure"}.
--- a/src/Pure/Isar/parse.ML Thu Jan 03 16:13:57 2019 +0100
+++ b/src/Pure/Isar/parse.ML Thu Jan 03 16:42:15 2019 +0100
@@ -328,7 +328,7 @@
local
-val mfix = input string;
+val mfix = input (string || cartouche);
val mixfix_ =
mfix -- !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000)