From 3dabf4fc82012c3b750206674c89e7abf5e65b67 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 8 Sep 2020 06:51:36 +0100 Subject: [PATCH] Improvements: @{boxed_theory_text [display] ... }. --- .../Isabelle_DOF-Manual/01_Introduction.thy | 14 -------------- .../Isabelle_DOF-Manual/02_Background.thy | 8 ++++---- .../Isabelle_DOF-Manual/04_RefMan.thy | 9 ++++----- .../document/lstisadof-manual.sty | 16 +++++++--------- .../Isabelle_DOF-Manual/document/preamble.tex | 17 ----------------- 5 files changed, 15 insertions(+), 49 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy index 65de821..a45e528 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy @@ -86,23 +86,9 @@ text\ 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]\ - lemma refl: "x = x" - by simp - \} - -% @ {boxed_isar [display] -% \lemma refl: "x = x" -% by simp\} - - \<^boxed_isar>\lemma refl: "x = x"\ - @{boxed_theory_text [display] \lemma refl: "x = x" by simp\} - \<^item> a green background for examples of generated document fragments (\<^ie>, PDF output): @{boxed_pdf [display] \The axiom refl\} \<^item> a red background for For (S)ML-code: diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index 5630494..5fab9f1 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -78,8 +78,8 @@ text\ consists of a \<^emph>\header\\<^bindex>\header\, a \<^emph>\context definition\\<^index>\context\, and a body consisting of a sequence of \<^emph>\command\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>\import\ and a - \<^boxed_isar>\keyword\ section, for example: + any context. The context-definition contains an \<^boxed_theory_text>\import\ and a + \<^boxed_theory_text>\keyword\ section, for example: @{boxed_theory_text [display]\ theory Example (* Name of the 'theory' *) imports (* Declaration of 'theory' dependencies *) @@ -87,8 +87,8 @@ text\ keywords (* Registration of keywords defined locally *) requirement (* A command for describing requirements *) \} - where \<^boxed_isar>\Example\ is the abstract name of the text-file, \<^boxed_isar>\Main\ refers to an - imported theory (recall that the import relation must be acyclic) and \inlineisar{keywords} are + where \<^boxed_theory_text>\Example\ is the abstract name of the text-file, \<^boxed_isar>\Main\ refers to an + imported theory (recall that the import relation must be acyclic) and \<^boxed_theory_text>\keywords\ are used to separate commands from each other. \ (* experiment starts here *) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index aa65cee..90761a2 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/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\ accept-clause\index{accept-clause} contains a regular expression over class identifiers. For example: - TODO bsub/esub @{boxed_theory_text [display]\ doc_class article = style_id :: string <= "''CENELEC_50128''" - accepts "(title ~~ \author\ bsup+esup ~~ abstract ~~ \introduction\ bsup+esup ~~ - \technical || example\ bsup+esup ~~ \conclusion\ bsup+esup)" + accepts "(title ~~ \author\\<^sup>+ ~~ abstract ~~ \introduction\\<^sup>+ ~~ + \technical || example\\<^sup>+ ~~ \conclusion\\<^sup>+)" \} Semantically, monitors introduce a behavioral element into ODL: diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty index 10fd05f..cd6c535 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty +++ b/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 - } - }% +} + %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index d13f81d..38cb1d8 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/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};} -}