--- a/NEWS Wed Sep 21 17:56:25 2016 +0200
+++ b/NEWS Thu Sep 22 15:41:47 2016 +0200
@@ -30,6 +30,15 @@
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.
+
+* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
+symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
+derivatives.
+
+* \<^raw:...> symbols are no longer supported.
+
* New symbol \<circle>, e.g. for temporal operator.
* Old 'header' command is no longer supported (legacy since
--- a/src/Doc/Implementation/ML.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Doc/Implementation/ML.thy Thu Sep 22 15:41:47 2016 +0200
@@ -1217,13 +1217,6 @@
\<^enum> a control symbol ``\<^verbatim>\<open>\<^ident>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
- \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of
- printable characters excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
- ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
-
- \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
- of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
-
The \<open>ident\<close> syntax for symbol names is \<open>letter (letter | digit)\<^sup>*\<close>, where
\<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular
symbols and control symbols, but a fixed collection of standard symbols is
@@ -1275,7 +1268,7 @@
\<^descr> Type @{ML_type "Symbol.sym"} is a concrete datatype that represents the
different kinds of symbols explicitly, with constructors @{ML
"Symbol.Char"}, @{ML "Symbol.UTF8"}, @{ML "Symbol.Sym"}, @{ML
- "Symbol.Control"}, @{ML "Symbol.Raw"}, @{ML "Symbol.Malformed"}.
+ "Symbol.Control"}, @{ML "Symbol.Malformed"}.
\<^descr> @{ML "Symbol.decode"} converts the string representation of a symbol into
the datatype version.
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Sep 22 15:41:47 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/Doc/Main/Main_Doc.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy Thu Sep 22 15:41:47 2016 +0200
@@ -229,7 +229,7 @@
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
@{term "Pair a b"} & @{term[source]"Pair a b"}\\
@{term "case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
-@{term "A \<times> B"} & \<open>Sigma A (\<lambda>\<^raw:\_>. B)\<close>
+@{term "A \<times> B"} & \<open>Sigma A (\<lambda>\<^latex>\<open>\_\<close>. B)\<close>
\end{tabular}
Pairs may be nested. Nesting to the right is printed as a tuple,
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Thu Sep 22 15:41:47 2016 +0200
@@ -69,7 +69,7 @@
Because both subgoals are easy, Isabelle can do it.
The base case @{prop"add 0 0 = 0"} holds by definition of @{const add},
and the induction step is almost as simple:
-@{text"add\<^raw:~>(Suc m) 0 = Suc(add m 0) = Suc m"}
+@{text"add\<^latex>\<open>~\<close>(Suc m) 0 = Suc(add m 0) = Suc m"}
using first the definition of @{const add} and then the induction hypothesis.
In summary, both subproofs rely on simplification with function definitions and
the induction hypothesis.
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Thu Sep 22 15:41:47 2016 +0200
@@ -9,38 +9,38 @@
begin
(* DUMMY *)
-consts DUMMY :: 'a ("\<^raw:\_>")
+consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
(* THEOREMS *)
notation (Rule output)
- Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+ Pure.imp ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
syntax (Rule output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+ ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
- ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+ ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
- "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
notation (Axiom output)
- "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+ "Trueprop" ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
notation (IfThen output)
- Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ Pure.imp ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
syntax (IfThen output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
- "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
- "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
notation (IfThenNoBox output)
- Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ Pure.imp ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
syntax (IfThenNoBox output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
- "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
setup{*
--- a/src/Doc/Prog_Prove/Logic.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy Thu Sep 22 15:41:47 2016 +0200
@@ -340,7 +340,7 @@
The expression @{text"conjI[of \"a=b\" \"False\"]"}
instantiates the unknowns in @{thm[source] conjI} from left to right with the
two formulas @{text"a=b"} and @{text False}, yielding the rule
-@{thm[display,mode=Rule]conjI[of "a=b" False]}
+@{thm[display,mode=Rule,margin=100]conjI[of "a=b" False]}
In general, @{text"th[of string\<^sub>1 \<dots> string\<^sub>n]"} instantiates
the unknowns in the theorem @{text th} from left to right with the terms
--- a/src/HOL/Library/LaTeXsugar.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Thu Sep 22 15:41:47 2016 +0200
@@ -10,15 +10,15 @@
(* LOGIC *)
notation (latex output)
- If ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
+ If ("(\<^latex>\<open>\\textsf{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>else\<^latex>\<open>}\<close> (_))" 10)
syntax (latex output)
"_Let" :: "[letbinds, 'a] => 'a"
- ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
+ ("(\<^latex>\<open>\\textsf{\<close>let\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>in\<^latex>\<open>}\<close> (_))" 10)
"_case_syntax":: "['a, cases_syn] => 'b"
- ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
+ ("(\<^latex>\<open>\\textsf{\<close>case\<^latex>\<open>}\<close> _ \<^latex>\<open>\\textsf{\<close>of\<^latex>\<open>}\<close>/ _)" 10)
(* SETS *)
@@ -59,41 +59,41 @@
(* nth *)
notation (latex output)
- nth ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
+ nth ("_\<^latex>\<open>\\ensuremath{_{[\\mathit{\<close>_\<^latex>\<open>}]}}\<close>" [1000,0] 1000)
(* DUMMY *)
-consts DUMMY :: 'a ("\<^raw:\_>")
+consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
(* THEOREMS *)
notation (Rule output)
- Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+ Pure.imp ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
syntax (Rule output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+ ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
- ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+ ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
- "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
notation (Axiom output)
- "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+ "Trueprop" ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
notation (IfThen output)
- Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ Pure.imp ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
syntax (IfThen output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
- "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
- "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+ ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
notation (IfThenNoBox output)
- Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ Pure.imp ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
syntax (IfThenNoBox output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
- "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
setup\<open>
--- a/src/HOL/Library/OptionalSugar.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Thu Sep 22 15:41:47 2016 +0200
@@ -27,7 +27,7 @@
(* append *)
syntax (latex output)
- "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
+ "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^latex>\<open>\\isacharat\<close>" 65)
translations
"_appendL xs ys" <= "xs @ ys"
"_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
@@ -36,8 +36,8 @@
(* deprecated, use thm with style instead, will be removed *)
(* aligning equations *)
notation (tab output)
- "HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
- "Pure.eq" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
+ "HOL.eq" ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>=\<^latex>\<open>}\\putisatab\\isa{\<close> (_)" [50,49] 50) and
+ "Pure.eq" ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>\<equiv>\<^latex>\<open>}\\putisatab\\isa{\<close> (_)")
(* Let *)
translations
--- a/src/HOL/Set_Interval.thy Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Set_Interval.thy Thu Sep 22 15:41:47 2016 +0200
@@ -1609,13 +1609,13 @@
syntax (latex_sum output)
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
+ ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
+ ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^latex>\<open>$\\sum_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^latex>\<open>$\\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
syntax
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
@@ -2013,13 +2013,13 @@
syntax (latex_prod output)
"_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
+ ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
"_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
+ ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
"_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^latex>\<open>$\\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
"_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^latex>\<open>$\\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
syntax
"_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Sep 22 15:41:47 2016 +0200
@@ -125,8 +125,8 @@
val get = maps (Proof_Context.get_fact ctxt o fst)
val keywords = Thy_Header.get_keywords' ctxt
in
- Source.of_string name
- |> Symbol.source
+ Symbol.explode name
+ |> Source.of_list
|> Token.source keywords Position.start
|> Token.source_proper
|> Source.source Token.stopper (Parse.thms1 >> get)
--- a/src/Pure/General/symbol.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/General/symbol.ML Thu Sep 22 15:41:47 2016 +0200
@@ -1,5 +1,5 @@
(* Title: Pure/General/symbol.ML
- Author: Markus Wenzel, TU Muenchen
+ Author: Makarius
Generalized characters with infinitely many named symbols.
*)
@@ -7,6 +7,7 @@
signature SYMBOL =
sig
type symbol = string
+ val explode: string -> symbol list
val spaces: int -> string
val STX: symbol
val DEL: symbol
@@ -41,12 +42,8 @@
val to_ascii_upper: symbol -> symbol
val is_ascii_identifier: string -> bool
val scan_ascii_id: string list -> string * string list
- val is_raw: symbol -> bool
- val decode_raw: symbol -> string
- val encode_raw: string -> string
datatype sym =
- Char of string | UTF8 of string | Sym of string | Control of string | Raw of string |
- Malformed of string | EOF
+ Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF
val decode: symbol -> sym
datatype kind = Letter | Digit | Quasi | Blank | Other
val kind: symbol -> kind
@@ -58,8 +55,6 @@
val is_quasi_letter: symbol -> bool
val is_letdig: symbol -> bool
val beginning: int -> symbol list -> string
- val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
- val explode: string -> symbol list
val esc: symbol -> string
val escape: string -> string
val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
@@ -81,11 +76,10 @@
(*Symbols, which are considered the smallest entities of any Isabelle
string, may be of the following form:
- (1) ASCII symbols: a
+ (1) ASCII: a
+ (2) UTF-8: รค
(2) regular symbols: \<ident>
(3) control symbols: \<^ident>
- (4) raw control symbols: \<^raw:...>, where "..." may be any printable
- character (excluding ".", ">"), or \<^raw000>
Output is subject to the print_mode variable (default: verbatim),
actual interpretation in display is up to front-end tools.
@@ -191,31 +185,6 @@
val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode);
-(* encode_raw *)
-
-fun raw_chr c =
- is_char c andalso
- (ord space <= ord c andalso ord c <= ord "~" andalso c <> "." andalso c <> ">"
- orelse ord c >= 128);
-
-fun encode_raw "" = ""
- | encode_raw str =
- let
- val raw0 = enclose "\092<^raw:" ">";
- val raw1 = raw0 o implode;
- val raw2 = enclose "\092<^raw" ">" o string_of_int o ord;
-
- fun encode cs = enc (take_prefix raw_chr cs)
- and enc ([], []) = []
- | enc (cs, []) = [raw1 cs]
- | enc ([], d :: ds) = raw2 d :: encode ds
- | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
- in
- if exists_string (not o raw_chr) str then implode (encode (raw_explode str))
- else raw0 str
- end;
-
-
(* diagnostics *)
fun beginning n cs =
@@ -230,28 +199,15 @@
end;
-(* decode_raw *)
-
-fun is_raw s =
- String.isPrefix "\092<^raw" s andalso String.isSuffix ">" s;
-
-fun decode_raw s =
- if not (is_raw s) then error (malformed_msg s)
- else if String.isPrefix "\092<^raw:" s then String.substring (s, 7, size s - 8)
- else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
-
-
(* symbol variants *)
datatype sym =
- Char of string | UTF8 of string | Sym of string | Control of string | Raw of string |
- Malformed of string | EOF;
+ Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF;
fun decode s =
if s = "" then EOF
else if is_char s then Char s
else if is_utf8 s then UTF8 s
- else if is_raw s then Raw (decode_raw s)
else if is_malformed s then Malformed s
else if is_control s then Control (String.substring (s, 3, size s - 4))
else Sym (String.substring (s, 2, size s - 3));
@@ -429,65 +385,6 @@
fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
-
-(** symbol input **)
-
-(* source *)
-
-local
-
-fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\";
-
-fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;
-
-fun implode_pseudo_utf8 (cs as ["\192", c]) =
- if ord c < 160 then chr (ord c - 128) else implode cs
- | implode_pseudo_utf8 cs = implode cs;
-
-val scan_encoded_newline =
- $$ "\^M" -- $$ "\n" >> K "\n" ||
- $$ "\^M" >> K "\n";
-
-val scan_raw =
- Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
- Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
-
-val scan_total =
- Scan.one is_plain ||
- Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
- scan_encoded_newline ||
- ($$ "\\" ^^ $$ "<" ^^
- (($$ "^" ^^ Scan.optional (scan_raw || scan_ascii_id) "" || Scan.optional scan_ascii_id "") ^^
- Scan.optional ($$ ">") "")) ||
- Scan.one not_eof;
-
-in
-
-fun source src = Source.source stopper (Scan.bulk scan_total) src;
-
-end;
-
-
-(* explode *)
-
-local
-
-fun no_explode [] = true
- | no_explode ("\\" :: "<" :: _) = false
- | no_explode ("\^M" :: _) = false
- | no_explode (c :: cs) = is_ascii c andalso no_explode cs;
-
-in
-
-fun sym_explode str =
- let val chs = raw_explode str in
- if no_explode chs then chs
- else Source.exhaust (source (Source.of_list chs))
- end;
-
-end;
-
-
(* escape *)
val esc = fn s =>
@@ -495,7 +392,7 @@
else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
else "\\" ^ s;
-val escape = implode o map esc o sym_explode;
+val escape = implode o map esc o Symbol.explode;
@@ -523,12 +420,12 @@
val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I);
-val explode_words = split_words o sym_explode;
+val explode_words = split_words o Symbol.explode;
(* blanks *)
-val trim_blanks = sym_explode #> trim is_blank #> implode;
+val trim_blanks = Symbol.explode #> trim is_blank #> implode;
(* bump string -- treat as base 26 or base 1 numbers *)
@@ -539,7 +436,7 @@
| symbolic_end [] = false;
fun bump_init str =
- if symbolic_end (rev (sym_explode str)) then str ^ "'"
+ if symbolic_end (rev (Symbol.explode str)) then str ^ "'"
else str ^ "a";
fun bump_string str =
@@ -551,7 +448,7 @@
then chr (ord s + 1) :: ss
else "a" :: s :: ss;
- val (ss, qs) = apfst rev (take_suffix is_quasi (sym_explode str));
+ val (ss, qs) = apfst rev (take_suffix is_quasi (Symbol.explode str));
val ss' = if symbolic_end ss then "'" :: ss else bump ss;
in implode (rev ss' @ qs) end;
@@ -574,11 +471,11 @@
val xsymbolsN = "xsymbols";
-fun output s = (s, sym_length (sym_explode s));
+fun output s = (s, sym_length (Symbol.explode s));
(*final declarations of this structure!*)
-val explode = sym_explode;
+val explode = Symbol.explode;
val length = sym_length;
end;
--- a/src/Pure/General/symbol.scala Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/General/symbol.scala Thu Sep 22 15:41:47 2016 +0200
@@ -64,9 +64,7 @@
/* symbol matching */
private val symbol_total = new Regex("""(?xs)
- [\ud800-\udbff][\udc00-\udfff] | \r\n |
- \\ < (?: \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* | \^? ([A-Za-z][A-Za-z0-9_']*)? ) >? |
- .""")
+ [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")
private def is_plain(c: Char): Boolean =
!(c == '\r' || c == '\\' || Character.isHighSurrogate(c))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/symbol_explode.ML Thu Sep 22 15:41:47 2016 +0200
@@ -0,0 +1,53 @@
+(* Title: Pure/General/symbol_explode.ML
+ Author: Makarius
+
+String explode operation for Isabelle symbols (see also symbol.ML).
+*)
+
+structure Symbol: sig val explode: string -> string list end =
+struct
+
+fun is_ascii_letter c = #"A" <= c andalso c <= #"Z" orelse #"a" <= c andalso c <= #"z";
+fun is_ascii_letdig c =
+ is_ascii_letter c orelse #"0" <= c andalso c <= #"9" orelse c = #"_" orelse c = #"'";
+
+fun is_utf8 c = c >= #"\128";
+fun is_utf8_trailer c = #"\128" <= c andalso c < #"\192";
+fun is_utf8_control c = #"\128" <= c andalso c < #"\160";
+
+fun explode string =
+ let
+ fun char i = String.sub (string, i);
+ fun string_range i j = String.substring (string, i, j - i);
+
+ val n = size string;
+ fun test pred i = i < n andalso pred (char i);
+ fun many pred i = if test pred i then many pred (i + 1) else i;
+ fun maybe pred i = if test pred i then i + 1 else i;
+ fun maybe_char c = maybe (fn c' => c = c');
+ fun maybe_ascii_id i = if test is_ascii_letter i then many is_ascii_letdig (i + 1) else i;
+
+ fun scan i =
+ if i < n then
+ let val ch = char i in
+ (*encoded newline*)
+ if ch = #"\^M" then "\n" :: scan (maybe_char #"\n" (i + 1))
+ (*pseudo utf8: encoded ascii control*)
+ else if ch = #"\192" andalso
+ test is_utf8_control (i + 1) andalso not (test is_utf8 (i + 2))
+ then chr (Char.ord (char (i + 1)) - 128) :: scan (i + 2)
+ (*utf8*)
+ else if is_utf8 ch then
+ let val j = many is_utf8_trailer (i + 1)
+ in string_range i j :: scan j end
+ (*named symbol*)
+ else if ch = #"\\" andalso test (fn c => c = #"<") (i + 1) then
+ let val j = (i + 2) |> maybe_char #"^" |> maybe_ascii_id |> maybe_char #">"
+ in string_range i j :: scan j end
+ (*single character*)
+ else String.str ch :: scan (i + 1)
+ end
+ else [];
+ in scan 0 end;
+
+end;
--- a/src/Pure/Isar/outer_syntax.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Sep 22 15:41:47 2016 +0200
@@ -220,17 +220,17 @@
in
-fun parse thy pos str =
- Source.of_string str
- |> Symbol.source
- |> Token.source (Thy_Header.get_keywords thy) pos
- |> commands_source thy
- |> Source.exhaust;
+fun parse thy pos =
+ Symbol.explode
+ #> Source.of_list
+ #> Token.source (Thy_Header.get_keywords thy) pos
+ #> commands_source thy
+ #> Source.exhaust;
-fun parse_tokens thy toks =
- Source.of_list toks
- |> commands_source thy
- |> Source.exhaust;
+fun parse_tokens thy =
+ Source.of_list
+ #> commands_source thy
+ #> Source.exhaust;
end;
--- a/src/Pure/Isar/token.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/Isar/token.ML Thu Sep 22 15:41:47 2016 +0200
@@ -650,8 +650,8 @@
(* explode *)
fun explode keywords pos =
- Source.of_string #>
- Symbol.source #>
+ Symbol.explode #>
+ Source.of_list #>
source keywords pos #>
Source.exhaust;
--- a/src/Pure/ML/ml_lex.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/ML/ml_lex.ML Thu Sep 22 15:41:47 2016 +0200
@@ -351,7 +351,7 @@
Symbol_Pos.source (Position.line 1) src
|> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_ml)) recover);
-val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
+val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust;
val read_pos = gen_read false;
--- a/src/Pure/ROOT.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/ROOT.ML Thu Sep 22 15:41:47 2016 +0200
@@ -10,6 +10,7 @@
ML_file "System/distribution.ML";
ML_file "General/basics.ML";
+ML_file "General/symbol_explode.ML";
ML_file "Concurrent/multithreading.ML";
ML_file "Concurrent/unsynchronized.ML";
--- a/src/Pure/Syntax/syntax_ext.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Thu Sep 22 15:41:47 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))) ||
--- a/src/Pure/Thy/html.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/Thy/html.ML Thu Sep 22 15:41:47 2016 +0200
@@ -48,11 +48,9 @@
val no_symbols = make_symbols [];
fun output_sym (Symbols tab) s =
- if Symbol.is_raw s then Symbol.decode_raw s
- else
- (case Symtab.lookup tab s of
- SOME x => x
- | NONE => XML.text s);
+ (case Symtab.lookup tab s of
+ SOME x => x
+ | NONE => XML.text s);
end;
--- a/src/Pure/Thy/latex.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/Thy/latex.ML Thu Sep 22 15:41:47 2016 +0200
@@ -7,6 +7,9 @@
signature LATEX =
sig
val output_ascii: string -> string
+ val latex_control: Symbol.symbol
+ val is_latex_control: Symbol.symbol -> bool
+ val embed_raw: string -> string
val output_known_symbols: (string -> bool) * (string -> bool) ->
Symbol.symbol list -> string
val output_symbols: Symbol.symbol list -> string
@@ -41,6 +44,11 @@
(* output symbols *)
+val latex_control = "\<^latex>";
+fun is_latex_control s = s = latex_control;
+
+val embed_raw = prefix latex_control o cartouche;
+
local
val char_table =
@@ -95,13 +103,26 @@
| Symbol.UTF8 s => s
| Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
| Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
- | Symbol.Raw s => s
| Symbol.Malformed s => error (Symbol.malformed_msg s)
| Symbol.EOF => error "Bad EOF symbol");
+fun scan_latex known =
+ Scan.one (is_latex_control o Symbol_Pos.symbol) |--
+ Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
+ Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
+
+fun read_latex known syms =
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat (scan_latex known))
+ (map (rpair Position.none) syms) of
+ SOME ss => implode ss
+ | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)));
+
in
-val output_known_symbols = implode oo (map o output_known_sym);
+fun output_known_symbols known syms =
+ if exists is_latex_control syms then read_latex known syms
+ else implode (map (output_known_sym known) syms);
+
val output_symbols = output_known_symbols (K true, K true);
val output_syms = output_symbols o Symbol.explode;
@@ -192,7 +213,7 @@
fun latex_indent "" _ = ""
| latex_indent s _ = enclose "\\isaindent{" "}" s;
-val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
+val _ = Output.add_mode latexN latex_output embed_raw;
val _ = Markup.add_mode latexN latex_markup;
val _ = Pretty.add_mode latexN latex_indent;
--- a/src/Pure/Thy/thy_header.ML Wed Sep 21 17:56:25 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Thu Sep 22 15:41:47 2016 +0200
@@ -168,11 +168,10 @@
val header =
(Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
-fun token_source pos str =
- str
- |> Source.of_string_limited 8000
- |> Symbol.source
- |> Token.source_strict bootstrap_keywords pos;
+fun token_source pos =
+ Symbol.explode
+ #> Source.of_list
+ #> Token.source_strict bootstrap_keywords pos;
fun read_source pos source =
let val res =