# HG changeset patch
# User wenzelm
# Date 1474490586 -7200
# Node ID e149e3e320a3626483c1944cf3ba6d0a45a00538
# Parent  6040db6b929d35ba30895842ae4f0d36512f4a8b
more general mixfix delimiters;

diff -r 6040db6b929d -r e149e3e320a3 NEWS
--- 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
diff -r 6040db6b929d -r e149e3e320a3 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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.
diff -r 6040db6b929d -r e149e3e320a3 src/Pure/Syntax/syntax_ext.ML
--- 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))) ||