raw control symbols are superseded by Latex.embed_raw;
authorwenzelm
Thu Sep 22 00:12:17 2016 +0200 (2016-09-22)
changeset 63935aa1fe1103ab8
parent 63934 397b25cee74c
child 63936 b87784e19a77
raw control symbols are superseded by Latex.embed_raw;
NEWS
src/Doc/Main/Main_Doc.thy
src/Doc/Prog_Prove/Bool_nat_list.thy
src/Doc/Prog_Prove/LaTeXsugar.thy
src/Doc/Prog_Prove/Logic.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Library/OptionalSugar.thy
src/HOL/Set_Interval.thy
src/Pure/Thy/latex.ML
     1.1 --- a/NEWS	Wed Sep 21 22:44:24 2016 +0200
     1.2 +++ b/NEWS	Thu Sep 22 00:12:17 2016 +0200
     1.3 @@ -33,6 +33,10 @@
     1.4  * Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
     1.5  this allows special forms of document output.
     1.6  
     1.7 +* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
     1.8 +symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
     1.9 +derivatives.
    1.10 +
    1.11  * New symbol \<circle>, e.g. for temporal operator.
    1.12  
    1.13  * Old 'header' command is no longer supported (legacy since
     2.1 --- a/src/Doc/Main/Main_Doc.thy	Wed Sep 21 22:44:24 2016 +0200
     2.2 +++ b/src/Doc/Main/Main_Doc.thy	Thu Sep 22 00:12:17 2016 +0200
     2.3 @@ -229,7 +229,7 @@
     2.4  \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
     2.5  @{term "Pair a b"} & @{term[source]"Pair a b"}\\
     2.6  @{term "case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
     2.7 -@{term "A \<times> B"} &  \<open>Sigma A (\<lambda>\<^raw:\_>. B)\<close>
     2.8 +@{term "A \<times> B"} &  \<open>Sigma A (\<lambda>\<^latex>\<open>\_\<close>. B)\<close>
     2.9  \end{tabular}
    2.10  
    2.11  Pairs may be nested. Nesting to the right is printed as a tuple,
     3.1 --- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Wed Sep 21 22:44:24 2016 +0200
     3.2 +++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Sep 22 00:12:17 2016 +0200
     3.3 @@ -69,7 +69,7 @@
     3.4  Because both subgoals are easy, Isabelle can do it.
     3.5  The base case @{prop"add 0 0 = 0"} holds by definition of @{const add},
     3.6  and the induction step is almost as simple:
     3.7 -@{text"add\<^raw:~>(Suc m) 0 = Suc(add m 0) = Suc m"}
     3.8 +@{text"add\<^latex>\<open>~\<close>(Suc m) 0 = Suc(add m 0) = Suc m"}
     3.9  using first the definition of @{const add} and then the induction hypothesis.
    3.10  In summary, both subproofs rely on simplification with function definitions and
    3.11  the induction hypothesis.
     4.1 --- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Wed Sep 21 22:44:24 2016 +0200
     4.2 +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Thu Sep 22 00:12:17 2016 +0200
     4.3 @@ -9,38 +9,38 @@
     4.4  begin
     4.5  
     4.6  (* DUMMY *)
     4.7 -consts DUMMY :: 'a ("\<^raw:\_>")
     4.8 +consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
     4.9  
    4.10  (* THEOREMS *)
    4.11  notation (Rule output)
    4.12 -  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    4.13 +  Pure.imp  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    4.14  
    4.15  syntax (Rule output)
    4.16    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    4.17 -  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    4.18 +  ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    4.19  
    4.20    "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    4.21 -  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    4.22 +  ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
    4.23  
    4.24 -  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    4.25 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
    4.26  
    4.27  notation (Axiom output)
    4.28 -  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    4.29 +  "Trueprop"  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    4.30  
    4.31  notation (IfThen output)
    4.32 -  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    4.33 +  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    4.34  syntax (IfThen output)
    4.35    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    4.36 -  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    4.37 -  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    4.38 -  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    4.39 +  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    4.40 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
    4.41 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
    4.42  
    4.43  notation (IfThenNoBox output)
    4.44 -  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    4.45 +  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    4.46  syntax (IfThenNoBox output)
    4.47    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    4.48 -  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    4.49 -  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    4.50 +  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    4.51 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
    4.52    "_asm" :: "prop \<Rightarrow> asms" ("_")
    4.53  
    4.54  setup{*
     5.1 --- a/src/Doc/Prog_Prove/Logic.thy	Wed Sep 21 22:44:24 2016 +0200
     5.2 +++ b/src/Doc/Prog_Prove/Logic.thy	Thu Sep 22 00:12:17 2016 +0200
     5.3 @@ -340,7 +340,7 @@
     5.4  The expression @{text"conjI[of \"a=b\" \"False\"]"}
     5.5  instantiates the unknowns in @{thm[source] conjI} from left to right with the
     5.6  two formulas @{text"a=b"} and @{text False}, yielding the rule
     5.7 -@{thm[display,mode=Rule]conjI[of "a=b" False]}
     5.8 +@{thm[display,mode=Rule,margin=100]conjI[of "a=b" False]}
     5.9  
    5.10  In general, @{text"th[of string\<^sub>1 \<dots> string\<^sub>n]"} instantiates
    5.11  the unknowns in the theorem @{text th} from left to right with the terms
     6.1 --- a/src/HOL/Library/LaTeXsugar.thy	Wed Sep 21 22:44:24 2016 +0200
     6.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Thu Sep 22 00:12:17 2016 +0200
     6.3 @@ -10,15 +10,15 @@
     6.4  
     6.5  (* LOGIC *)
     6.6  notation (latex output)
     6.7 -  If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
     6.8 +  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)
     6.9  
    6.10  syntax (latex output)
    6.11  
    6.12    "_Let"        :: "[letbinds, 'a] => 'a"
    6.13 -  ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
    6.14 +  ("(\<^latex>\<open>\\textsf{\<close>let\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>in\<^latex>\<open>}\<close> (_))" 10)
    6.15  
    6.16    "_case_syntax":: "['a, cases_syn] => 'b"
    6.17 -  ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
    6.18 +  ("(\<^latex>\<open>\\textsf{\<close>case\<^latex>\<open>}\<close> _ \<^latex>\<open>\\textsf{\<close>of\<^latex>\<open>}\<close>/ _)" 10)
    6.19  
    6.20  
    6.21  (* SETS *)
    6.22 @@ -59,41 +59,41 @@
    6.23  
    6.24  (* nth *)
    6.25  notation (latex output)
    6.26 -  nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
    6.27 +  nth  ("_\<^latex>\<open>\\ensuremath{_{[\\mathit{\<close>_\<^latex>\<open>}]}}\<close>" [1000,0] 1000)
    6.28  
    6.29  (* DUMMY *)
    6.30 -consts DUMMY :: 'a ("\<^raw:\_>")
    6.31 +consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
    6.32  
    6.33  (* THEOREMS *)
    6.34  notation (Rule output)
    6.35 -  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    6.36 +  Pure.imp  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    6.37  
    6.38  syntax (Rule output)
    6.39    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    6.40 -  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    6.41 +  ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    6.42  
    6.43    "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
    6.44 -  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
    6.45 +  ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
    6.46  
    6.47 -  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    6.48 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
    6.49  
    6.50  notation (Axiom output)
    6.51 -  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    6.52 +  "Trueprop"  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
    6.53  
    6.54  notation (IfThen output)
    6.55 -  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    6.56 +  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    6.57  syntax (IfThen output)
    6.58    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    6.59 -  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    6.60 -  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    6.61 -  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    6.62 +  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    6.63 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
    6.64 +  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
    6.65  
    6.66  notation (IfThenNoBox output)
    6.67 -  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    6.68 +  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    6.69  syntax (IfThenNoBox output)
    6.70    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    6.71 -  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    6.72 -  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    6.73 +  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
    6.74 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
    6.75    "_asm" :: "prop \<Rightarrow> asms" ("_")
    6.76  
    6.77  setup\<open>
     7.1 --- a/src/HOL/Library/OptionalSugar.thy	Wed Sep 21 22:44:24 2016 +0200
     7.2 +++ b/src/HOL/Library/OptionalSugar.thy	Thu Sep 22 00:12:17 2016 +0200
     7.3 @@ -27,7 +27,7 @@
     7.4  
     7.5  (* append *)
     7.6  syntax (latex output)
     7.7 -  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
     7.8 +  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^latex>\<open>\\isacharat\<close>" 65)
     7.9  translations
    7.10    "_appendL xs ys" <= "xs @ ys" 
    7.11    "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
    7.12 @@ -36,8 +36,8 @@
    7.13  (* deprecated, use thm with style instead, will be removed *)
    7.14  (* aligning equations *)
    7.15  notation (tab output)
    7.16 -  "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    7.17 -  "Pure.eq"  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    7.18 +  "HOL.eq"  ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>=\<^latex>\<open>}\\putisatab\\isa{\<close> (_)" [50,49] 50) and
    7.19 +  "Pure.eq"  ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>\<equiv>\<^latex>\<open>}\\putisatab\\isa{\<close> (_)")
    7.20  
    7.21  (* Let *)
    7.22  translations 
     8.1 --- a/src/HOL/Set_Interval.thy	Wed Sep 21 22:44:24 2016 +0200
     8.2 +++ b/src/HOL/Set_Interval.thy	Thu Sep 22 00:12:17 2016 +0200
     8.3 @@ -1609,13 +1609,13 @@
     8.4  
     8.5  syntax (latex_sum output)
     8.6    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
     8.7 - ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
     8.8 + ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
     8.9    "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    8.10 - ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
    8.11 + ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
    8.12    "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    8.13 - ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
    8.14 + ("(3\<^latex>\<open>$\\sum_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
    8.15    "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    8.16 - ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
    8.17 + ("(3\<^latex>\<open>$\\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
    8.18  
    8.19  syntax
    8.20    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
    8.21 @@ -2013,13 +2013,13 @@
    8.22  
    8.23  syntax (latex_prod output)
    8.24    "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    8.25 - ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
    8.26 + ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
    8.27    "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    8.28 - ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
    8.29 + ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
    8.30    "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    8.31 - ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
    8.32 + ("(3\<^latex>\<open>$\\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
    8.33    "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
    8.34 - ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
    8.35 + ("(3\<^latex>\<open>$\\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
    8.36  
    8.37  syntax
    8.38    "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
     9.1 --- a/src/Pure/Thy/latex.ML	Wed Sep 21 22:44:24 2016 +0200
     9.2 +++ b/src/Pure/Thy/latex.ML	Thu Sep 22 00:12:17 2016 +0200
     9.3 @@ -7,6 +7,9 @@
     9.4  signature LATEX =
     9.5  sig
     9.6    val output_ascii: string -> string
     9.7 +  val latex_control: Symbol.symbol
     9.8 +  val is_latex_control: Symbol.symbol -> bool
     9.9 +  val embed_raw: string -> string
    9.10    val output_known_symbols: (string -> bool) * (string -> bool) ->
    9.11      Symbol.symbol list -> string
    9.12    val output_symbols: Symbol.symbol list -> string
    9.13 @@ -41,6 +44,11 @@
    9.14  
    9.15  (* output symbols *)
    9.16  
    9.17 +val latex_control = "\<^latex>";
    9.18 +fun is_latex_control s = s = latex_control;
    9.19 +
    9.20 +val embed_raw = prefix latex_control o cartouche;
    9.21 +
    9.22  local
    9.23  
    9.24  val char_table =
    9.25 @@ -95,13 +103,27 @@
    9.26    | Symbol.UTF8 s => s
    9.27    | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
    9.28    | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
    9.29 -  | Symbol.Raw s => s
    9.30 +  | Symbol.Raw _ => error "Bad raw symbol"
    9.31    | Symbol.Malformed s => error (Symbol.malformed_msg s)
    9.32    | Symbol.EOF => error "Bad EOF symbol");
    9.33  
    9.34 +fun scan_latex known =
    9.35 +  Scan.one (is_latex_control o Symbol_Pos.symbol) |--
    9.36 +    Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
    9.37 +  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
    9.38 +
    9.39 +fun read_latex known syms =
    9.40 +  (case Scan.read Symbol_Pos.stopper (Scan.repeat (scan_latex known))
    9.41 +      (map (rpair Position.none) syms) of
    9.42 +    SOME ss => implode ss
    9.43 +  | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)));
    9.44 +
    9.45  in
    9.46  
    9.47 -val output_known_symbols = implode oo (map o output_known_sym);
    9.48 +fun output_known_symbols known syms =
    9.49 +  if exists is_latex_control syms then read_latex known syms
    9.50 +  else implode (map (output_known_sym known) syms);
    9.51 +
    9.52  val output_symbols = output_known_symbols (K true, K true);
    9.53  val output_syms = output_symbols o Symbol.explode;
    9.54  
    9.55 @@ -192,7 +214,7 @@
    9.56  fun latex_indent "" _ = ""
    9.57    | latex_indent s _ = enclose "\\isaindent{" "}" s;
    9.58  
    9.59 -val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
    9.60 +val _ = Output.add_mode latexN latex_output embed_raw;
    9.61  val _ = Markup.add_mode latexN latex_markup;
    9.62  val _ = Pretty.add_mode latexN latex_indent;
    9.63