--- a/NEWS Wed Sep 21 22:44:24 2016 +0200
+++ b/NEWS Thu Sep 22 00:12:17 2016 +0200
@@ -33,6 +33,10 @@
* 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.
+
* New symbol \<circle>, e.g. for temporal operator.
* Old 'header' command is no longer supported (legacy since
--- a/src/Doc/Main/Main_Doc.thy Wed Sep 21 22:44:24 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy Thu Sep 22 00:12:17 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 22:44:24 2016 +0200
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Thu Sep 22 00:12:17 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 22:44:24 2016 +0200
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Thu Sep 22 00:12:17 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 22:44:24 2016 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy Thu Sep 22 00:12:17 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 22:44:24 2016 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Thu Sep 22 00:12:17 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 22:44:24 2016 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Thu Sep 22 00:12:17 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 22:44:24 2016 +0200
+++ b/src/HOL/Set_Interval.thy Thu Sep 22 00:12:17 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/Pure/Thy/latex.ML Wed Sep 21 22:44:24 2016 +0200
+++ b/src/Pure/Thy/latex.ML Thu Sep 22 00:12:17 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,27 @@
| 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.Raw _ => error "Bad raw symbol"
| 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 +214,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;