diff --git a/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy b/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy
index 27b42c8f..259b0c98 100644
--- a/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy
+++ b/Isabelle_DOF/thys/manual/M_00_Frontmatter.thy
@@ -42,7 +42,7 @@ 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,6 +61,7 @@ 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 *)
diff --git a/Isabelle_DOF/thys/manual/M_05_Implementation.thy b/Isabelle_DOF/thys/manual/M_05_Implementation.thy
index e28c8b89..0649f2ca 100644
--- a/Isabelle_DOF/thys/manual/M_05_Implementation.thy
+++ b/Isabelle_DOF/thys/manual/M_05_Implementation.thy
@@ -22,10 +22,10 @@ chapter*[isadof_developers::text_section]\<open>Extending \<^isadof>\<close>
 text\<open>
   In this chapter, we describe the basic implementation aspects of \<^isadof>, which is based on 
   the following design-decisions:
-  \<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign the possibility to 
+  \<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign to the possibility to 
     modify Isabelle itself,
-  \<^item> we made a small exception to this rule: the \<^isadof> package modifies in its installation 
-    about 10 lines in the \LaTeX-generator (\path{src/patches/thy_output.ML}),
+  \<^item> \<^isadof> has been organized as an AFP entry and a form of an Isabelle component that is
+    compatible with this goal,
   \<^item> we decided to make the markup-generation by itself to adapt it as well as possible to the 
     needs of tracking the linking in documents,
   \<^item> \<^isadof> is deeply integrated into the Isabelle's IDE (PIDE) to give immediate feedback during 
@@ -95,10 +95,11 @@ op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \<close>}
   for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing 
   combinators have the advantage that they can be integrated into standard programs, 
   and they enable the dynamic extension of the grammar. There is a more high-level structure 
-  \inlinesml{Parse} providing specific combinators for the command-language Isar:
+  \<^boxed_sml>\<open>Parse\<close> providing specific combinators for the command-language Isar:
 
-\begin{sml}[mathescape=false]
-val attribute = Parse.position Parse.name 
+% boxed_sml does not work here due to the dollar symbols. Repair: mathescape option in sty ?
+@{boxed_sml [display]
+\<open>val attribute = Parse.position Parse.name 
               -- Scan.optional(Parse.$$$ "=" |-- Parse.!!! Parse.name)"";
 val reference = Parse.position Parse.name 
               -- Scan.option (Parse.$$$ "::" |-- Parse.!!!
@@ -106,7 +107,7 @@ val reference = Parse.position Parse.name
 val attributes =(Parse.$$$ "[" |-- (reference 
                -- (Scan.optional(Parse.$$$ ","
                    |--(Parse.enum ","attribute)))[]))--| Parse.$$$ "]"              
-\end{sml}                                            
+\<close>}                                          
 
   The ``model'' \<^boxed_sml>\<open>create_and_check_docitem\<close> and ``new''
   \<^boxed_sml>\<open>ODL_Meta_Args_Parser.attributes\<close> parts were 
@@ -171,7 +172,7 @@ section\<open>Implementing Second-level Type-Checking\<close>
 text\<open>
   On expressions for attribute values, for which we chose to use HOL syntax to avoid that users 
   need to learn another syntax, we implemented an own pass over type-checked terms. Stored in the 
-  late-binding table \<^boxed_sml>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation 
+  late-binding table \<^boxed_sml>\<open>ISA_transformer_tab\<close>, we register for each term-annotation 
   (ISA's), a function of type
 
 @{boxed_sml [display]