diff --git a/examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy b/examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy index 0d5d095..d50995f 100644 --- a/examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy +++ b/examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy @@ -1,7 +1,7 @@ theory PikeOS_ST (*Security Target *) imports "../../../src/ontologies/CC_v3.1_R5/CC_v3_1_R5" - (* Isabelle_DOF.CommonCriteria_15408 *) + (* Isabelle_DOF.CC_v3_1_R5 in the future. *) begin @@ -14,7 +14,7 @@ subsection*[pkosstrefsubsec::st_ref_cls]\ ST Reference \ text*[pkosstref::st_ref_cls, title="''PikeOS Security Target''", st_version ="(0,4,5)", authors= "[]", st_date= "''29072020''"] -\This document is the @{docitem st_def} for the Common Criteria evaluation of PikeOS. +\This document is the @{docitem st} for the Common Criteria evaluation of PikeOS. It complies with the Common Criteria for Information Technology Security Evaluation Version 3.1 Revision 4.\ @@ -29,7 +29,7 @@ text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''", Certification Kit build S4250 and PikeOS 3.4 Common Criteria Kit build S4388.\ subsection*[pkossttoeovrvwsubsec::st_ref_cls]\ TOE Overview \ -text*[pkosovrw1::toe_ovrw_cls]\The @{definition \toe_def\ } is a special kind of operating +text*[pkosovrw1::toe_ovrw_cls]\The @{definition \toe\ } is a special kind of operating system, that allows to effectively separate different applications running on the same platform from each other. The TOE can host user applications that can also be operating systems. User applications can also be diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 2b18be2..63d35a3 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -19,13 +19,13 @@ begin section\Document Local Setup.\ text\Some internal setup, introducing document specific abbreviations and macros.\ -setup \DOF_lib.define_shortcut ("dof",\<^here>) "\\dof"\ -setup \DOF_lib.define_shortcut ("isadof",\<^here>) "\\isadof"\ -setup \ DOF_lib.define_shortcut ("eg",\<^here>) "\\eg" - #> DOF_lib.define_shortcut ("ie",\<^here>) "\\ie"\ +setup \DOF_lib.define_shortcut \<^binding>\dof\ "\\dof"\ +setup \DOF_lib.define_shortcut \<^binding>\isadof\ "\\isadof"\ +setup \ DOF_lib.define_shortcut \<^binding>\eg\ "\\eg" + #> DOF_lib.define_shortcut \<^binding>\ie\ "\\ie"\ (* this is an alternative style for macro definitions eauivalent to setup ... setup ...*) -setup \ DOF_lib.define_shortcut ("TeXLive",\<^here>) "\\TeXLife" - #> DOF_lib.define_shortcut ("LaTeX",\<^here>) "\\LaTeX{}"\ +setup \ DOF_lib.define_shortcut \<^binding>\TeXLive\"\\TeXLife" + #> DOF_lib.define_shortcut \<^binding>\LaTeX\ "\\LaTeX{}"\ text\Note that these setups assume that the \<^LaTeX> macros are defined in the document prelude. \ diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy index 9660248..dac08d5 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy @@ -23,7 +23,7 @@ The linking of the \<^emph>\formal\ to the \<^emph>\informal\ digitization of knowledge and its propagation. This challenge incites numerous research efforts summarized under the labels ``semantic web,'' ``data mining,'' or any form of advanced ``semantic'' text processing. A key role in structuring this linking play \<^emph>\document ontologies\ (also called -\<^emph>\vocabulary\ in the semantic web community~@{cite "w3c:ontologies:2015"}), \ie, a machine-readable +\<^emph>\vocabulary\ in the semantic web community~@{cite "w3c:ontologies:2015"}), \<^ie>, a machine-readable form of the structure of documents as well as the document discourse. Such ontologies can be used for the scientific discourse within scholarly articles, mathematical @@ -42,21 +42,21 @@ In general, an ontology is a formal explicit description of \<^emph>\conce as \<^emph>\links\ between them. A particular link between concepts is the \<^emph>\is-a\ relation declaring the instances of a subclass to be instances of the super-class. -To adress this challenge, we present the Document Ontology Framework (\dof) and an -implementation of \dof called \isadof. \dof is designed for building scalable and user-friendly -tools on top of interactive theorem provers. \isadof is an instance of this novel framework, +To address this challenge, we present the Document Ontology Framework (\<^dof>) and an +implementation of \<^dof> called \<^isadof>. \<^dof> is designed for building scalable and user-friendly +tools on top of interactive theorem provers. \<^isadof> is an instance of this novel framework, implemented as extension of Isabelle/HOL, to \<^emph>\model\ typed ontologies and to \<^emph>\enforce\ them during document evolution. Based on Isabelle's infrastructures, ontologies may refer to types, terms, proven theorems, code, or established assertions. Based on a novel adaption of the Isabelle IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}), a document is checked to be -\<^emph>\conform\ to a particular ontology---\isadof is designed to give fast user-feedback \<^emph>\during the +\<^emph>\conform\ to a particular ontology---\<^isadof> is designed to give fast user-feedback \<^emph>\during the capture of content\. This is particularly valuable in case of document evolution, where the \<^emph>\coherence\ between the formal and the informal parts of the content can be mechanically checked. -To avoid any misunderstanding: \isadof is \<^emph>\not a theory in HOL\ on ontologies and operations to +To avoid any misunderstanding: \<^isadof> is \<^emph>\not a theory in HOL\ on ontologies and operations to track and trace links in texts, it is an \<^emph>\environment to write structured text\ which \<^emph>\may contain\ Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and -scientific papers---as the present one, which is written in \isadof itself. \isadof is a plugin +scientific papers---as the present one, which is written in \<^isadof> itself. \<^isadof> is a plugin into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}.\ subsubsection\How to Read This Manual\ @@ -69,28 +69,28 @@ declare_reference*[isadof_developers::text_section] text\ This manual can be read in different ways, depending on what you want to accomplish. We see three different main user groups: -\<^enum> \<^emph>\\isadof users\, \ie, users that just want to edit a core document, be it for a paper or a +\<^enum> \<^emph>\\<^isadof> users\, \<^ie>, users that just want to edit a core document, be it for a paper or a technical report, using a given ontology. These users should focus on @{docitem (unchecked) \isadof_tour\} and, depending on their knowledge of Isabelle/HOL, also @{docitem (unchecked) \background\}. -\<^enum> \<^emph>\Ontology developers\, \ie, users that want to develop new ontologies or modify existing +\<^enum> \<^emph>\Ontology developers\, \<^ie>, users that want to develop new ontologies or modify existing document ontologies. These users should, after having gained acquaintance as a user, focus on @{docitem (unchecked) \isadof_ontologies\}. -\<^enum> \<^emph>\\isadof developers\, \ie, users that want to extend or modify \isadof, \eg, by adding new +\<^enum> \<^emph>\\<^isadof> developers\, \<^ie>, users that want to extend or modify \<^isadof>, \<^eg>, by adding new text-elements. These users should read @{docitem (unchecked) \isadof_developers\} \ subsubsection\Typographical Conventions\ text\ - We acknowledge that understanding \isadof and its implementation in all details requires + We acknowledge that understanding \<^isadof> and its implementation in all details requires 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: + \<^item> a light-blue background for input written in Isabelle's Isar language, \<^eg>: \begin{isar} lemma refl: "x = x" by simp \end{isar} - \<^item> a green background for examples of generated document fragments (\ie, PDF output): + \<^item> a green background for examples of generated document fragments (\<^ie>, PDF output): \begin{out} The axiom refl \end{out} @@ -111,8 +111,8 @@ text\ subsubsection\How to Cite \isadof\ text\ - If you use or extend \isadof in your publications, please use - \<^item> for the \isadof system~@{cite "brucker.ea:isabelle-ontologies:2018"}: + If you use or extend \<^isadof> in your publications, please use + \<^item> for the \<^isadof> system~@{cite "brucker.ea:isabelle-ontologies:2018"}: \begin{quote}\small A.~D. Brucker, I.~Ait-Sadoune, P.~Crisafulli, and B.~Wolff. Using the {Isabelle} ontology framework: Linking the formal with the informal. In \<^emph>\Conference on Intelligent Computer @@ -122,9 +122,9 @@ text\ \end{quote} A \BibTeX-entry is available at: \url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018}. - \<^item> for the implementation of \isadof~@{cite "brucker.ea:isabelledof:2019"}: + \<^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 + A.~D. Brucker and B.~Wolff. \<^isadof>: Design and implementation. In P.C.~{\"O}lveczky and G.~Sala{\"u}n, editors, \<^emph>\Software Engineering and Formal Methods (SEFM)\, number 11724 in Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019. \href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}. @@ -136,7 +136,7 @@ text\ subsubsection\Availability\ text\ The implementation of the framework is available at - \url{\dofurl}. The website also provides links to the latest releases. \isadof is licensed + \url{\dofurl}. The website also provides links to the latest releases. \<^isadof> is licensed under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause). \ diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index b8a8678..500a789 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -1,7 +1,7 @@ (************************************************************************* * Copyright (C) - * 2019 The University of Exeter - * 2018-2019 The University of Paris-Saclay + * 2019-2020 The University of Exeter + * 2018-2020 The University of Paris-Saclay * 2018 The University of Sheffield * * License: @@ -49,14 +49,14 @@ The Isabelle system architecture shown in @{docitem \architecture\} with Standard ML (SML) at the bottom layer as implementation language. The architecture actually foresees a \<^emph>\Nano-Kernel\ (our terminology) which resides in the SML structure \inlinesml{Context}. This structure provides a kind of container called \<^emph>\context\ providing an identity, an -ancestor-list as well as typed, user-defined state for components (plugins) such as \isadof. +ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>. On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific support for higher specification constructs were built.\ -section*[dof::introduction]\The Document Model Required by \dof\ +section*[dof::introduction]\The Document Model Required by \<^dof> \ text\ In this section, we explain the assumed document model underlying our Document Ontology Framework - (\dof) in general. In particular we discuss the concepts \<^emph>\integrated document\, \<^emph>\sub-document\, + (\<^dof>) in general. In particular we discuss the concepts \<^emph>\integrated document\, \<^emph>\sub-document\, \<^emph>\text-element\ and \<^emph>\semantic macros\ occurring inside text-elements. Furthermore, we assume two different levels of parsers (for \<^emph>\outer\ and \<^emph>\inner syntax\) where the inner-syntax is basically a typed \inlineisar|\|-calculus and some Higher-order Logic (HOL). @@ -68,7 +68,7 @@ declare_reference*["fig:dependency"::text_section] text\ - We assume a hierarchical document model\index{document model}, \ie, an \<^emph>\integrated\ document + We assume a hierarchical document model\index{document model}, \<^ie>, an \<^emph>\integrated\ document consist of a hierarchy \<^emph>\sub-documents\ (files) that can depend acyclically on each other. Sub-documents can have different document types in order to capture documentations consisting of documentation, models, proofs, code of various forms and other technical artifacts. We call the @@ -91,9 +91,9 @@ text\ separate commands from each other. We distinguish fundamentally two different syntactic levels: - \<^item> the *\outer-syntax\\bindex{syntax!outer}\index{outer syntax|see {syntax, outer}} (\ie, the + \<^item> the *\outer-syntax\\bindex{syntax!outer}\index{outer syntax|see {syntax, outer}} (\<^ie>, the syntax for commands) is processed by a lexer-library and parser combinators built on top, and - \<^item> the *\inner-syntax\\bindex{syntax!inner}\index{inner syntax|see {syntax, inner}} (\ie, the + \<^item> the *\inner-syntax\\bindex{syntax!inner}\index{inner syntax|see {syntax, inner}} (\<^ie>, the syntax for \inlineisar|\|-terms in HOL) with its own parametric polymorphism type checking. @@ -101,19 +101,19 @@ text\ On the semantic level, we assume a validation process for an integrated document, where the semantics of a command is a transformation \inlineisar+\ \ \+ for some system state \inlineisar+\+. This document model can be instantiated with outer-syntax commands for common - text elements, \eg, \inlineisar+section{*...*}+ or \inlineisar+text{*...*}+. Thus, users can add + text elements, \<^eg>, \inlineisar+section{*...*}+ or \inlineisar+text{*...*}+. Thus, users can add informal text to a sub-document using a text command: \begin{isar} text\This is a description.\ \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, + translation is not necessarily one-to-one: text elements can be enriched by formal, \<^ie>, machine-checked content via *\semantic macros\, called antiquotations\bindex{antiquotation}: \begin{isar} text\According to the *\reflexivity\ axiom <@>{thm refl}, we obtain in \ for <@>{term "fac 5"} the result <@>{value "fac 5"}.\ \end{isar} -which is represented in the final document (\eg, a PDF) by: +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}}$. \end{out} @@ -132,41 +132,41 @@ figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hie section*[bgrnd21::introduction]\Implementability of the Required Document Model.\ text\ - 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 + 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 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 + features of \<^dof>. For example, current Isabelle versions offer cascade-syntaxes (different syntaxes and even parser-technologies which can be nested along the - \inlineisar+\ ... \ + barriers, while \dof actually only requires a two-level + \inlineisar+\ ... \ + barriers, while \<^dof> actually only requires a two-level syntax model. \ figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\ - The \isadof IDE (left) and the corresponding PDF (right), showing the first page + The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page of~\cite{brucker.ea:isabelle-ontologies:2018}.\ text\ - We call the present implementation of \dof on the Isabelle platform \isadof. + We call the present implementation of \<^dof> on the Isabelle platform \<^isadof> . @{docitem "fig:dof-ide"} shows a screen-shot of an introductory paper on - \isadof~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \isadof PIDE can be seen on the left, + \<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left, while the generated presentation in PDF is shown on the right. - Isabelle provides, beyond the features required for \dof, a lot of additional benefits. For + Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits. For example, it also allows the asynchronous evaluation and checking of the document content~@{cite "wenzel:asynchronous:2014" and "wenzel:system:2014" and "barras.ea:pervasive:2013"} and is dynamically extensible. Its PIDE provides a \<^emph>\continuous build, continuous check\ functionality, syntax highlighting, and auto-completion. - It also provides infrastructure for displaying meta-information (\eg, binding and type annotation) + It also provides infrastructure for displaying meta-information (\<^eg>, binding and type annotation) as pop-ups, while hovering over sub-expressions. A fine-grained dependency analysis allows the processing of individual parts of theory files asynchronously, allowing Isabelle to interactively process large (hundreds of theory files) documents. Isabelle can group sub-documents into sessions, - \ie, sub-graphs of the document-structure that can be ``pre-compiled'' and loaded - instantaneously, \ie, without re-processing. \ + \<^ie>, sub-graphs of the document-structure that can be ``pre-compiled'' and loaded + instantaneously, \<^ie>, without re-processing. \ (*<*) end diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index baa303b..99d698a 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -228,14 +228,22 @@ end section\Shortcuts, Macros, Environments\ text\This is actually \<^emph>\not\ a real DOF feature, rather a slightly more abstract layer over - slightly buried standard features of the Isabelle document generator ... \ + somewhat buried standard features of the Isabelle document generator ... \ ML\ structure DOF_lib = struct -fun define_shortcut (name, pos) latexshcut = - Thy_Output.antiquotation_raw (Binding.make(name,pos)) (Scan.succeed ()) +fun define_shortcut name latexshcut = + Thy_Output.antiquotation_raw name (Scan.succeed ()) (fn _ => fn () => Latex.string latexshcut) + +(* This is just a copy of Isabelle2020 function "control_antiquotation" from + document_antiquotations.ML, where it is unfortunately not exported. (Thanks Makarius!) + *) +fun define_macro name s1 s2 = + Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input) + (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false}); + end \ diff --git a/src/ontologies/CC_v3.1_R5/CC_terminology.thy b/src/ontologies/CC_v3.1_R5/CC_terminology.thy index 38a8e55..4761974 100644 --- a/src/ontologies/CC_v3.1_R5/CC_terminology.thy +++ b/src/ontologies/CC_v3.1_R5/CC_terminology.thy @@ -323,7 +323,7 @@ Definition* [sr_def::concept, tag="''security requirement''", short_tag="Some('' \requirement, stated in a standardised language, which is meant to contribute to achieving the security objectives for a TOE\ text \@{docitem toe_def}\ -Definition* [st_def::concept, tag="''Security Target''", short_tag="Some(''ST'')"] +Definition* [st::concept, tag="''Security Target''", short_tag="Some(''ST'')"] \implementation-dependent statement of security needs for a specific i\
dentified @{docitem toe_def}\ Definition* [slct_def::concept, tag="''selection''"] @@ -350,7 +350,7 @@ Definition* [st_eval_def::concept, tag="''ST evaluation''"] Definition* [subj_def::concept, tag="''subject''"] \active entity in the TOE that performs operations on objects\ -Definition* [toe_def::concept, tag= "''target of evaluation''"] +Definition* [toe::concept, tag= "''target of evaluation''"] \set of software, firmware and/or hardware possibly accompanied by guidance\ Definition* [thrt_agnt_def::concept, tag="''threat agent''"] @@ -417,7 +417,7 @@ Definition* [dev_def::concept, tag="''Developer''"] \who respond to actual or perceived consumer security requirements in constructing a @{docitem toe_def}, reference this CC_Part_3 when interpreting statements of assurance requirements and determining - assurance approaches of @{docitem toe_def}s.\ + assurance approaches of @{docitem toe}s.\ Definition*[evalu_def::concept, tag="'' Evaluator''"] \who use the assurance requirements defined in CC_Part_3 diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index e4096a6..19230cf 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -148,11 +148,15 @@ textN\... and here is its application macro expansion: textN\ \<^theory_text>\definition df = ... \ - @{ML [display] \ let val x = 3 + 4 in true end \} + @{ML [display] \ let val x = 3 + 4 in true end + \} + + @{ML_text [display] \ val x = ... + \} @{verbatim [display] \ Lorem ipsum ... @{thm refl} _ Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \} - @{theory_text [display] \definition df = ... + @{theory_text [display] \definition df = ... \x. \} @{cartouche [display] \ @{figure "cfgdfg"}\} \ @@ -180,10 +184,19 @@ val _ = textN\ \<^doof> \<^LATEX> \ (* the same effect is achieved with : *) -setup \DOF_lib.define_shortcut ("bla",\<^here>) "\\blabla"\ -(* Note that this assumes that the generated LaTeX macro "blabla" is defined somewhere in the - target document, for example, in the tex prelude. *) +setup \DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\ +(* Note that this assumes that the generated LaTeX macro call "\blabla" is defined somewhere in the + target document, for example, in the tex prelude. Note that the "Binding.make" can be avoided + using the alternative \<^binding> notation (see above).*) +ML\ + +fun control_antiquotation name s1 s2 = + Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input) + (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false}); + +\ + end (*>*)