Improvements: @{boxed_theory_text [display] ... }.

examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy

@@ -86,23 +86,9 @@ text\<open>
   separating multiple technological layers or languages. To help the reader with this, we 
   will type-set the different languages in different styles. In particular, we will use 
   \<^item> a light-blue background for input written in Isabelle's Isar language, \<^eg>:
-
-
-    @{boxed_theory_text [display]\<open>
-    lemma refl: "x = x" 
-      by simp
-    \<close>}
-
-%    @ {boxed_isar [display]
-%      \<open>lemma refl: "x = x" 
-%         by simp\<close>}
-
-    \<^boxed_isar>\<open>lemma refl: "x = x"\<close>
-
     @{boxed_theory_text [display]
     \<open>lemma refl: "x = x" 
       by simp\<close>}
-
   \<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
     @{boxed_pdf [display] \<open>The axiom refl\<close>}
   \<^item> a red background for For (S)ML-code:

examples/technical_report/Isabelle_DOF-Manual/02_Background.thy

@@ -78,8 +78,8 @@ text\<open>
   consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body 
   consisting of a sequence of \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even 
   the header consists of a sequence of commands used for introductory text elements not depending on 
-  any context. The context-definition contains an \<^boxed_isar>\<open>import\<close> and a 
-  \<^boxed_isar>\<open>keyword\<close> section, for example:
+  any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a 
+  \<^boxed_theory_text>\<open>keyword\<close> section, for example:
 @{boxed_theory_text [display]\<open>
   theory Example         (* Name of the 'theory'                     *)
     imports              (* Declaration of 'theory' dependencies     *)
@@ -87,8 +87,8 @@ text\<open>
     keywords             (* Registration of keywords defined locally *)
       requirement        (* A command for describing requirements    *)
 \<close>}
-  where \<^boxed_isar>\<open>Example\<close> is the abstract name of the text-file, \<^boxed_isar>\<open>Main\<close> refers to an 
-  imported theory (recall that the import relation must be acyclic) and \inlineisar{keywords} are 
+  where \<^boxed_theory_text>\<open>Example\<close> is the abstract name of the text-file, \<^boxed_isar>\<open>Main\<close> refers to an 
+  imported theory (recall that the import relation must be acyclic) and \<^boxed_theory_text>\<open>keywords\<close> are 
   used to separate commands from each other.
 \<close>
 (* experiment starts here *)

examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy

@@ -1,7 +1,7 @@
 (*************************************************************************
  * Copyright (C) 
- *               2019      The University of Exeter 
- *               2018-2019 The University of Paris-Saclay
+ *               2019-2020 University of Exeter 
+ *               2018-2020 University of Paris-Saclay
  *               2018      The University of Sheffield
  *
  * License:
@@ -659,11 +659,10 @@ text\<open>
   accept-clause\index{accept-clause} contains a regular expression over class identifiers. 
   For example:
 
- TODO bsub/esub
   @{boxed_theory_text [display]\<open>
   doc_class article = style_id :: string   <= "''CENELEC_50128''"
-      accepts "(title ~~ \<lbrace>author\<rbrace> bsup+esup ~~ abstract ~~ \<lbrace>introduction\<rbrace> bsup+esup  ~~
-               \<lbrace>technical || example\<rbrace> bsup+esup ~~ \<lbrace>conclusion\<rbrace> bsup+esup)"
+      accepts "(title ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ abstract ~~ \<lbrace>introduction\<rbrace>\<^sup>+ ~~
+               \<lbrace>technical || example\<rbrace>\<^sup>+ ~~ \<lbrace>conclusion\<rbrace>\<^sup>+)"
   \<close>}
 
   Semantically, monitors introduce a behavioral element into ODL:

examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty

@@ -182,8 +182,11 @@
 
 \providecolor{isar}{named}{blue}
 \def\inlineisar{\lstinline[style=isar,breaklines=true,mathescape,breakatwhitespace=true]}
-\newtcblisting{isar}[1][]{%
-      listing only%
+
+\renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}}
+\newcommand{\inlineisarbox}[1]{#1}
+
+\NewTColorBox[]{isarbox}{}{
      ,boxrule=0pt
      ,boxsep=0pt
      ,colback=white!90!isar
@@ -197,13 +200,8 @@
      ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north
        east,font=\bfseries\footnotesize\color{white}]
                 at (frame.north east) {Isar};}
-     ,listing options={
-          style=isar
-          ,basicstyle=\small\ttfamily
-         ,mathescape
-         ,#1
-      }
-  }%
+}
+
 %% </isar>
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 

examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex

@@ -117,20 +117,3 @@ France, and therefore granted with public funds of the Program ``Investissements
 }
 
 \AtBeginDocument{\isabellestyle{literal}\newcommand{\lstnumberautorefname}{Line}}
-\renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}}
-
-\NewTColorBox[]{isarbox}{}{
-     ,boxrule=0pt
-     ,boxsep=0pt
-     ,colback=white!90!isar
-     ,enhanced jigsaw
-     ,borderline west={2pt}{0pt}{isar!60!black}
-     ,sharp corners
-     % ,before skip=10pt
-     % ,after skip=10pt
-     ,enlarge top by=0mm
-     ,enhanced
-     ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north
-       east,font=\bfseries\footnotesize\color{white}]
-                at (frame.north east) {Isar};}
-}