Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

added wrapper to achims listings environments.

This commit is contained in:
Burkhart Wolff 2020-08-28 12:42:20 +02:00
parent d206bf9f7c
commit 094281cf89
6 changed files with 118 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy
View File

@ -46,11 +46,41 @@ fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
(fn ctxt => DOF_lib.string_2_text_antiquotation ctxt
#> DOF_lib.enclose_env ctxt "isarbox")
val neant = K(Latex.text("",\<^here>))
fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) =
DOF_lib.gen_text_antiquotation name DOF_lib.report_theory_text
(fn ctxt => DOF_lib.string_2_theory_text_antiquotation ctxt
#> DOF_lib.enclose_env ctxt "isarbox")
#> DOF_lib.enclose_env ctxt "isarbox"
(* #> neant *)) (*debugging *)
fun boxed_sml_text_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "sml")
(* the simplest conversion possible *)
fun boxed_pdf_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "out")
(* the simplest conversion possible *)
fun boxed_latex_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "ltx")
(* the simplest conversion possible *)
fun boxed_bash_antiquotation name =
DOF_lib.gen_text_antiquotation name (K(K()))
(fn ctxt => Input.source_content
#> Latex.text
#> DOF_lib.enclose_env ctxt "bash")
(* the simplest conversion possible *)
\<close>
@ -59,7 +89,12 @@ setup\<open>(* std_text_antiquotation \<^binding>\<open>my_text\<close> #
(* std_text_antiquotation \<^binding>\<open>my_cartouche\<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>\<close>
boxed_theory_text_antiquotation \<^binding>\<open>boxed_theory_text\<close> #>
boxed_sml_text_antiquotation \<^binding>\<open>boxed_sml\<close> #>
boxed_pdf_antiquotation \<^binding>\<open>boxed_pdf\<close> #>
boxed_latex_antiquotation \<^binding>\<open>boxed_latex\<close>#>
boxed_bash_antiquotation \<^binding>\<open>boxed_bash\<close>\<close>
@ -85,7 +120,7 @@ text*[abs::abstract,
\<open> \<^isadof> provides an implementation of \<^dof> on top of Isabelle/HOL.
\<^dof> itself is a novel framework for \<^emph>\<open>defining\<close> ontologies
and \<^emph>\<open>enforcing\<close> them during document development and document
evolution. \<^isadof> targets use-cases such as mathematical texts referring
evolution. \<^isadof> targets use-cases such as mathematical texts referring
to a theory development or technical reports requiring a particular structure.
A major application of \<^dof> is the integrated development of
formal certification documents (\<^eg>, for Common Criteria or CENELEC

32
examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
View File

@ -90,26 +90,34 @@ text\<open>
lemma refl: "x = x"
by simp
\end{isar}
% @ {boxed_isar [display]
% \<open>lemma refl: "x = x"
% by simp\<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):
\begin{out}
The axiom refl
\end{out}
@{boxed_pdf [display] \<open>The axiom refl\<close>}
\<^item> a red background for For (S)ML-code:
\begin{sml}
fun id x = x
\end{sml}
@{boxed_sml [display] \<open>fun id x = x\<close>}
\<^item> a yellow background for \LaTeX-code:
@{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>}
\begin{ltx}
\newcommand{\refl}{$x = x$}
\end{ltx}
\<^item> a grey background for shell scripts and interactive shell sessions:
@{boxed_bash [display]
\<open>ë\prompt{}ë ls
CHANGELOG.md CITATION examples install LICENSE README.md ROOTS src\<close>}
\begin{bash}
ë\prompt{}ë ls
CHANGELOG.md CITATION examples install LICENSE README.md ROOTS src
\end{bash}
\end{bash}
\<close>
subsubsection\<open>How to Cite \isadof\<close>
subsubsection\<open>How to Cite \<^isadof>\<close>
text\<open>
If you use or extend \<^isadof> in your publications, please use
\<^item> for the \<^isadof> system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
@ -120,8 +128,8 @@ text\<open>
Heidelberg, 2018. \href{https://doi.org/10.1007/978-3-319-96812-4\_3}
{10.1007/978-3-319-96812-4\_3}.
\end{quote}
A \BibTeX-entry is available at:
\url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018}.
A \<^BibTeX>-entry is available at:
\<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018\<close>.
\<^item> for the implementation of \<^isadof>~@{cite "brucker.ea:isabelledof:2019"}:
\begin{quote}\small
A.~D. Brucker and B.~Wolff. \<^isadof>: Design and implementation. In P.C.~{\"O}lveczky and
@ -130,8 +138,8 @@ text\<open>
\href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}.
\end{quote}
A \BibTeX-entry is available at:
\url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019}.
A \<^BibTeX>-entry is available at:
\<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019\<close>.
\<close>
subsubsection\<open>Availability\<close>
text\<open>

63
examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
View File

@ -89,38 +89,67 @@ text\<open>
\inlineisar{Main} refers to an imported theory (recall that the import
relation must be acyclic) and \inlineisar{keywords} are used to
separate commands from each other.
\<close>
(* experiment starts here *)
(* somewhere we destroyed the standard antiquotation thm ...
text\<open> \<^emph>\<open>blabla\<close> @{thm \<open>refl\<close>}\<close>
text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
for @{term "fac 5"} the result @{value "fac 5"}.\<close>
*)
text\<open> \<^theory_text>\<open>text\<open> According to the *\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>\<close>
text\<open>
We distinguish fundamentally two different syntactic levels:
\<^item> the \<^emph>\<open>outer-syntax\<close>\<^bindex>\<open>syntax!outer\<close>\<^index>\<open>outer syntax|see {syntax, outer}\<close> (\<^ie>, the
syntax for commands) is processed by a lexer-library and parser combinators built on top, and
\<^item> the \<^emph>\<open>inner-syntax\<close>\<^bindex>\<open>syntax!inner\<close>\<^index>\<open>inner syntax|see {syntax, inner}\<close> (\<^ie>, the
syntax for \inlineisar|\<lambda>|-terms in HOL) with its own parametric polymorphism type
checking.
syntax for \<open>\<lambda>\<close>-terms in HOL) with its own parametric polymorphism type checking.
On the semantic level, we assume a validation process for an integrated document, where the
semantics of a command is a transformation \inlineisar+\<theta> \<rightarrow> \<theta>+ for some system state
\inlineisar+\<theta>+. This document model can be instantiated with outer-syntax commands for common
text elements, \<^eg>, \inlineisar+section\<Open>...\<Close>+ or \inlineisar+text\<Open>...\<Close>+.
semantics of a command is a transformation \<open>\<theta> \<rightarrow> \<theta>\<close> for some system state \<open>\<theta>\<close>.
This document model can be instantiated with outer-syntax commands for common
text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>.
Thus, users can add informal text to a sub-document using a text command:
@{boxed_theory_text [display] \<open>text\<open>This is a description.\<close>\<close> }
\begin{isar}
text\<Open>This is a description.\<Close>
\end{isar}
This will type-set the corresponding text in, for example, a PDF document. However, this
translation is not necessarily one-to-one: text elements can be enriched by formal, \<^ie>,
machine-checked content via *\<open>semantic macros\<close>, called antiquotations\<^bindex>\<open>antiquotation\<close>:
@{boxed_theory_text [display]
\<open>text\<open> According to the *\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>
}
\begin{isar}
text\<Open>According to the *\<Open>reflexivity\<Close> axiom <@>{thm refl}, we obtain in \<Gamma>
for <@>{term "fac 5"} the result <@>{value "fac 5"}.\<Close>
\end{isar}
which is represented in the final document (\<^eg>, a PDF) by:
\begin{out}
According to the \emph{reflexivity} axiom $\mathrm{x = x}$, we obtain in $\Gamma$ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.
According to the \emph{reflexivity} axiom $\mathrm{x = x}$, we obtain in $\Gamma$
for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.
\end{out}
Semantic macros are partial functions of type \inlineisar+\<theta> \<rightarrow> text+; since they can use the
@{boxed_pdf [display]
\<open>According to the \emph{reflexivity} axiom $\mathrm{x = x}$, we obtain in $\Gamma$
for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.\<close>
}
Semantic macros are partial functions of type \<open>\<theta> \<rightarrow> text\<close>; since they can use the
system state, they can perform all sorts of specific checks or evaluations (type-checks,
executions of code-elements, references to text-elements or proven theorems such as
\inlineisar+refl+, which is the reference to the axiom of reflexivity).
\<open>refl\<close>, which is the reference to the axiom of reflexivity).
Semantic macros establish \<^emph>\<open>formal content\<close> inside informal content; they can be
type-checked before being displayed and can be used for calculations before being
@ -133,17 +162,15 @@ figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hie
section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model.\<close>
text\<open>
Batch-mode checkers for \<^dof> can be implemented in all systems of the LCF-style prover family,
\<^ie>, systems with a type-checked \inlinesml{term}, and abstract \inlinesml{thm}-type for
theorems (protected by a kernel). This includes, \<^eg>, ProofPower, HOL4, HOL-light, Isabelle, or
Coq and its derivatives. \<^dof> is, however, designed for fast interaction in an IDE. If a user wants
\<^ie>, systems with a type-checked \<open>term\<close>, and abstract \<open>thm\<close>-type for theorems
(protected by a kernel). This includes, \<^eg>, ProofPower, HOL4, HOL-light, Isabelle, or Coq
and its derivatives. \<^dof> is, however, designed for fast interaction in an IDE. If a user wants
to benefit from this experience, only Isabelle and Coq have the necessary infrastructure of
asynchronous proof-processing and support by a PIDE~@{cite "wenzel:asynchronous:2014" and
"wenzel:system:2014" and "barras.ea:pervasive:2013"
and "faithfull.ea:coqoon:2018"} which in many features over-accomplishes the required
features of \<^dof>. For example, current Isabelle versions offer cascade-syntaxes (different
syntaxes and even parser-technologies which can be nested along the
\inlineisar+\<Open> ... \<Close> + barriers, while \<^dof> actually only requires a two-level
syntax model.
"wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"} which
in many features over-accomplishes the required features of \<^dof>. For example, current Isabelle
versions offer cascade-syntaxes (different syntaxes and even parser-technologies which can be
nested along the \<open>\<open>...\<close>\<close> barriers, while \<^dof> actually only requires a two-level syntax model.
\<close>
figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\<open>
@ -168,6 +195,8 @@ text\<open>
\<^ie>, sub-graphs of the document-structure that can be ``pre-compiled'' and loaded
instantaneously, \<^ie>, without re-processing. \<close>
(* end experiment *)
(*<*)
end
(*>*)

12
examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
View File

@ -118,6 +118,16 @@ 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{mybox}[1]{colback=red!5!white,colframe=red!75!black,fonttitle=\bfseries,title=#1},
%\newenvironment{isarbox}
%{\begin{mybox}}
%{\end{mybox}}
%\newenvironment{isarbox}
%{\begin{isar}}
%{\end{isar}}
\newenvironment{isarbox}
{AAA - bu isarbox}
{ZZZ - bu isarbox}
{ZZZ - bu isarbox}

2
src/DOF/Isa_COL.thy
View File

@ -375,7 +375,7 @@ fun theory_text_antiquotation name =
fun enclose_env ctxt block_env body =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Latex.environment_block block_env [body]
else body;
else Latex.block ([Latex.string (block_env ^"inline{")] @ [body] @ [ Latex.string ("}")]);
end
\<close>

4
src/tests/OutOfOrderPresntn.thy
View File

@ -316,8 +316,8 @@ val _ = Theory.setup
\<close>
textN\<open>
@{boxed_cartouche [display] \<open>definition dfg = \<lambda>x. x\<close>}
@{boxed_theory_text [display] \<open>doc_class dfg = ...\<close>} \<close>
@{boxed_cartouche [display] \<open>definition dfg = \<lambda>x. x\<close>}
@{boxed_theory_text [display] \<open>doc_class dfg = \<lambda>x... \<Gamma>\<close>} \<close>
end
(*>*)