From 0f48f356df49b5b123e634a212ba7ba814373602 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Wed, 26 Apr 2023 18:58:01 +0200
Subject: [PATCH] Fix sml latex environment issue with "$"

---
 .../CENELEC_50128/mini_odo/document/lstisadof.sty  |  5 +++--
 .../document/lstisadof-manual.sty                  |  4 ++--
 Isabelle_DOF/document/lstisadof-manual.sty         | 14 +++++++-------
 Isabelle_DOF/thys/manual/M_00_Frontmatter.thy      |  9 ++-------
 4 files changed, 14 insertions(+), 18 deletions(-)

diff --git a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/lstisadof.sty b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/lstisadof.sty
index a2b6e19a..3e85bae1 100644
--- a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/lstisadof.sty
+++ b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/lstisadof.sty
@@ -179,7 +179,8 @@
 %%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%
 \lstloadlanguages{ML}
-\lstdefinestyle{sml}{basicstyle=\ttfamily,%
+\lstdefinestyle{sml}{escapechar=ë,%
+                     basicstyle=\ttfamily,%
                      commentstyle=\itshape,%
                      keywordstyle=\bfseries\color{CornflowerBlue},%
                      ndkeywordstyle=\color{red},%
@@ -193,4 +194,4 @@
     frame=lines,
     basicstyle=\footnotesize\ttfamily,#1}}{}
 %%% 
-\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}
+\def\inlinesml{\lstinline[style=sml,breaklines=true,breakatwhitespace=true]}
diff --git a/Isabelle_DOF-Ontologies/document/lstisadof-manual.sty b/Isabelle_DOF-Ontologies/document/lstisadof-manual.sty
index 64516fcd..38701bbd 100644
--- a/Isabelle_DOF-Ontologies/document/lstisadof-manual.sty
+++ b/Isabelle_DOF-Ontologies/document/lstisadof-manual.sty
@@ -136,6 +136,7 @@
 \lstloadlanguages{ML}
 \providecolor{sml}{named}{red}
 \lstdefinestyle{sml}{
+   escapechar=ë,%
    basicstyle=\ttfamily,%
    commentstyle=\itshape,%
    keywordstyle=\bfseries\color{CornflowerBlue},%
@@ -150,7 +151,7 @@
    ,tagstyle=\color{CornflowerBlue}%
    ,markfirstintag=true%
 }%
-\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}
+\def\inlinesml{\lstinline[style=sml,breaklines=true,breakatwhitespace=true]}
 \newtcblisting{sml}[1][]{%
       listing only%
      ,boxrule=0pt
@@ -170,7 +171,6 @@
           style=sml
           ,columns=flexible%
           ,basicstyle=\small\ttfamily
-          ,mathescape
           ,#1
       }
   }%
diff --git a/Isabelle_DOF/document/lstisadof-manual.sty b/Isabelle_DOF/document/lstisadof-manual.sty
index 64516fcd..c9d2605d 100644
--- a/Isabelle_DOF/document/lstisadof-manual.sty
+++ b/Isabelle_DOF/document/lstisadof-manual.sty
@@ -136,11 +136,12 @@
 \lstloadlanguages{ML}
 \providecolor{sml}{named}{red}
 \lstdefinestyle{sml}{
-   basicstyle=\ttfamily,%
-   commentstyle=\itshape,%
-   keywordstyle=\bfseries\color{CornflowerBlue},%
-   ndkeywordstyle=\color{green},%
-   language=ML
+   ,escapechar=ë%
+   ,basicstyle=\ttfamily%
+   ,commentstyle=\itshape%
+   ,keywordstyle=\bfseries\color{CornflowerBlue}%
+   ,ndkeywordstyle=\color{green}%
+   ,language=ML
 %  ,literate={%
 %     {<@>}{@}1%
 %    }
@@ -150,7 +151,7 @@
    ,tagstyle=\color{CornflowerBlue}%
    ,markfirstintag=true%
 }%
-\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}
+\def\inlinesml{\lstinline[style=sml,breaklines=true,breakatwhitespace=true]}
 \newtcblisting{sml}[1][]{%
       listing only%
      ,boxrule=0pt
@@ -170,7 +171,6 @@
           style=sml
           ,columns=flexible%
           ,basicstyle=\small\ttfamily
-          ,mathescape
           ,#1
       }
   }%
diff --git a/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy b/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy
index 6b338639..854f38fa 100644
--- a/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy
+++ b/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy
@@ -42,7 +42,6 @@ define_macro* nolinkurl \<rightleftharpoons> \<open>\nolinkurl{\<close> _ \<open
 define_macro* center    \<rightleftharpoons> \<open>\center{\<close> _ \<open>}\<close>
 define_macro* ltxinline \<rightleftharpoons> \<open>\inlineltx|\<close> _ \<open>|\<close>
 
-ML\<open>curry (op ^) "[mathescape=false]" \<close>
 ML\<open>
 
 fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
@@ -61,10 +60,9 @@ fun boxed_theory_text_antiquotation name (* redefined in these more abstract ter
 fun boxed_sml_text_antiquotation name  =
     DOF_lib.gen_text_antiquotation name (K(K())) 
                            (fn ctxt => Input.source_content 
-                                        #> apfst (curry (op ^) "[mathescape=false]")
                                         #> Latex.text 
                                         #> DOF_lib.enclose_env true ctxt "sml") 
-                           (* the simplest conversion possible, preseving $ symbols *)
+                           (* the simplest conversion possible *)
 
 fun boxed_pdf_antiquotation name =
     DOF_lib.gen_text_antiquotation name (K(K())) 
@@ -88,11 +86,8 @@ fun boxed_bash_antiquotation name =
                            (* the simplest conversion possible *)
 \<close>
 
-setup\<open>(* std_text_antiquotation        \<^binding>\<open>my_text\<close> #> *)
-      boxed_text_antiquotation         \<^binding>\<open>boxed_text\<close> #>
-      (* std_text_antiquotation        \<^binding>\<open>my_cartouche\<close> #> *)
+setup\<open>boxed_text_antiquotation         \<^binding>\<open>boxed_text\<close> #>
       boxed_text_antiquotation         \<^binding>\<open>boxed_cartouche\<close> #>
-      (* std_theory_text_antiquotation \<^binding>\<open>my_theory_text\<close>#> *)
       boxed_theory_text_antiquotation  \<^binding>\<open>boxed_theory_text\<close> #>
 
       boxed_sml_text_antiquotation     \<^binding>\<open>boxed_sml\<close> #>