--- a/NEWS Wed Sep 21 20:33:44 2016 +0200
+++ b/NEWS Wed Sep 21 22:43:06 2016 +0200
@@ -30,6 +30,9 @@
to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
+* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
+this allows special forms of document output.
+
* New symbol \<circle>, e.g. for temporal operator.
* Old 'header' command is no longer supported (legacy since
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 21 20:33:44 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 21 22:43:06 2016 +0200
@@ -329,20 +329,21 @@
printing, notably spaces, blocks, and breaks. The general template format is
a sequence over any of the following entities.
- \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of characters other than
- the following special characters:
-
- \<^medskip>
- \begin{tabular}{ll}
- \<^verbatim>\<open>'\<close> & single quote \\
- \<^verbatim>\<open>_\<close> & underscore \\
- \<open>\<index>\<close> & index symbol \\
- \<^verbatim>\<open>(\<close> & open parenthesis \\
- \<^verbatim>\<open>)\<close> & close parenthesis \\
- \<^verbatim>\<open>/\<close> & slash \\
- \<open>\<open> \<close>\<close> & cartouche delimiters \\
- \end{tabular}
- \<^medskip>
+ \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence delimiter items of the
+ following form:
+ \<^enum> a control symbol followed by a cartouche
+ \<^enum> a single symbol, excluding the following special characters:
+ \<^medskip>
+ \begin{tabular}{ll}
+ \<^verbatim>\<open>'\<close> & single quote \\
+ \<^verbatim>\<open>_\<close> & underscore \\
+ \<open>\<index>\<close> & index symbol \\
+ \<^verbatim>\<open>(\<close> & open parenthesis \\
+ \<^verbatim>\<open>)\<close> & close parenthesis \\
+ \<^verbatim>\<open>/\<close> & slash \\
+ \<open>\<open> \<close>\<close> & cartouche delimiters \\
+ \end{tabular}
+ \<^medskip>
\<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these meta-characters, producing a
literal version of the following character, unless that is a blank.
--- a/src/Pure/Syntax/syntax_ext.ML Wed Sep 21 20:33:44 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Wed Sep 21 22:43:06 2016 +0200
@@ -251,9 +251,10 @@
val is_meta = member (op =) ["(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
-val scan_delim_char =
- $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
- scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
+val scan_delim =
+ scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " ||
+ $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) >> single ||
+ scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof) >> single;
val scan_sym =
$$ "_" >> K (Argument ("", 0)) ||
@@ -265,7 +266,7 @@
$$ "/" -- $$ "/" >> K (Brk ~1) ||
$$ "/" |-- scan_many Symbol.is_space >> (Brk o length) ||
scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) ||
- Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
+ Scan.repeat1 scan_delim >> (Delim o Symbol_Pos.content o flat);
val scan_symb =
Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) ||