forked from Isabelle_DOF/Isabelle_DOF
...
This commit is contained in:
Burkhart Wolff
commit
db4290428f
|
|
@ -206,7 +206,7 @@ The current system framework offers moreover the following features:
|
|||
the most prominent and deeply integrated system component.
|
||||
\<close>
|
||||
|
||||
figure*[architecture::figure,relative_width="100",src="''figures/isabelle-architecture''"]\<open>
|
||||
figure*[architecture::figure,relative_width="100",file_src="''figures/isabelle-architecture.pdf''"]\<open>
|
||||
The system architecture of Isabelle (left-hand side) and the
|
||||
asynchronous communication between the Isabelle system and
|
||||
the IDE (right-hand side). \<close>
|
||||
|
|
@ -315,7 +315,7 @@ Isabelle users to Isabelle users only. Of course, such references can be added e
|
|||
represent a particular strength of \<^isadof>.\<close>
|
||||
|
||||
text*["paper_onto_core"::float,
|
||||
caption="\<open>The core of the ontology definition for writing scholarly papers.\<close>"]
|
||||
main_caption="\<open>The core of the ontology definition for writing scholarly papers.\<close>"]
|
||||
\<open>@{boxed_theory_text [display]\<open>
|
||||
doc_class title =
|
||||
short_title :: "string option" <= None
|
||||
|
|
@ -350,7 +350,7 @@ The translation of its content to, \<^eg>, Springer's \<^LaTeX> setup for the Le
|
|||
Science Series, as required by many scientific conferences, is mostly straight-forward.
|
||||
\<^vs>\<open>-0.8cm\<close>\<close>
|
||||
|
||||
figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
|
||||
figure*[fig1::figure,relative_width="95",file_src="''figures/Dogfood-Intro.png''"]
|
||||
\<open> Ouroboros I: This paper from inside \<^dots> \<close>
|
||||
|
||||
(*<*)declare_reference*[paper_onto_sections::float](*>*)
|
||||
|
|
@ -385,7 +385,7 @@ of the scope of this paper.
|
|||
|
||||
We proceed more or less conventionally by the subsequent sections (@{float (unchecked)\<open>paper_onto_sections\<close>})\<close>
|
||||
text*["paper_onto_sections"::float,
|
||||
caption = "''Various types of sections of a scholarly papers.''"]\<open>
|
||||
main_caption = "''Various types of sections of a scholarly papers.''"]\<open>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class example = text_section +
|
||||
comment :: string
|
||||
|
|
@ -403,7 +403,7 @@ doc_class bibliography =
|
|||
text\<open>... and finish with a monitor class definition that enforces a textual ordering
|
||||
in the document core by a regular expression (@{float (unchecked) "paper_onto_monitor"}).\<close>
|
||||
text*["paper_onto_monitor"::float,
|
||||
caption = "''A monitor for the scholarly paper ontology.''"]\<open>
|
||||
main_caption = "''A monitor for the scholarly paper ontology.''"]\<open>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class article =
|
||||
trace :: "(title + subtitle + author+ abstract +
|
||||
|
|
@ -433,7 +433,7 @@ use fractions or even mathematical reals. This must be counterbalanced by syntac
|
|||
and semantic convenience. Choosing the mathematical reals, \<^eg>, would have the drawback that
|
||||
attribute evaluation could be substantially more complicated.\<close>
|
||||
|
||||
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
|
||||
figure*[fig_figures::figure,relative_width="85",file_src="''figures/Dogfood-figures.png''"]
|
||||
\<open> Ouroboros II: figures \<^dots> \<close>
|
||||
|
||||
text\<open> The document class \<^theory_text>\<open>figure\<close> --- supported by the \<^isadof> text command
|
||||
|
|
@ -462,7 +462,7 @@ where for organizational reasons the execution of an exam takes place in facilit
|
|||
where the author of the exam is not expected to be physically present.
|
||||
Furthermore, we assume a simple grade system (thus, some calculation is required). \<close>
|
||||
text*["onto_exam"::float,
|
||||
caption = "''The core of the ontology modeling math exams.''"]\<open>
|
||||
main_caption = "''The core of the ontology modeling math exams.''"]\<open>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class Author = ...
|
||||
datatype Subject = algebra | geometry | statistical
|
||||
|
|
@ -495,7 +495,7 @@ assume familiarity of the students with Isabelle (\<^theory_text>\<open>term\<cl
|
|||
parse-able and type-checkable entity), we basically model a derivation as a sequence of strings
|
||||
(see @{float (unchecked)"onto_questions"}).\<close>
|
||||
text*["onto_questions"::float,
|
||||
caption = "''An exam can contain different types of questions.''"]\<open>
|
||||
main_caption = "''An exam can contain different types of questions.''"]\<open>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class Answer_Formal_Step = Exam_item +
|
||||
justification :: string
|
||||
|
|
@ -530,7 +530,7 @@ question by a sample proof validated by Isabelle (see @{float (unchecked) "onto_
|
|||
In our scenario this sample proofs are completely \<^emph>\<open>intern\<close>, \<^ie>, not exposed to the
|
||||
students but just additional material for the internal review process of the exam.\<close>
|
||||
text*["onto_exam_monitor"::float,
|
||||
caption = "''Validating exams.''"]\<open>
|
||||
main_caption = "''Validating exams.''"]\<open>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class Validation =
|
||||
tests :: "term list" <="[]"
|
||||
|
|
@ -555,9 +555,9 @@ exam-sheets with multiple-choice and/or free-response elements
|
|||
help of the latter, it is possible that students write in a browser a formal mathematical
|
||||
derivation---as part of an algebra exercise, for example---which is submitted to the examiners
|
||||
electronically. \<close>
|
||||
figure*[fig_qcm::figure,spawn_columns=False,
|
||||
relative_width="90",src="''figures/InteractiveMathSheet''"]
|
||||
\<open> A Generated QCM Fragment \<^dots> \<close>
|
||||
figure*[fig_qcm::figure,
|
||||
relative_width="90",file_src="''figures/InteractiveMathSheet.png''"]
|
||||
\<open>A Generated QCM Fragment \<^dots> \<close>
|
||||
|
||||
subsection*[cenelec_onto::example]\<open> The Certification Scenario following CENELEC \<close>
|
||||
text\<open> Documents to be provided in formal certifications (such as CENELEC
|
||||
|
|
@ -583,7 +583,7 @@ text\<open> In the sequel, we present a simplified version of an ontological mod
|
|||
case-study~ @{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of requirement
|
||||
(see @{float (unchecked) "conceptual"}). \<close>
|
||||
text*["conceptual"::float,
|
||||
caption = "''Modeling requirements.''"]\<open>
|
||||
main_caption = "''Modeling requirements.''"]\<open>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class requirement = long_name :: "string option"
|
||||
|
||||
|
|
@ -641,18 +641,20 @@ Clicking on a document class identifier permits to hyperlink into the correspond
|
|||
class definition (\<^unchecked_label>\<open>fig:Dogfood-IV-jumpInDocCLass\<close>; hovering over an attribute-definition
|
||||
(which is qualified in order to disambiguate; \<^unchecked_label>\<open>fig:Dogfood-V-attribute\<close>).
|
||||
\<close>
|
||||
|
||||
side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''",
|
||||
caption="''Exploring a Reference of a Text-Element.''",relative_width="48",
|
||||
src="''figures/Dogfood-II-bgnd1''",anchor2="''fig-bgnd-text_section''",
|
||||
caption2="''Exploring the class of a text element.''",relative_width2="47",
|
||||
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Exploring text elements. \<close>
|
||||
|
||||
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
|
||||
caption="''Hyperlink to Class-Definition.''",relative_width="48",
|
||||
src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''",
|
||||
caption2="''Exploring an attribute.''",relative_width2="47",
|
||||
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Hyperlinks.\<close>
|
||||
text*["text-elements"::float,
|
||||
main_caption="\<open>Exploring text elements.\<close>"]
|
||||
\<open>
|
||||
@{fig_content (width=48, caption="Exploring a Reference of a Text-Element.") "figures/Dogfood-II-bgnd1.png"
|
||||
}\<^hfill>@{fig_content (width=47, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"}
|
||||
\<close>
|
||||
|
||||
text*["hyperlinks"::float,
|
||||
main_caption="\<open>Hyperlinks.\<close>"]
|
||||
\<open>
|
||||
@{fig_content (width=48, caption="Hyperlink to Class-Definition.") "figures/Dogfood-IV-jumpInDocCLass.png"
|
||||
}\<^hfill>@{fig_content (width=47, caption="Exploring an attribute.") "figures/Dogfood-III-bgnd-text_section.png"}
|
||||
\<close>
|
||||
|
||||
|
||||
(*<*)declare_reference*["figDogfoodVIlinkappl"::figure](*>*)
|
||||
|
|
@ -661,8 +663,9 @@ antiquotation \<^theory_text>\<open>@{example ...}\<close> refers to the corresp
|
|||
for inspection, clicking for jumping to the definition. If the link does not exist or has a
|
||||
non-compatible type, the text is not validated. \<close>
|
||||
|
||||
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
|
||||
figure*[figDogfoodVIlinkappl::figure,relative_width="80",file_src="''figures/Dogfood-V-attribute.png''"]
|
||||
\<open> Exploring an attribute (hyperlinked to the class). \<close>
|
||||
|
||||
subsection*[cenelec_pide::example]\<open> CENELEC \<close>
|
||||
(*<*)declare_reference*[figfig3::figure](*>*)
|
||||
text\<open> The corresponding view in @{figure (unchecked) \<open>figfig3\<close>} shows core part of a document,
|
||||
|
|
@ -670,7 +673,7 @@ coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows s
|
|||
@{cite "wenzel:isabelle-isar:2017"} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.\<close>
|
||||
|
||||
figure*[figfig3::figure,relative_width="80",src="''figures/antiquotations-PIDE''"]
|
||||
figure*[figfig3::figure,relative_width="80",file_src="''figures/antiquotations-PIDE.png''"]
|
||||
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||
|
||||
(*<*)declare_reference*[figfig5::figure] (*>*)
|
||||
|
|
@ -680,9 +683,9 @@ has the consequence that a certain calculation must be executed sufficiently fas
|
|||
device. This condition can not be established inside the formal theory but has to be
|
||||
checked by system integration tests.\<close>
|
||||
|
||||
figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"]
|
||||
figure*[figfig5::figure, relative_width="80", file_src="''figures/srac-definition.png''"]
|
||||
\<open> Defining a SRAC reference \<^dots> \<close>
|
||||
figure*[figfig7::figure, relative_width="80", src="''figures/srac-as-es-application''"]
|
||||
figure*[figfig7::figure, relative_width="80", file_src="''figures/srac-as-es-application.png''"]
|
||||
\<open> Using a SRAC as EC document reference. \<close>
|
||||
|
||||
text\<open> Now we reference in @{figure \<open>figfig7\<close>} this safety-related condition;
|
||||
|
|
|
|||
|
|
@ -22,9 +22,6 @@
|
|||
\usepackage{listings}
|
||||
\usepackage{lstisadof-manual}
|
||||
|
||||
\usepackage[caption]{subfig}
|
||||
\usepackage[size=footnotesize]{caption}
|
||||
|
||||
\providecommand{\isactrlemph}[1]{\emph{#1}}
|
||||
\usepackage[LNCS,
|
||||
orcidicon,
|
||||
|
|
|
|||
|
|
@ -126,7 +126,7 @@ text\<open>
|
|||
|
||||
subsection\<open>Capturing ``System Architecture.''\<close>
|
||||
|
||||
figure*["three-phase"::figure,relative_width="70",src="''figures/three-phase-odo''"]
|
||||
figure*["three-phase"::figure,relative_width="70",file_src="''figures/three-phase-odo.pdf''"]
|
||||
\<open>An odometer with three sensors \<open>C1\<close>, \<open>C2\<close>, and \<open>C3\<close>.\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -162,7 +162,7 @@ text\<open>
|
|||
of the measuring device, and the required format and precision of the measurements of the odometry
|
||||
function as represented (see @{figure (unchecked) "df-numerics-encshaft"}).\<close>
|
||||
|
||||
figure*["df-numerics-encshaft"::figure,relative_width="76",src="''figures/df-numerics-encshaft''"]
|
||||
figure*["df-numerics-encshaft"::figure,relative_width="76",file_src="''figures/df-numerics-encshaft.png''"]
|
||||
\<open>Real distance vs. discrete distance vs. shaft-encoder sequence\<close>
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ text\<open> \<^vs>\<open>-0.5cm\<close>
|
|||
maximum of formal content which makes this text re-checkable at each load and easier
|
||||
maintainable. \<close>
|
||||
|
||||
figure*[architecture::figure,relative_width="70",src="''figures/isabelle-architecture''"]\<open>
|
||||
figure*[architecture::figure,relative_width="70",file_src="''figures/isabelle-architecture.pdf''"]\<open>
|
||||
The system architecture of Isabelle (left-hand side) and the asynchronous communication
|
||||
between the Isabelle system and the IDE (right-hand side). \<close>
|
||||
|
||||
|
|
@ -148,7 +148,7 @@ text\<open> \<open>*\<open>This is a text.\<close>\<close>\<close>
|
|||
|
||||
text\<open>and displayed in the Isabelle/jEdit front-end at the sceen by:\<close>
|
||||
|
||||
figure*[fig2::figure, relative_width="60", placement="pl_h", src="''figures/text-element''"]
|
||||
figure*[fig2::figure, relative_width="60", file_src="''figures/text-element.pdf''"]
|
||||
\<open>A text-element as presented in Isabelle/jEdit.\<close>
|
||||
|
||||
text\<open>The text-commands, ML-commands (and in principle any other command) can be seen as
|
||||
|
|
@ -807,18 +807,13 @@ text\<open> They reflect the Pure logic depicted in a number of presentations s
|
|||
Notated as logical inference rules, these operations were presented as follows:
|
||||
\<close>
|
||||
|
||||
side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-kernel1''",
|
||||
caption="''Pure Kernel Inference Rules I ''",relative_width="48",
|
||||
src="''figures/pure-inferences-I''",anchor2="''fig-kernel2''",
|
||||
caption2="''Pure Kernel Inference Rules II''",relative_width2="47",
|
||||
src2="''figures/pure-inferences-II''"]\<open> \<close>
|
||||
text*["text-elements"::float,
|
||||
main_caption="\<open>Kernel Inference Rules.\<close>"]
|
||||
\<open>
|
||||
@{fig_content (width=48, caption="Pure Kernel Inference Rules I.") "figures/pure-inferences-I.pdf"
|
||||
}\<^hfill>@{fig_content (width=47, caption="Pure Kernel Inference Rules II.") "figures/pure-inferences-II.pdf"}
|
||||
\<close>
|
||||
|
||||
(*
|
||||
figure*[kir1::figure,relative_width="100",src="''figures/pure-inferences-I''"]
|
||||
\<open> Pure Kernel Inference Rules I.\<close>
|
||||
figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"]
|
||||
\<open> Pure Kernel Inference Rules II. \<close>
|
||||
*)
|
||||
|
||||
text\<open>Note that the transfer rule:
|
||||
\[
|
||||
|
|
@ -1440,7 +1435,7 @@ text\<open>The document model forsees a number of text files, which are organize
|
|||
secondary formats can be \<^verbatim>\<open>.sty\<close>,\<^verbatim>\<open>.tex\<close>, \<^verbatim>\<open>.png\<close>, \<^verbatim>\<open>.pdf\<close>, or other files processed
|
||||
by Isabelle and listed in a configuration processed by the build system.\<close>
|
||||
|
||||
figure*[fig3::figure, relative_width="100",src="''figures/document-model''"]
|
||||
figure*[fig3::figure, relative_width="100",file_src="''figures/document-model.pdf''"]
|
||||
\<open>A Theory-Graph in the Document Model\<close>
|
||||
|
||||
text\<open>A \<^verbatim>\<open>.thy\<close> file consists of a \<^emph>\<open>header\<close>, a \<^emph>\<open>context-definition\<close> and
|
||||
|
|
@ -1535,7 +1530,7 @@ text\<open> ... uses the antiquotation @{ML "@{here}"} to infer from the system
|
|||
of itself in the global document, converts it to markup (a string-representation of it) and sends
|
||||
it via the usual @{ML "writeln"} to the interface. \<close>
|
||||
|
||||
figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"]
|
||||
figure*[hyplinkout::figure,relative_width="40",file_src="''figures/markup-demo.png''"]
|
||||
\<open>Output with hyperlinked position.\<close>
|
||||
|
||||
text\<open>@{figure \<open>hyplinkout\<close>} shows the produced output where the little house-like symbol in the
|
||||
|
|
|
|||
|
|
@ -194,17 +194,17 @@ result communication times \ldots \<close>
|
|||
text\<open>Note that this \<^pdf>-output is the result of a specific setup for \<^typ>\<open>SRAC\<close>s.\<close>
|
||||
|
||||
subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
|
||||
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
|
||||
figure*[figfig3::figure,relative_width="95",file_src="''figures/antiquotations-PIDE.png''"]
|
||||
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
|
||||
conforming to the \<^verbatim>\<open>CENELEC_50128\<close> ontology. The first sample shows standard Isabelle antiquotations
|
||||
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.\<close>
|
||||
|
||||
figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
|
||||
figure*[figfig5::figure, relative_width="95", file_src="''figures/srac-definition.png''"]
|
||||
\<open> Defining a \<^typ>\<open>SRAC\<close> in the integrated source ... \<close>
|
||||
|
||||
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
|
||||
figure*[figfig7::figure, relative_width="95", file_src="''figures/srac-as-es-application.png''"]
|
||||
\<open> Using a \<^typ>\<open>SRAC\<close> as \<^typ>\<open>EC\<close> document element. \<close>
|
||||
text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of a
|
||||
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
|
||||
|
|
|
|||
|
|
@ -207,7 +207,8 @@ map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
|
|||
|
||||
let val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Conceptual.D",
|
||||
"Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M",
|
||||
"Isa_COL.float", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.section",
|
||||
"Isa_COL.float", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.listing",
|
||||
"Isa_COL.section",
|
||||
"Isa_COL.paragraph", "Isa_COL.subsection", "Isa_COL.figure_group",
|
||||
"Isa_COL.text_element", "Isa_COL.subsubsection",
|
||||
"Isa_COL.side_by_side_figure"]
|
||||
|
|
|
|||
|
|
@ -38,8 +38,6 @@
|
|||
} % more detailed digital TOC (aka bookmarks)
|
||||
\sloppy
|
||||
\allowdisplaybreaks[4]
|
||||
\usepackage[caption]{subfig}
|
||||
\usepackage[size=footnotesize]{caption}
|
||||
\let\DOFauthor\relax
|
||||
\begin{document}
|
||||
\selectlanguage{USenglish}%
|
||||
|
|
@ -50,8 +48,6 @@
|
|||
\renewcommand{\subsectionautorefname}{Sect.}
|
||||
\renewcommand{\sectionautorefname}{Sect.}
|
||||
\renewcommand{\figureautorefname}{Fig.}
|
||||
\newcommand{\subtableautorefname}{\tableautorefname}
|
||||
\newcommand{\subfigureautorefname}{\figureautorefname}
|
||||
\newcommand{\lstnumberautorefname}{Line}
|
||||
|
||||
\maketitle
|
||||
|
|
|
|||
|
|
@ -40,8 +40,6 @@
|
|||
} % more detailed digital TOC (aka bookmarks)
|
||||
\sloppy
|
||||
\allowdisplaybreaks[4]
|
||||
\usepackage[caption]{subfig}
|
||||
\usepackage[size=footnotesize]{caption}
|
||||
|
||||
\begin{document}
|
||||
\selectlanguage{USenglish}%
|
||||
|
|
@ -52,8 +50,6 @@
|
|||
\renewcommand{\subsectionautorefname}{Sect.}
|
||||
\renewcommand{\sectionautorefname}{Sect.}
|
||||
\renewcommand{\figureautorefname}{Fig.}
|
||||
\newcommand{\subtableautorefname}{\tableautorefname}
|
||||
\newcommand{\subfigureautorefname}{\figureautorefname}
|
||||
\newcommand{\lstnumberautorefname}{Line}
|
||||
|
||||
\maketitle
|
||||
|
|
|
|||
|
|
@ -4,10 +4,10 @@ theory Reification_Test
|
|||
begin
|
||||
|
||||
ML\<open>
|
||||
val ty1 = ISA_core.reify_typ @{typ "int"}
|
||||
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
|
||||
val ty3 = ISA_core.reify_typ @{typ "prop"}
|
||||
val ty4 = ISA_core.reify_typ @{typ "'a list"}
|
||||
val ty1 = Meta_ISA_core.reify_typ @{typ "int"}
|
||||
val ty2 = Meta_ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
|
||||
val ty3 = Meta_ISA_core.reify_typ @{typ "prop"}
|
||||
val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"}
|
||||
\<close>
|
||||
|
||||
term*\<open>@{typ \<open>int\<close>}\<close>
|
||||
|
|
@ -19,9 +19,9 @@ term*\<open>@{typ \<open>'a list\<close>}\<close>
|
|||
value*\<open>@{typ \<open>'a list\<close>}\<close>
|
||||
|
||||
ML\<open>
|
||||
val t1 = ISA_core.reify_term @{term "1::int"}
|
||||
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
|
||||
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
|
||||
val t1 = Meta_ISA_core.reify_term @{term "1::int"}
|
||||
val t2 = Meta_ISA_core.reify_term @{term "\<lambda>x. x = 1"}
|
||||
val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"}
|
||||
\<close>
|
||||
term*\<open>@{term \<open>1::int\<close>}\<close>
|
||||
value*\<open>@{term \<open>1::int\<close>}\<close>
|
||||
|
|
@ -45,7 +45,7 @@ value*\<open>@{thms-of \<open>HOL.refl\<close>}\<close>
|
|||
ML\<open>
|
||||
val t_schematic = TVar(("'a",0), [])
|
||||
val t = @{term "Tv (Var (STR '''a'', 0)) {}"}
|
||||
val rt_schematic = ISA_core.reify_typ t_schematic
|
||||
val rt_schematic = Meta_ISA_core.reify_typ t_schematic
|
||||
val true = rt_schematic = t
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -15,6 +15,5 @@ term "@{term \<open>\<forall>x. P x \<longrightarrow> Q\<close>}"
|
|||
term "@{thm \<open>refl\<close>}"
|
||||
term "@{docitem \<open>doc_ref\<close>}"
|
||||
ML\<open> @{term "@{docitem \<open>doc_ref\<close>}"}\<close>
|
||||
(**)
|
||||
|
||||
end
|
||||
|
|
@ -32,89 +32,9 @@ consts Isabelle_DOF_trace_attribute :: "string \<Rightarrow> (string * string) l
|
|||
subsection\<open> Semantics \<close>
|
||||
|
||||
ML\<open>
|
||||
structure ISA_core =
|
||||
structure Meta_ISA_core =
|
||||
struct
|
||||
|
||||
fun check_path check_file ctxt dir (name, pos) =
|
||||
let
|
||||
val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be
|
||||
"lifted" to
|
||||
type source *)
|
||||
|
||||
val path = Path.append dir (Path.explode name) handle ERROR msg => ISA_core.err msg pos;
|
||||
val _ = Path.expand path handle ERROR msg => ISA_core.err msg pos;
|
||||
val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
|
||||
val _ =
|
||||
(case check_file of
|
||||
NONE => path
|
||||
| SOME check => (check path handle ERROR msg => ISA_core.err msg pos));
|
||||
in path end;
|
||||
|
||||
|
||||
fun ML_isa_antiq check_file thy (name, _, pos) =
|
||||
let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos);
|
||||
in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
|
||||
|
||||
|
||||
fun ML_isa_check_generic check thy (term, pos) =
|
||||
let val name = (HOLogic.dest_string term
|
||||
handle TERM(_,[t]) => error ("wrong term format: must be string constant: "
|
||||
^ Syntax.string_of_term_global thy t ))
|
||||
val _ = check thy (name,pos)
|
||||
in SOME term end;
|
||||
|
||||
fun check_identity _ (term, _, _) _ = SOME term
|
||||
|
||||
fun ML_isa_check_typ thy (term, _, pos) _ =
|
||||
let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
|
||||
in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
|
||||
|
||||
fun ML_isa_check_term thy (term, _, pos) _ =
|
||||
let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
|
||||
in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
|
||||
|
||||
fun ML_isa_check_thm thy (term, _, pos) _ =
|
||||
(* this works for long-names only *)
|
||||
let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of
|
||||
NONE => ISA_core.err ("No Theorem:" ^name) pos
|
||||
| SOME X => X
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
|
||||
|
||||
fun ML_isa_check_file thy (term, _, pos) _ =
|
||||
let fun check thy (name, pos) = check_path (SOME File.check_file)
|
||||
(Proof_Context.init_global thy)
|
||||
(Path.current)
|
||||
(name, pos);
|
||||
in ML_isa_check_generic check thy (term, pos) end;
|
||||
|
||||
fun ML_isa_id thy (term,pos) = SOME term
|
||||
|
||||
|
||||
fun ML_isa_check_docitem thy (term, req_ty, pos) _ =
|
||||
let fun check thy (name, _) s =
|
||||
let val DOF_core.Instance {cid,...} =
|
||||
DOF_core.get_instance_global name thy
|
||||
val ns = DOF_core.get_instances (Proof_Context.init_global thy)
|
||||
|> Name_Space.space_of_table
|
||||
val {pos=pos', ...} = Name_Space.the_entry ns name
|
||||
val ctxt = (Proof_Context.init_global thy)
|
||||
val req_class = case req_ty of
|
||||
\<^Type>\<open>fun _ T\<close> => DOF_core.typ_to_cid T
|
||||
| _ => error("can not infer type for: "^ name)
|
||||
in if cid <> DOF_core.default_cid
|
||||
andalso not(DOF_core.is_subclass ctxt cid req_class)
|
||||
then error("reference ontologically inconsistent: "
|
||||
^cid^" vs. "^req_class^ Position.here pos')
|
||||
else ()
|
||||
end
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
|
||||
|
||||
fun ML_isa_check_trace_attribute thy (term, _, pos) s =
|
||||
let
|
||||
val oid = (HOLogic.dest_string term
|
||||
|
|
@ -123,11 +43,6 @@ fun ML_isa_check_trace_attribute thy (term, _, pos) s =
|
|||
val _ = DOF_core.get_instance_global oid thy
|
||||
in SOME term end
|
||||
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
|
||||
case term_option of
|
||||
NONE => error("Wrong term option. You must use a defined term")
|
||||
| SOME term => Const (isa_name, ty) $ term
|
||||
|
||||
fun reify_typ (Type (s, typ_list)) =
|
||||
\<^Const>\<open>Ty\<close> $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\<open>typ\<close> (map reify_typ typ_list)
|
||||
| reify_typ (TFree (name, sort)) =
|
||||
|
|
@ -273,16 +188,16 @@ end; (* struct *)
|
|||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val ty1 = ISA_core.reify_typ @{typ "int"}
|
||||
val ty2 = ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
|
||||
val ty3 = ISA_core.reify_typ @{typ "prop"}
|
||||
val ty4 = ISA_core.reify_typ @{typ "'a list"}
|
||||
val ty1 = Meta_ISA_core.reify_typ @{typ "int"}
|
||||
val ty2 = Meta_ISA_core.reify_typ @{typ "int \<Rightarrow> bool"}
|
||||
val ty3 = Meta_ISA_core.reify_typ @{typ "prop"}
|
||||
val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"}
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val t1 = ISA_core.reify_term @{term "1::int"}
|
||||
val t2 = ISA_core.reify_term @{term "\<lambda>x. x = 1"}
|
||||
val t3 = ISA_core.reify_term @{term "[2, 3::int]"}
|
||||
val t1 = Meta_ISA_core.reify_term @{term "1::int"}
|
||||
val t2 = Meta_ISA_core.reify_term @{term "\<lambda>x. x = 1"}
|
||||
val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"}
|
||||
\<close>
|
||||
|
||||
subsection\<open> Isar - Setup\<close>
|
||||
|
|
@ -290,8 +205,8 @@ subsection\<open> Isar - Setup\<close>
|
|||
They must be declared in the same theory file as the one of the declaration
|
||||
of Isabelle_DOF term anti-quotations !!! *)
|
||||
setup\<open>
|
||||
[(\<^type_name>\<open>thm\<close>, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thm)
|
||||
, (\<^type_name>\<open>thms_of\<close>, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thms_of)
|
||||
[(\<^type_name>\<open>thm\<close>, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thm)
|
||||
, (\<^type_name>\<open>thms_of\<close>, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thms_of)
|
||||
, (\<^type_name>\<open>file\<close>, ISA_core.ML_isa_check_file, ISA_core.ML_isa_elaborate_generic)]
|
||||
|> fold (fn (n, check, elaborate) => fn thy =>
|
||||
let val ns = Sign.tsig_of thy |> Type.type_space
|
||||
|
|
@ -304,8 +219,8 @@ let val ns = Sign.tsig_of thy |> Type.type_space
|
|||
in DOF_core.add_isa_transformer binding ((check, elaborate) |> DOF_core.make_isa_transformer) thy
|
||||
end)
|
||||
#>
|
||||
([(\<^const_name>\<open>Isabelle_DOF_typ\<close>, ISA_core.ML_isa_check_typ, ISA_core.ML_isa_elaborate_typ)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_term\<close>, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_term)
|
||||
([(\<^const_name>\<open>Isabelle_DOF_typ\<close>, ISA_core.ML_isa_check_typ, Meta_ISA_core.ML_isa_elaborate_typ)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_term\<close>, ISA_core.ML_isa_check_term, Meta_ISA_core.ML_isa_elaborate_term)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_docitem\<close>,
|
||||
ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>,
|
||||
|
|
|
|||
|
|
@ -182,29 +182,29 @@ open_monitor*[figs1::figure_group,
|
|||
caption="''Sample ''"]
|
||||
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
|
||||
text*[testFreeA::A]\<open>\<close>
|
||||
figure*[fig_A::figure, spawn_columns=False,
|
||||
figure*[fig_A::figure,
|
||||
relative_width="90",
|
||||
src="''figures/A.png''"]
|
||||
file_src="''figures/A.png''"]
|
||||
\<open> The A train \ldots \<close>
|
||||
|
||||
figure*[fig_B::figure,
|
||||
spawn_columns=False,relative_width="90",
|
||||
src="''figures/B.png''"]
|
||||
relative_width="90",
|
||||
file_src="''figures/B.png''"]
|
||||
\<open> The B train \ldots \<close>
|
||||
open_monitor*[figs2::figure_group,
|
||||
caption="''Sample ''"]
|
||||
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
|
||||
figure*[fig_C::figure, spawn_columns=False,
|
||||
figure*[fig_C::figure,
|
||||
relative_width="90",
|
||||
src="''figures/A.png''"]
|
||||
file_src="''figures/A.png''"]
|
||||
\<open> The C train \ldots \<close>
|
||||
open_monitor*[figs3::figure_group,
|
||||
caption="''Sample ''"]
|
||||
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
|
||||
|
||||
figure*[fig_D::figure,
|
||||
spawn_columns=False,relative_width="90",
|
||||
src="''figures/B.png''"]
|
||||
relative_width="90",
|
||||
file_src="''figures/B.png''"]
|
||||
\<open> The D train \ldots \<close>
|
||||
close_monitor*[figs3]
|
||||
|
||||
|
|
@ -216,8 +216,8 @@ text*[testRejected1::figure_group, caption="''document/figures/A.png''"]
|
|||
\<open> The A train \ldots \<close>
|
||||
|
||||
figure*[fig_E::figure,
|
||||
spawn_columns=False,relative_width="90",
|
||||
src="''figures/B.png''"]
|
||||
relative_width="90",
|
||||
file_src="''figures/B.png''"]
|
||||
\<open> The E train \ldots \<close>
|
||||
close_monitor*[figs4]
|
||||
close_monitor*[figs2]
|
||||
|
|
|
|||
|
|
@ -28,58 +28,32 @@ text*[S5'::"paragraph"]\<open>Paragraph\<close>
|
|||
|
||||
section\<open>General Figure COL Elements\<close>
|
||||
|
||||
figure*[fig1_test::figure,spawn_columns=False,relative_width="95",src="''figures/A''"]
|
||||
figure*[fig1_test,relative_width="95",file_src="''figures/A.png''"]
|
||||
\<open> This is the label text \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>
|
||||
|
||||
text*[fig2_test::figure, spawn_columns=False, relative_width="95",src="''figures/A''"
|
||||
(*<*)
|
||||
text*[fig2_test::figure, relative_width="95",file_src="''figures/A.png''"
|
||||
]\<open> This is the label text\<close>
|
||||
|
||||
(*>*)
|
||||
text\<open>check @{figure fig1_test} cmp to @{figure fig2_test}\<close>
|
||||
|
||||
side_by_side_figure*["sbsfig1"::side_by_side_figure,
|
||||
anchor="''Asub1''",
|
||||
caption="''First caption.''",
|
||||
relative_width="48",
|
||||
src="''figures/A''",
|
||||
anchor2="''Asub2''",
|
||||
caption2="''Second caption.''",
|
||||
relative_width2="47",
|
||||
src2="''figures/B''"]\<open> Exploring text elements. \<close>
|
||||
|
||||
|
||||
text*["sbsfig2"::side_by_side_figure,
|
||||
anchor="''fig:Asub1''",
|
||||
caption="''First caption.''",
|
||||
relative_width="48",
|
||||
src="''figures/A''",
|
||||
anchor2="''fig:Asub2''",
|
||||
caption2="''Second caption.''",
|
||||
relative_width2="47",
|
||||
src2="''figures/B''"]\<open>The global caption\<close>
|
||||
|
||||
text\<open>check @{side_by_side_figure sbsfig1} cmp to @{side_by_side_figure sbsfig2}
|
||||
\autoref{Asub1} vs. \autoref{Asub2}
|
||||
\autoref{fig:Asub1} vs. \autoref{fig:Asub2}
|
||||
\<close>
|
||||
|
||||
(* And a side-chick ... *)
|
||||
|
||||
text*[inlinefig::float,
|
||||
caption="\<open>The Caption.\<close>"]
|
||||
\<open>@{theory_text [display, margin = 5] \<open>lemma A :: "a \<longrightarrow> b"\<close>}\<close>
|
||||
main_caption="\<open>The Caption.\<close>"]
|
||||
\<open>@{theory_text [display, margin = 5] \<open>lemma A :: "a \<longrightarrow> b"\<close>}\<close>
|
||||
|
||||
text*[fffff::float]\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>)
|
||||
\<open>figures/A.png\<close>}\<close>
|
||||
|
||||
(*<*)
|
||||
text*[inlinegraph::float,
|
||||
caption="\<open>Another \<sigma>\<^sub>i+2 Caption.\<close>"]
|
||||
\<open>@{fig_content [display] (scale = 80, width=80, caption=\<open>This is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
|
||||
\<open>figures/A.png\<close>}\<close>
|
||||
(*>*)
|
||||
text*[dupl_graphics::float,
|
||||
main_caption="\<open>The Caption.\<close>"]
|
||||
\<open>
|
||||
@{fig_content (width=40, height=35, caption="This is a left test") "figures/A.png"
|
||||
}\<^hfill>@{fig_content (width=40, height=35, caption="This is a right \<^term>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/B.png"}
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
(*<*)
|
||||
end
|
||||
(*>*)
|
||||
|
||||
|
|
|
|||
|
|
@ -131,7 +131,7 @@ text\<open>Now assume the following ontology:\<close>
|
|||
doc_class title =
|
||||
short_title :: "string option" <= "None"
|
||||
|
||||
doc_class Author =
|
||||
doc_class author =
|
||||
email :: "string" <= "''''"
|
||||
|
||||
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
||||
|
|
@ -141,18 +141,18 @@ doc_class abstract =
|
|||
safety_level :: "classification" <= "SIL3"
|
||||
|
||||
doc_class text_section =
|
||||
authored_by :: "Author set" <= "{}"
|
||||
authored_by :: "author set" <= "{}"
|
||||
level :: "int option" <= "None"
|
||||
|
||||
type_synonym notion = string
|
||||
|
||||
doc_class Introduction = text_section +
|
||||
authored_by :: "Author set" <= "UNIV"
|
||||
doc_class introduction = text_section +
|
||||
authored_by :: "author set" <= "UNIV"
|
||||
uses :: "notion set"
|
||||
invariant author_finite :: "finite (authored_by \<sigma>)"
|
||||
and force_level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 1"
|
||||
|
||||
doc_class claim = Introduction +
|
||||
doc_class claim = introduction +
|
||||
based_on :: "notion list"
|
||||
|
||||
doc_class technical = text_section +
|
||||
|
|
@ -181,7 +181,10 @@ text\<open>Next we define some instances (docitems): \<close>
|
|||
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
||||
text*[church::Author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
|
||||
text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
|
||||
|
||||
text\<open>We can also reference instances of classes defined in parent theories:\<close>
|
||||
text*[church'::scholarly_paper.author, email="\<open>church'@lambda.org\<close>"]\<open>\<close>
|
||||
|
||||
text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
|
||||
text*[resultArgument::result, evidence = "argument"]\<open>\<close>
|
||||
|
|
@ -193,29 +196,41 @@ text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^the
|
|||
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
||||
text*[curry::Author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
|
||||
text*[introduction2::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
|
||||
|
||||
text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
(* When not commented, should violated the invariant:
|
||||
update_instance*[introduction2::Introduction
|
||||
, authored_by := "{@{Author \<open>church\<close>}}"
|
||||
, level := "Some 1"]
|
||||
*)
|
||||
text\<open>Use of the instance @{docitem_name "church'"}
|
||||
to instantiate a \<^doc_class>\<open>scholarly_paper.introduction\<close> class:\<close>
|
||||
text*[introduction2'::scholarly_paper.introduction,
|
||||
main_author = "Some @{scholarly-paper.author \<open>church'\<close>}", level = "Some 2"]\<open>\<close>
|
||||
|
||||
value*\<open>@{scholarly-paper.author \<open>church'\<close>}\<close>
|
||||
value*\<open>@{author \<open>church\<close>}\<close>
|
||||
value*\<open>@{Concept-High-Level-Invariants.author \<open>church\<close>}\<close>
|
||||
|
||||
text*[introduction3::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[introduction4::Introduction, authored_by = "{@{Author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
|
||||
value*\<open>@{scholarly-paper.author-instances}\<close>
|
||||
value*\<open>@{author-instances}\<close>
|
||||
value*\<open>@{Concept-High-Level-Invariants.author-instances}\<close>
|
||||
|
||||
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
|
||||
|
||||
text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
|
||||
|
||||
text\<open>Then we can evaluate expressions with instances:\<close>
|
||||
|
||||
term*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction4\<close>}\<close>
|
||||
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction4\<close>}\<close>
|
||||
|
||||
value*\<open>@{Introduction \<open>introduction2\<close>}\<close>
|
||||
value*\<open>@{introduction \<open>introduction2\<close>}\<close>
|
||||
|
||||
value*\<open>{@{Author \<open>curry\<close>}} = {@{Author \<open>church\<close>}}\<close>
|
||||
value*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>
|
||||
|
||||
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
value*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
|
|
|
|||
|
|
@ -22,9 +22,12 @@ begin
|
|||
section\<open>Test Purpose.\<close>
|
||||
text\<open> Creation of document parts that are controlled by (nested, locally defined) monitors. \<close>
|
||||
|
||||
doc_class test_monitor_B =
|
||||
tmB :: int
|
||||
|
||||
doc_class monitor_M =
|
||||
tmM :: int
|
||||
rejects "test_monitor_B"
|
||||
rejects "Concept_MonitorTest1.test_monitor_B"
|
||||
accepts "test_monitor_E ~~ test_monitor_C"
|
||||
|
||||
doc_class test_monitor_head =
|
||||
|
|
|
|||
|
|
@ -200,10 +200,10 @@ Consequently, it has the same limitations as \<^emph>\<open>value*\<close>.
|
|||
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\<close>
|
||||
we can check logical statements:\<close>
|
||||
|
||||
term*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{Introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Introduction \<open>introduction4\<close>})\<close>
|
||||
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{introduction \<open>introduction2\<close>}
|
||||
= authored_by @{introduction \<open>introduction4\<close>})\<close>
|
||||
|
||||
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
|
||||
(* Error:
|
||||
|
|
|
|||
|
|
@ -418,16 +418,16 @@ Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
|
|||
|
||||
(*<*)
|
||||
|
||||
text-latex\<open>
|
||||
@{fig_content (width=40, scale=35, caption="This is a right test") "figures/A.png"}
|
||||
@{fig_content (width=40, scale=35, caption="This is a left \<^term>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/A.png"}
|
||||
Figure*[figxxx::float,main_caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
|
||||
\<open> @{fig_content (width=40, height=35, caption="This is a right test") "figures/A.png"}
|
||||
@{fig_content (width=40, height=35, caption="This is a left \<^term>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/A.png"}
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
(* proposed syntax for sub-figure labels : text\<open> @{figure "ffff(2)"}\<close> *)
|
||||
|
||||
Figure*[figxxx::float,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
|
||||
Figure*[figxxxx::float,main_caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
|
||||
\<open>@{boxed_theory_text [display]
|
||||
\<open>lemma inv_c2_preserved : "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)"
|
||||
unfolding c1_inv_def c2_inv_def
|
||||
|
|
|
|||
|
|
@ -408,7 +408,7 @@ Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
|
|||
*)
|
||||
|
||||
|
||||
Figure*[ffff::float, caption="\<open>this is another 2 side-by-side\<close>"]
|
||||
Figure*[ffff::float, main_caption="\<open>this is another 2 side-by-side\<close>"]
|
||||
\<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\<close>
|
||||
\<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\<close>
|
||||
|
||||
|
|
@ -416,7 +416,7 @@ Figure*[ffff::float, caption="\<open>this is another 2 side-by-side\<close>"]
|
|||
text\<open> @{figure "ffff(2)"}\<close>
|
||||
*)
|
||||
|
||||
Figure*[figxxx::float,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
|
||||
Figure*[figxxx::float,main_caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
|
||||
\<open>@{boxed_theory_text [display]
|
||||
\<open>lemma inv_c2_preserved : "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)"
|
||||
unfolding c1_inv_def c2_inv_def
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
|
|||
"Attributes"
|
||||
"AssnsLemmaThmEtc"
|
||||
"Ontology_Matching_Example"
|
||||
(* "Cenelec_Test" *)
|
||||
"Cenelec_Test"
|
||||
"OutOfOrderPresntn"
|
||||
"COL_Test"
|
||||
document_files
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -36,7 +36,7 @@
|
|||
\sloppy
|
||||
\allowdisplaybreaks[4]
|
||||
|
||||
\usepackage[caption]{subfig}
|
||||
\usepackage{subcaption}
|
||||
\usepackage[size=footnotesize]{caption}
|
||||
|
||||
\renewcommand{\topfraction}{0.9} % max fraction of floats at top
|
||||
|
|
@ -59,8 +59,6 @@
|
|||
\renewcommand{\subsectionautorefname}{Sect.}
|
||||
\renewcommand{\sectionautorefname}{Sect.}
|
||||
\renewcommand{\figureautorefname}{Fig.}
|
||||
\newcommand{\subtableautorefname}{\tableautorefname}
|
||||
\newcommand{\subfigureautorefname}{\figureautorefname}
|
||||
\newcommand{\lstnumberautorefname}{Line}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@
|
|||
|
||||
\usepackage{textcomp}
|
||||
\bibliographystyle{abbrvnat}
|
||||
\RequirePackage[caption]{subfig}
|
||||
\RequirePackage{subcaption}
|
||||
|
||||
|
||||
\usepackage[numbers, sort&compress, sectionbib]{natbib}
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@
|
|||
\addtokomafont{paragraph}{\color{DOFsectioncolor}}
|
||||
\addtokomafont{subparagraph}{\color{DOFsectioncolor}}
|
||||
|
||||
\RequirePackage[caption]{subfig}
|
||||
\RequirePackage{subcaption}
|
||||
\renewcommand{\isastyletext}{\normalsize\normalfont\sffamily}
|
||||
\renewcommand{\isastyletxt}{\normalfont\sffamily}
|
||||
\renewcommand{\isastylecmt}{\normalfont\sffamily}
|
||||
|
|
@ -68,8 +68,6 @@
|
|||
\renewcommand{\sectionautorefname}{Section}
|
||||
\renewcommand{\subsectionautorefname}{Section}
|
||||
\renewcommand{\subsubsectionautorefname}{Section}
|
||||
\newcommand{\subtableautorefname}{\tableautorefname}
|
||||
\newcommand{\subfigureautorefname}{\figureautorefname}
|
||||
\begin{frontmatter}
|
||||
\maketitle
|
||||
\tableofcontents
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@
|
|||
|
||||
\usepackage{textcomp}
|
||||
\bibliographystyle{abbrvnat}
|
||||
\RequirePackage[caption]{subfig}
|
||||
\RequirePackage{subcaption}
|
||||
|
||||
|
||||
\usepackage[numbers, sort&compress, sectionbib]{natbib}
|
||||
|
|
@ -48,8 +48,6 @@
|
|||
\renewcommand{\sectionautorefname}{Section}
|
||||
\renewcommand{\subsectionautorefname}{Section}
|
||||
\renewcommand{\subsubsectionautorefname}{Section}
|
||||
\newcommand{\subtableautorefname}{\tableautorefname}
|
||||
\newcommand{\subfigureautorefname}{\figureautorefname}
|
||||
\maketitle
|
||||
\tableofcontents
|
||||
\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
|
||||
|
|
|
|||
|
|
@ -18,100 +18,21 @@
|
|||
|
||||
\RequirePackage{DOF-core}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: figure*
|
||||
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
|
||||
\newisadof{IsaUNDERSCORECOLDOTfigure}%
|
||||
[label=,type=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
|
||||
][1]{%
|
||||
\begin{figure}[]
|
||||
\centering
|
||||
\ifcommandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}
|
||||
{%
|
||||
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}}
|
||||
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
|
||||
\FPdiv\scale{\dof@width}{100}%
|
||||
\includegraphics[width=\scale\textwidth]{\dof@src}%
|
||||
}{%
|
||||
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
|
||||
\includegraphics[]{\dof@src}%
|
||||
}
|
||||
\caption{#1}\label{\commandkey{label}}%
|
||||
\end{figure}
|
||||
}
|
||||
% end: figure*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: float*
|
||||
\NewEnviron{isamarkupfloat*}[1][]{\isaDof[env={float},#1]{\BODY}}
|
||||
\newisadof{IsaUNDERSCORECOLDOTfloat}%
|
||||
[label=,type=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
|
||||
,IsaUNDERSCORECOLDOTfloatDOTcaption=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
|
||||
,IsaUNDERSCORECOLDOTfloatDOTplacement=%
|
||||
,IsaUNDERSCORECOLDOTfloatDOTfloatUNDERSCOREkind=%
|
||||
,IsaUNDERSCORECOLDOTfloatDOTmainUNDERSCOREcaption=%
|
||||
,IsaUNDERSCORECOLDOTfloatDOTspawnUNDERSCOREcolumns=enum False True%
|
||||
][1]{%
|
||||
\begin{figure}[]
|
||||
\begin{figure}
|
||||
#1
|
||||
\caption{\commandkey{IsaUNDERSCORECOLDOTfloatDOTcaption}}
|
||||
\caption{\commandkey{IsaUNDERSCORECOLDOTfloatDOTmainUNDERSCOREcaption}}
|
||||
\label{\commandkey{label}}%
|
||||
\end{figure}
|
||||
}
|
||||
% end: float*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: side_by_side_figure*
|
||||
\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={sideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure},#1]{\BODY}}
|
||||
\newisadof{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure}%
|
||||
[label=,type=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
|
||||
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchor=%
|
||||
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaption=%
|
||||
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO=%
|
||||
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO=%
|
||||
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchorTWO=%
|
||||
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaptionTWO=%
|
||||
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTplacement=%
|
||||
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
|
||||
][1]{%
|
||||
\begin{figure}[]
|
||||
\subfloat[\label{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchor}}\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaption}]%
|
||||
{\ifcommandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}%
|
||||
{%
|
||||
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}}
|
||||
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
|
||||
\FPdiv\scale{\dof@width}{100}%
|
||||
\includegraphics[width=\scale\textwidth]{\dof@src}%
|
||||
}{%
|
||||
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
|
||||
\includegraphics[]{\dof@src}%
|
||||
}%
|
||||
}%
|
||||
\hfill%
|
||||
\subfloat[\label{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchorTWO}}\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaptionTWO}]%
|
||||
{\ifcommandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO}%
|
||||
{%
|
||||
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO}}
|
||||
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO}}
|
||||
\FPdiv\scale{\dof@width}{100}%
|
||||
\includegraphics[width=\scale\textwidth]{\dof@src}%
|
||||
}{%
|
||||
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO}}
|
||||
\includegraphics[]{\dof@src}%
|
||||
}%
|
||||
}%
|
||||
\caption{#1}\label{\commandkey{label}}%
|
||||
\end{figure}
|
||||
}
|
||||
% end: side_by_side_figure*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
|
|
|||
|
|
@ -167,7 +167,6 @@
|
|||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\title{No Title Given}
|
||||
\author{No Author Given}
|
||||
\input{ontologies}
|
||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
||||
|
||||
|
|
|
|||
|
|
@ -141,33 +141,41 @@ val _ = heading_command \<^command_keyword>\<open>subsection*\<close> "subsectio
|
|||
val _ = heading_command \<^command_keyword>\<open>subsubsection*\<close> "subsubsection heading" (SOME (SOME 3));
|
||||
val _ = heading_command \<^command_keyword>\<open>paragraph*\<close> "paragraph" (SOME (SOME 4));
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
||||
section\<open> Library of Standard Text Ontology \<close>
|
||||
|
||||
datatype placement = pl_h | (*here*)
|
||||
pl_t | (*top*)
|
||||
pl_b | (*bottom*)
|
||||
pl_ht | (*here -> top*)
|
||||
pl_hb (*here -> bottom*)
|
||||
datatype placement = here | top | bottom
|
||||
|
||||
ML\<open> "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context>
|
||||
|> Name_Space.space_of_table)\<close>
|
||||
|
||||
print_doc_classes
|
||||
datatype float_kind = listing | table | graphics
|
||||
|
||||
doc_class figure =
|
||||
relative_width :: "int" (* percent of textwidth *)
|
||||
src :: "string"
|
||||
placement :: placement
|
||||
spawn_columns :: bool <= True
|
||||
doc_class float =
|
||||
placement :: "placement list"
|
||||
kind :: float_kind
|
||||
spawn_columns :: bool <= False
|
||||
main_caption :: string <= "''''"
|
||||
|
||||
doc_class float = figure +
|
||||
caption :: string
|
||||
doc_class figure = float +
|
||||
kind :: float_kind <= graphics
|
||||
file_src :: string
|
||||
relative_width :: int
|
||||
relative_height :: int
|
||||
invariant fig_kind :: "kind \<sigma> = graphics"
|
||||
|
||||
|
||||
doc_class listing = float +
|
||||
kind :: float_kind
|
||||
invariant fig_kind' :: "kind \<sigma> = float_kind.listing"
|
||||
|
||||
|
||||
(* obsolete *)
|
||||
doc_class side_by_side_figure = figure +
|
||||
anchor :: "string"
|
||||
caption :: "string"
|
||||
|
|
@ -225,7 +233,7 @@ end\<close>
|
|||
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>vs\<close> "\\vspace{" "}" (check_latex_measure) \<close>
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>hs\<close> "\\hspace{" "}" (check_latex_measure) \<close>
|
||||
|
||||
define_shortcut* hfill \<rightleftharpoons> \<open>\hfill\<close>
|
||||
(*<*)
|
||||
|
||||
text\<open>Tests: \<^vs>\<open>-0.14cm\<close>\<close>
|
||||
|
|
@ -238,17 +246,6 @@ define_macro* hs2 \<rightleftharpoons> \<open>\hspace{\<close> _ \<open>}\<close
|
|||
|
||||
subsection\<open>Figures\<close>
|
||||
|
||||
ML\<open>open Args\<close>
|
||||
|
||||
ML\<open>
|
||||
(* *********************************************************************** *)
|
||||
(* Ontological Macro Command Support *)
|
||||
(* *********************************************************************** *)
|
||||
|
||||
val _ = Onto_Macros.heading_command \<^command_keyword>\<open>figure*\<close> "figure" NONE;
|
||||
val _ = Onto_Macros.heading_command \<^command_keyword>\<open>side_by_side_figure*\<close> "multiple figures" NONE;
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
|
||||
ML\<open>
|
||||
|
|
@ -266,29 +263,28 @@ text\<open>The intermediate development goal is to separate the ontological, top
|
|||
\<^emph>\<open>import\<close> of a figure. The hope is that this opens the way for more orthogonality and
|
||||
abstraction from the LaTeX engine.
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
ML\<open>
|
||||
|
||||
type fig_content = {relative_width : int, (* percent of textwidth, default 100 *)
|
||||
scale : int, (* percent, default 100 *)
|
||||
relative_height : int, (* percent, default 100 *)
|
||||
caption : Input.source (* default empty *)}
|
||||
|
||||
val mt_fig_content = {relative_width = 100,
|
||||
scale = 100,
|
||||
relative_height = 100,
|
||||
caption = Input.empty }: fig_content
|
||||
|
||||
fun upd_relative_width key {relative_width,scale,caption } : fig_content =
|
||||
{relative_width = key,scale = scale,caption = caption}: fig_content
|
||||
fun upd_relative_width key {relative_width,relative_height,caption } : fig_content =
|
||||
{relative_width = key,relative_height = relative_height,caption = caption}: fig_content
|
||||
|
||||
fun upd_scale key {relative_width,scale,caption } : fig_content =
|
||||
{relative_width = relative_width,scale = key,caption = caption}: fig_content
|
||||
fun upd_relative_height key {relative_width,relative_height,caption } : fig_content =
|
||||
{relative_width = relative_width,relative_height = key,caption = caption}: fig_content
|
||||
|
||||
fun upd_caption key {relative_width,scale,caption} : fig_content =
|
||||
{relative_width = relative_width,scale = scale,caption= key}: fig_content
|
||||
fun upd_caption key {relative_width,relative_height,caption} : fig_content =
|
||||
{relative_width = relative_width,relative_height = relative_height,caption= key}: fig_content
|
||||
|
||||
|
||||
val widthN = "width"
|
||||
val scaleN = "scale"
|
||||
val heightN = "height"
|
||||
val captionN = "caption";
|
||||
|
||||
fun fig_content_modes (ctxt, toks) =
|
||||
|
|
@ -297,8 +293,8 @@ fun fig_content_modes (ctxt, toks) =
|
|||
(Parse.list1
|
||||
( (Args.$$$ widthN |-- Args.$$$ "=" -- Parse.int
|
||||
>> (fn (_, k) => upd_relative_width k))
|
||||
|| (Args.$$$ scaleN |-- Args.$$$ "=" -- Parse.int
|
||||
>> (fn (_, k) => upd_scale k))
|
||||
|| (Args.$$$ heightN |-- Args.$$$ "=" -- Parse.int
|
||||
>> (fn (_, k) => upd_relative_height k))
|
||||
|| (Args.$$$ captionN |-- Args.$$$ "=" -- Parse.document_source
|
||||
>> (fn (_, k) => upd_caption k))
|
||||
))) [K mt_fig_content])
|
||||
|
|
@ -329,41 +325,48 @@ fun get_document_dir ctxt =
|
|||
val sess_dir = get_session_dir ctxt (Resources.master_directory thy)
|
||||
in Path.append sess_dir (Path.explode "document") end;
|
||||
|
||||
fun generate_caption ctxt caption =
|
||||
let
|
||||
val cap_txt= Document_Output.output_document ctxt {markdown = false} caption
|
||||
fun drop_latex_macro (XML.Elem (("latex_environment", [("name", "isabelle")]),xmlt)) = xmlt
|
||||
|drop_latex_macro X = [X]
|
||||
val drop_latex_macros = List.concat o map drop_latex_macro;
|
||||
in
|
||||
drop_latex_macros cap_txt
|
||||
end
|
||||
fun fig_content ctxt (cfg_trans,file:Input.source) =
|
||||
let val {relative_width,relative_height,caption} = cfg_trans mt_fig_content
|
||||
val _ = if relative_width < 0 orelse relative_height <0 then error("negative parameter.")
|
||||
else ()
|
||||
val wdth_val_s = Real.toString((Real.fromInt relative_width)
|
||||
/ (Real.fromInt 100))^"\\textwidth"
|
||||
val ht_s= if relative_height = 100 then ""
|
||||
else "height="^Real.toString((Real.fromInt relative_height)
|
||||
/ (Real.fromInt 100)) ^"\\textheight"
|
||||
val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s])
|
||||
val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
|
||||
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
|
||||
|
||||
in if Input.string_of(caption) = "" then
|
||||
file
|
||||
|> (Latex.string o Input.string_of)
|
||||
|> (XML.enclose ("\\includegraphics"^arg^"{") "}")
|
||||
else
|
||||
file
|
||||
|> (Latex.string o Input.string_of)
|
||||
|> (fn X => (Latex.string ("{"^wdth_val_s^"}"))
|
||||
@ (Latex.string "\\centering")
|
||||
@ (XML.enclose ("\\includegraphics"^arg^"{") "}" X)
|
||||
@ (Latex.macro "caption" (generate_caption ctxt caption)))
|
||||
|> (Latex.environment ("subcaptionblock") )
|
||||
(* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *)
|
||||
end
|
||||
|
||||
fun fig_content_antiquotation name scan =
|
||||
(Document_Output.antiquotation_raw_embedded name
|
||||
(scan : ((fig_content -> fig_content) * Input.source) context_parser)
|
||||
(fn ctxt =>
|
||||
(fn (cfg_trans,file:Input.source) =>
|
||||
let val {relative_width,scale,caption} = cfg_trans mt_fig_content
|
||||
val _ = if relative_width < 0 orelse scale<0 then error("negative parameter.")
|
||||
else ()
|
||||
val wdth_s = if relative_width = 100 then ""
|
||||
else "width="^Real.toString((Real.fromInt relative_width)
|
||||
/ (Real.fromInt 100))^"\\textwidth"
|
||||
val scale_s= if scale = 100 then ""
|
||||
else "scale="^Real.toString((Real.fromInt scale) / (Real.fromInt 100))
|
||||
val arg = enclose "[" "]" (commas [wdth_s,scale_s])
|
||||
val cap_txt= Document_Output.output_document ctxt {markdown = false} caption
|
||||
fun drop_latex_macro (XML.Elem (("latex_environment", [("name", "isabelle")]),xmlt)) = xmlt
|
||||
|drop_latex_macro X = [X];
|
||||
val drop_latex_macros = List.concat o map drop_latex_macro;
|
||||
val cap_txt = drop_latex_macros cap_txt
|
||||
val path = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
|
||||
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
|
||||
|
||||
in file
|
||||
|> (Latex.string o Input.string_of)
|
||||
|> (XML.enclose ("\\includegraphics"^arg^"{") "}")
|
||||
|> (fn X => X @ Latex.macro "caption" cap_txt)
|
||||
end
|
||||
)
|
||||
));
|
||||
|
||||
val _ = fig_content_antiquotation
|
||||
: binding
|
||||
-> ((fig_content -> fig_content) * Input.source) context_parser
|
||||
-> theory -> theory
|
||||
(fig_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text));
|
||||
|
||||
|
||||
val _ = Theory.setup
|
||||
( fig_content_antiquotation \<^binding>\<open>fig_content\<close>
|
||||
|
|
@ -373,32 +376,68 @@ val _ = Theory.setup
|
|||
|
||||
|
||||
ML\<open>
|
||||
val _ = Path.parent
|
||||
val mdir = Resources.master_directory @{theory}
|
||||
val pp = Resources.check_session_dir @{context}
|
||||
(SOME (Path.dir mdir )) (Syntax.read_input ".nnn")
|
||||
handle ERROR s => (if String.isPrefix "No such directory:" s then
|
||||
(writeln ("MMM"^s); mdir)
|
||||
else error s)
|
||||
|
||||
(*
|
||||
type fig_content = {relative_width : int, (* percent of textwidth, default 100 *)
|
||||
relative_height : int, (* percent, default 100 *)
|
||||
caption : Input.source (* default empty *)}
|
||||
|
||||
val ppp = (Path.explode "document")
|
||||
*)
|
||||
val SPY = Unsynchronized.ref("")
|
||||
|
||||
fun get_session_dir ctxt path =
|
||||
Resources.check_session_dir ctxt
|
||||
(SOME (path))
|
||||
(Syntax.read_input ".")
|
||||
handle ERROR s => (if String.isPrefix "Bad session root directory (missing ROOT or ROOTS): " s
|
||||
then get_session_dir ctxt (Path.dir path)
|
||||
else error s)
|
||||
(* ML\<open>snd(HOLogic.dest_number(Syntax.read_term @{context} (!SPY)))\<close>
|
||||
*)
|
||||
fun convert_meta_args (X, (((str,_),value) :: R)) =
|
||||
let fun conv_int x = snd(HOLogic.dest_number(Syntax.read_term @{context} x))
|
||||
handle TERM x => error "Illegal int format."
|
||||
in
|
||||
(case YXML.content_of str of
|
||||
"relative_width" => upd_relative_width (conv_int value)
|
||||
o convert_meta_args (X, R)
|
||||
| "relative_height" => upd_relative_height (conv_int value)
|
||||
o convert_meta_args (X, R )
|
||||
| "file_src" => convert_meta_args (X, R)
|
||||
| s => error("!undefined attribute:"^s))
|
||||
end
|
||||
|convert_meta_args (X,[]) = I
|
||||
|
||||
fun get_document_dir ctxt =
|
||||
let val thy = Proof_Context.theory_of ctxt
|
||||
val sess_dir = get_session_dir ctxt (Resources.master_directory thy)
|
||||
in Path.append sess_dir (Path.explode "document") end;
|
||||
fun convert_src_from_margs (X, (((str,_),value)::R)) =
|
||||
(case YXML.content_of str of
|
||||
"file_src" => Input.string (HOLogic.dest_string (Syntax.read_term @{context} value))
|
||||
| _ => convert_src_from_margs(X,R))
|
||||
|convert_src_from_margs (X, []) = error("No file_src provided.")
|
||||
|
||||
fun float_command (name, pos) descr cid =
|
||||
let fun set_default_class NONE = SOME(cid,pos)
|
||||
|set_default_class (SOME X) = SOME X
|
||||
fun create_instance ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
|
||||
Value_Command.Docitem_Parser.create_and_check_docitem
|
||||
{is_monitor = false}
|
||||
{is_inline = true}
|
||||
{define = true} oid pos (set_default_class cid_pos) doc_attrs
|
||||
val opts = {markdown = false, body = true}
|
||||
fun parse_and_tex opts (margs, text) ctxt = (fig_content ctxt
|
||||
(convert_meta_args margs o upd_caption Input.empty,
|
||||
convert_src_from_margs margs))
|
||||
|> (fn X => (Latex.macro0 "centering"
|
||||
@ X
|
||||
@ Latex.macro "caption" (generate_caption ctxt text)))
|
||||
|> (Latex.environment ("figure") )
|
||||
in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex
|
||||
end
|
||||
|
||||
get_document_dir @{context}
|
||||
\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
(* *********************************************************************** *)
|
||||
(* Ontological Macro Command Support *)
|
||||
(* *********************************************************************** *)
|
||||
|
||||
float_command \<^command_keyword>\<open>figure*\<close> "figure" "Isa_COL.figure" ;
|
||||
val _ = Onto_Macros.heading_command \<^command_keyword>\<open>side_by_side_figure*\<close> "multiple figures" NONE;
|
||||
\<close>
|
||||
|
||||
subsection\<open>Tables\<close>
|
||||
(* TODO ! ! ! *)
|
||||
(* dito the future monitor: table - block *)
|
||||
|
|
@ -673,7 +712,7 @@ declare[[tab_cell_placing="left",tab_cell_height="18.0cm"]]
|
|||
section\<open>Tests\<close>
|
||||
(*<*)
|
||||
|
||||
text\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
|
||||
text\<open> @{fig_content [display] (height = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
|
||||
\<open>figures/isabelle-architecture.pdf\<close>}\<close>
|
||||
text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open>12.0cm\<close>,
|
||||
cell_height =\<open>13pt\<close>, cell_width = \<open>12.0cm\<close>,
|
||||
|
|
@ -685,11 +724,6 @@ text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open
|
|||
|
||||
(*>*)
|
||||
|
||||
ML\<open>@{term "side_by_side_figure"};
|
||||
@{typ "doc_class rexp"};
|
||||
DOF_core.SPY;
|
||||
|
||||
\<close>
|
||||
|
||||
text\<open>@{term_ \<open>3 + 4::int\<close>} @{value_ \<open>3 + 4::int\<close>} \<close>
|
||||
end
|
||||
|
|
|
|||
|
|
@ -670,8 +670,6 @@ fun typ_to_cid (Type(s,[\<^Type>\<open>unit\<close>])) = Long_Name.qualifier s
|
|||
|typ_to_cid _ = error("type is not an ontological type.")
|
||||
|
||||
|
||||
val SPY = Unsynchronized.ref(Bound 0)
|
||||
|
||||
fun check_regexps term =
|
||||
let val _ = case fold_aterms Term.add_free_names term [] of
|
||||
n::_ => error("No free variables allowed in monitor regexp:" ^ n)
|
||||
|
|
@ -806,24 +804,24 @@ fun binding_from_onto_class_pos name thy =
|
|||
fun binding_from_instance_pos name thy =
|
||||
binding_from_pos get_instances get_instance_name_global name thy
|
||||
|
||||
fun check_invs get_ml_invs cid_long oid is_monitor thy =
|
||||
fun check_invs get_ml_invs invariant_class_of invariant_check_of cid_long oid is_monitor thy =
|
||||
thy |> Context.Theory
|
||||
|> (fn ctxt =>
|
||||
let val invs = get_ml_invs (Proof_Context.init_global thy)
|
||||
|> Name_Space.dest_table
|
||||
val checks = invs |> filter (fn (_, inv) => let val ML_Invariant class = inv
|
||||
in class |> #class |> equal cid_long
|
||||
end)
|
||||
|> map (fn (_, inv) => let val ML_Invariant check = inv
|
||||
in check |> #check end)
|
||||
val checks = invs |> filter (fn (name, _) =>
|
||||
equal (invariant_class_of name thy) cid_long)
|
||||
|> map (fn (name, _) => invariant_check_of name thy)
|
||||
|> map (fn check => check oid is_monitor ctxt)
|
||||
in (List.all I checks) end)
|
||||
in (forall I checks) end)
|
||||
|
||||
val check_ml_invs = check_invs get_ml_invariants
|
||||
val check_ml_invs = check_invs get_ml_invariants ml_invariant_class_of ml_invariant_check_of
|
||||
|
||||
val check_opening_ml_invs = check_invs get_opening_ml_invariants
|
||||
val check_opening_ml_invs =
|
||||
check_invs get_opening_ml_invariants opening_ml_invariant_class_of opening_ml_invariant_check_of
|
||||
|
||||
val check_closing_ml_invs = check_invs get_closing_ml_invariants
|
||||
val check_closing_ml_invs =
|
||||
check_invs get_closing_ml_invariants closing_ml_invariant_class_of closing_ml_invariant_check_of
|
||||
|
||||
(* Output name for LaTeX macros.
|
||||
Also rewrite "." to allow macros with objects long names *)
|
||||
|
|
@ -833,12 +831,10 @@ val ISA_prefix = "Isabelle_DOF_"
|
|||
|
||||
val doc_class_prefix = ISA_prefix ^ "doc_class_"
|
||||
|
||||
val long_doc_class_prefix = ISA_prefix ^ "long_doc_class_"
|
||||
|
||||
fun is_ISA s = String.isPrefix ISA_prefix (Long_Name.base_name s)
|
||||
|
||||
fun get_class_name_without_prefix s = String.extract (s, String.size(doc_class_prefix), NONE)
|
||||
|
||||
fun get_doc_class_name_without_ISA_prefix s = String.extract (s, String.size(ISA_prefix), NONE)
|
||||
|
||||
|
||||
fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy =
|
||||
(* pre: term should be fully typed in order to allow type-related term-transformations *)
|
||||
|
|
@ -1066,27 +1062,6 @@ struct
|
|||
fun err msg pos = error (msg ^ Position.here pos);
|
||||
fun warn msg pos = warning (msg ^ Position.here pos);
|
||||
|
||||
fun check_path check_file ctxt dir (name, pos) =
|
||||
let
|
||||
val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be
|
||||
"lifted" to
|
||||
type source *)
|
||||
|
||||
val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
|
||||
val _ = Path.expand path handle ERROR msg => err msg pos;
|
||||
val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
|
||||
val _ =
|
||||
(case check_file of
|
||||
NONE => path
|
||||
| SOME check => (check path handle ERROR msg => err msg pos));
|
||||
in path end;
|
||||
|
||||
|
||||
fun ML_isa_antiq check_file thy (name, _, pos) =
|
||||
let val path = check_path check_file (Proof_Context.init_global thy) Path.current (name, pos);
|
||||
in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
|
||||
|
||||
|
||||
fun ML_isa_check_generic check thy (term, pos) =
|
||||
let val name = (HOLogic.dest_string term
|
||||
handle TERM(_,[t]) => error ("wrong term format: must be string constant: "
|
||||
|
|
@ -1115,19 +1090,20 @@ fun ML_isa_check_thm thy (term, _, pos) _ =
|
|||
|
||||
fun ML_isa_check_file thy (term, _, pos) _ =
|
||||
let fun check thy (name, _) = name |> Syntax.read_input
|
||||
|> Resources.check_file (Proof_Context.init_global thy) NONE
|
||||
|> Resources.check_file (Proof_Context.init_global thy) NONE
|
||||
in ML_isa_check_generic check thy (term, pos) end;
|
||||
|
||||
fun check_instance thy (term, _, pos) s =
|
||||
let
|
||||
val bname = Long_Name.base_name s;
|
||||
val qual = Long_Name.qualifier s;
|
||||
val class_name =
|
||||
Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE));
|
||||
val class_name = (case try (unprefix DOF_core.doc_class_prefix) bname of
|
||||
NONE => unprefix DOF_core.long_doc_class_prefix bname
|
||||
| SOME name => name)
|
||||
|> Long_Name.qualify qual
|
||||
fun check thy (name, _) =
|
||||
let
|
||||
val object_cid = let val DOF_core.Instance cid = DOF_core.get_instance_global name thy
|
||||
in cid |> #cid end
|
||||
val object_cid = DOF_core.cid_of name thy
|
||||
fun check' (class_name, object_cid) =
|
||||
if class_name = object_cid then
|
||||
DOF_core.value_of name thy
|
||||
|
|
@ -1150,6 +1126,11 @@ fun ML_isa_check_trace_attribute thy (term, _, _) _ =
|
|||
val _ = DOF_core.get_instance_global oid thy
|
||||
in SOME term end
|
||||
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
|
||||
case term_option of
|
||||
NONE => error("Wrong term option. You must use a defined term")
|
||||
| SOME term => Const (isa_name, ty) $ term
|
||||
|
||||
(* Convert excluded mixfix symbols.
|
||||
Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
|
||||
we can not use "_" or "'" for classes names in term antiquotation.
|
||||
|
|
@ -1159,10 +1140,19 @@ val clean_string = translate_string
|
|||
| "'" => "-"
|
||||
| c => c);
|
||||
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
|
||||
case term_option of
|
||||
NONE => error("Wrong term option. You must use a defined term")
|
||||
| SOME term => Const (isa_name, ty) $ term
|
||||
fun rm_mixfix name mixfix thy =
|
||||
let
|
||||
val old_constants =
|
||||
Consts.dest (Sign.consts_of thy) |> #constants
|
||||
|> map fst
|
||||
|> filter (Long_Name.base_name #> equal name)
|
||||
|> map (pair mixfix)
|
||||
|> map swap
|
||||
|> map (apfst (Syntax.read_term_global thy))
|
||||
|> map (apsnd Mixfix.mixfix)
|
||||
in thy |> (Local_Theory.notation false Syntax.mode_default old_constants
|
||||
|> Named_Target.theory_map)
|
||||
end
|
||||
|
||||
fun elaborate_instance thy _ _ term_option pos =
|
||||
case term_option of
|
||||
|
|
@ -1177,49 +1167,64 @@ fun elaborate_instance thy _ _ term_option pos =
|
|||
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
|
||||
by add_doc_class_cmd function
|
||||
*)
|
||||
fun declare_ISA_class_accessor_and_check_instance doc_class_name =
|
||||
fun declare_ISA_class_accessor_and_check_instance (doc_class_name, bind_pos) thy =
|
||||
let
|
||||
val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name
|
||||
val typestring = "string => " ^ (Binding.name_of doc_class_name)
|
||||
val conv_class_name = clean_string (Binding.name_of doc_class_name)
|
||||
val mixfix_string = "@{" ^ conv_class_name ^ " _}"
|
||||
val bname = Long_Name.base_name doc_class_name
|
||||
val bname' = prefix DOF_core.doc_class_prefix bname
|
||||
val bind = bname' |> pair bind_pos |> swap |> Binding.make
|
||||
val bind' = prefix DOF_core.long_doc_class_prefix bname
|
||||
|> pair bind_pos |> swap |> Binding.make
|
||||
val const_typ = \<^typ>\<open>string\<close> --> Syntax.read_typ (Proof_Context.init_global thy) doc_class_name
|
||||
fun mixfix_enclose name = name |> enclose "@{" " _}"
|
||||
val mixfix = clean_string bname |> mixfix_enclose
|
||||
val mixfix' = clean_string doc_class_name |> mixfix_enclose
|
||||
in
|
||||
Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))]
|
||||
#> DOF_core.add_isa_transformer bind ((check_instance, elaborate_instance)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
thy |> rm_mixfix bname' mixfix
|
||||
|> Sign.add_consts [(bind, const_typ, Mixfix.mixfix mixfix)]
|
||||
|> DOF_core.add_isa_transformer bind ((check_instance, elaborate_instance)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
|> Sign.add_consts [(bind', const_typ, Mixfix.mixfix mixfix')]
|
||||
|> DOF_core.add_isa_transformer bind' ((check_instance, elaborate_instance)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
end
|
||||
|
||||
fun elaborate_instances_list thy isa_name _ _ _ =
|
||||
let
|
||||
val base_name = Long_Name.base_name isa_name
|
||||
fun get_isa_name_without_intances_suffix s =
|
||||
String.extract (s, 0, SOME (String.size(s) - String.size(instances_of_suffixN)))
|
||||
val base_name_without_suffix = get_isa_name_without_intances_suffix base_name
|
||||
val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
|
||||
val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
(base_name')
|
||||
val long_class_name = DOF_core.get_onto_class_name_global base_name' thy
|
||||
val qualifier = Long_Name.qualifier isa_name
|
||||
val isa_name' = (case try (unprefix DOF_core.doc_class_prefix) base_name of
|
||||
NONE => unprefix DOF_core.long_doc_class_prefix base_name
|
||||
| SOME name => name)
|
||||
|> unsuffix instances_of_suffixN
|
||||
|> Long_Name.qualify qualifier
|
||||
val class_typ = isa_name' |> Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
val long_class_name = DOF_core.get_onto_class_name_global isa_name' thy
|
||||
val values = thy |> Proof_Context.init_global |> DOF_core.get_instances
|
||||
|> Name_Space.dest_table
|
||||
|> filter (fn (_, instance) =>
|
||||
let val DOF_core.Instance cid = instance
|
||||
in (cid |> #cid) = long_class_name end)
|
||||
|> filter (fn (name, _) => equal (DOF_core.cid_of name thy) long_class_name)
|
||||
|> map (fn (oid, _) => DOF_core.value_of oid thy)
|
||||
in HOLogic.mk_list class_typ values end
|
||||
|
||||
|
||||
fun declare_class_instances_annotation thy doc_class_name =
|
||||
fun declare_class_instances_annotation (doc_class_name, bind_pos) thy =
|
||||
let
|
||||
val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name
|
||||
|> Binding.suffix_name instances_of_suffixN
|
||||
val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
((Binding.name_of doc_class_name) ^ " List.list")
|
||||
val conv_class_name' = clean_string ((Binding.name_of doc_class_name) ^ instances_of_suffixN)
|
||||
val mixfix_string = "@{" ^ conv_class_name' ^ "}"
|
||||
val bname = Long_Name.base_name doc_class_name
|
||||
val bname' = prefix DOF_core.doc_class_prefix bname |> suffix instances_of_suffixN
|
||||
val bind = bname' |> pair bind_pos |> swap |> Binding.make
|
||||
val bind' = prefix DOF_core.long_doc_class_prefix bname
|
||||
|> suffix instances_of_suffixN |> pair bind_pos |> swap |> Binding.make
|
||||
val class_typ = doc_class_name |> Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
fun mixfix_enclose name = name |> enclose "@{" "}"
|
||||
val mixfix = clean_string (bname ^ instances_of_suffixN) |> mixfix_enclose
|
||||
val mixfix' = clean_string (doc_class_name ^ instances_of_suffixN) |> mixfix_enclose
|
||||
in
|
||||
Sign.add_consts [(bind, class_list_typ, Mixfix.mixfix(mixfix_string))]
|
||||
#> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
thy |> rm_mixfix bname' mixfix
|
||||
|> Sign.add_consts [(bind, \<^Type>\<open>list class_typ\<close>, Mixfix.mixfix mixfix)]
|
||||
|> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
|> Sign.add_consts [(bind', \<^Type>\<open>list class_typ\<close>, Mixfix.mixfix mixfix')]
|
||||
|> DOF_core.add_isa_transformer bind' ((check_identity, elaborate_instances_list)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
end
|
||||
|
||||
fun symbex_attr_access0 ctxt proj_term term =
|
||||
|
|
@ -2172,16 +2177,32 @@ fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_
|
|||
fun markup xml =
|
||||
let val m = if body then Markup.latex_body else Markup.latex_heading
|
||||
in [XML.Elem (m (Latex.output_name name), xml)] end;
|
||||
in document_output {markdown = markdown, markup = markup} sem_attrs transform_attr meta_args text ctxt end;
|
||||
val config = {markdown = markdown, markup = markup}
|
||||
in document_output config sem_attrs transform_attr meta_args text ctxt
|
||||
end;
|
||||
|
||||
|
||||
(* document output commands *)
|
||||
|
||||
fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
|
||||
Outer_Syntax.command (name, pos) descr
|
||||
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
|
||||
Toplevel.theory' (fn _ => cmd meta_args)
|
||||
(Toplevel.presentation_context #> document_output_reports name mark sem_attrs transform_attr meta_args text #> SOME)));
|
||||
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >>
|
||||
(fn (meta_args, text) =>
|
||||
Toplevel.theory' (fn _ => cmd meta_args)
|
||||
((Toplevel.presentation_context
|
||||
#> document_output_reports name mark sem_attrs transform_attr meta_args text
|
||||
#> SOME): Toplevel.state -> Latex.text option)) );
|
||||
|
||||
|
||||
fun float_command (name, pos) descr (mark: {body: bool, markdown: bool})
|
||||
cmd output_figure =
|
||||
Outer_Syntax.command (name, pos) descr
|
||||
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >>
|
||||
(fn (meta_args, text) =>
|
||||
Toplevel.theory' (fn _ => cmd meta_args)
|
||||
(Toplevel.presentation_context
|
||||
#> (fn ctxt => (output_figure mark (meta_args, text)) ctxt)
|
||||
#> SOME)))
|
||||
|
||||
|
||||
(* Core Command Definitions *)
|
||||
|
|
@ -2952,6 +2973,7 @@ fun define_inv cid_long ((lbl, pos), inv) thy =
|
|||
fun add_doc_class_cmd overloaded (raw_params, binding)
|
||||
raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy =
|
||||
let
|
||||
val bind_pos = Binding.pos_of binding
|
||||
val ctxt = Proof_Context.init_global thy;
|
||||
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
|
||||
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
|
||||
|
|
@ -3008,8 +3030,8 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
|||
(* The function declare_ISA_class_accessor_and_check_instance uses a prefix
|
||||
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
|
||||
by add_doc_class_cmd function *)
|
||||
|> ISA_core.declare_ISA_class_accessor_and_check_instance binding
|
||||
|> (fn thy => (ISA_core.declare_class_instances_annotation thy binding) thy)
|
||||
|> (fn thy => ISA_core.declare_ISA_class_accessor_and_check_instance (cid thy, bind_pos) thy)
|
||||
|> (fn thy => ISA_core.declare_class_instances_annotation (cid thy, bind_pos) thy)
|
||||
end;
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -17,6 +17,7 @@ theory "M_01_Introduction"
|
|||
begin
|
||||
(*>*)
|
||||
|
||||
|
||||
chapter*[intro::introduction]\<open> Introduction \<close>
|
||||
text*[introtext::introduction]\<open>
|
||||
The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the most pervasive challenge in the
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ begin
|
|||
chapter*[background::text_section]\<open> Background\<close>
|
||||
section*[bgrnd1::introduction]\<open>The Isabelle System Architecture\<close>
|
||||
|
||||
figure*[architecture::figure,relative_width="95",src="''figures/isabelle-architecture''"]\<open>
|
||||
figure*[architecture::figure,relative_width="95",file_src="''figures/isabelle-architecture.pdf''"]\<open>
|
||||
The system architecture of Isabelle (left-hand side) and the
|
||||
asynchronous communication between the Isabelle system and
|
||||
the IDE (right-hand side). \<close>
|
||||
|
|
@ -45,7 +45,7 @@ The current system framework offers moreover the following features:
|
|||
the most prominent and deeply integrated system component.
|
||||
\<close>
|
||||
text\<open>
|
||||
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers,
|
||||
The Isabelle system architecture shown in @{figure \<open>architecture\<close>} comes with many layers,
|
||||
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
|
||||
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>.
|
||||
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
|
||||
|
|
@ -102,17 +102,18 @@ text\<open>
|
|||
\<^boxed_theory_text>\<open>keywords\<close> are used to separate commands from each other.
|
||||
\<close>
|
||||
|
||||
side_by_side_figure*[docModGenConcr::side_by_side_figure,anchor="''docModGen''",
|
||||
caption="''Schematic Representation.''",relative_width="45",
|
||||
src="''figures/doc-mod-generic.pdf''",anchor2="''docModIsar''",
|
||||
caption2="''The Isar Instance.''",relative_width2="45",
|
||||
src2="''figures/doc-mod-isar.pdf''"]\<open>A Representation of a Document Model.\<close>
|
||||
text*[docModGenConcr::float,
|
||||
main_caption="\<open>A Representation of a Document Model.\<close>"]
|
||||
\<open>
|
||||
@{fig_content (width=45, caption="Schematic Representation.") "figures/doc-mod-generic.pdf"
|
||||
}\<^hfill>@{fig_content (width=45, caption="The Isar Instance.") "figures/doc-mod-isar.pdf"}
|
||||
\<close>
|
||||
|
||||
text\<open>The body of a theory file consists of a sequence of \<^emph>\<open>commands\<close> that must be introduced
|
||||
by a command keyword such as \<^boxed_theory_text>\<open>requirement\<close> above. Command keywords may mark
|
||||
the the begin of a text that is parsed by a command-specific parser; the end of the
|
||||
command-span is defined by the next keyword. Commands were used to define definitions, lemmas,
|
||||
code and text-elements (see @{figure "docModGenConcr"}(right)). \<close>
|
||||
code and text-elements (see @{float "docModGenConcr"}(right)). \<close>
|
||||
|
||||
text\<open> A simple text-element \<^index>\<open>text-element\<close> may look like this:
|
||||
|
||||
|
|
@ -182,17 +183,18 @@ text\<open>Antiquotations seen as semantic macros are partial functions of type
|
|||
typeset. They represent the device for linking formal with the informal content.
|
||||
\<close>
|
||||
|
||||
side_by_side_figure*[docModOnto::side_by_side_figure,anchor="''docModGen''",
|
||||
caption="''A Document with Ontological Annotations.''",relative_width="47",
|
||||
src="''figures/doc-mod-DOF.pdf''",anchor2="''docModDOF''",
|
||||
caption2="''Ontological References.''",relative_width2="47",
|
||||
src2="''figures/doc-mod-onto-docinst.pdf''"]\<open>Documents conform to Ontologies.\<close>
|
||||
text*[docModOnto::float,
|
||||
main_caption="\<open>Documents conform to Ontologies.\<close>"]
|
||||
\<open>
|
||||
@{fig_content (width=47, caption="A Document with Ontological Annotations.") "figures/doc-mod-DOF.pdf"
|
||||
}\<^hfill>@{fig_content (width=47, caption="Ontological References.") "figures/doc-mod-onto-docinst.pdf"}
|
||||
\<close>
|
||||
|
||||
text\<open>Since Isabelle's commands are freely programmable, it is possible to implement \<^dof> as an
|
||||
extension of the system. In particular, the ontology language of \<^dof> provides an ontology
|
||||
definition language ODL\<^bindex>\<open>ODL\<close> that \<^emph>\<open>generates\<close> anti-quotations and the infrastructure to check and evaluate
|
||||
them. This allows for checking an annotated document with respect to a given ontology, which may be
|
||||
specific for a given domain-specific universe of discourse (see @{figure "docModOnto"}). ODL will
|
||||
specific for a given domain-specific universe of discourse (see @{float "docModOnto"}). ODL will
|
||||
be described in @{text_section (unchecked) "isadof_tour"} in more detail.\<close>
|
||||
|
||||
section*[bgrnd21::introduction]\<open>Implementability of the Document Model in other ITP's\<close>
|
||||
|
|
@ -207,13 +209,13 @@ text\<open>
|
|||
in many features over-accomplishes the required features of \<^dof>.
|
||||
\<close>
|
||||
|
||||
figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\<open>
|
||||
figure*["fig:dof-ide",relative_width="95",file_src="''figures/cicm2018-combined.png''"]\<open>
|
||||
The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page
|
||||
of~@{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
|
||||
|
||||
text\<open>
|
||||
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
|
||||
@{figure "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,
|
||||
while the generated presentation in PDF is shown on the right.
|
||||
|
||||
|
|
|
|||
|
|
@ -332,10 +332,10 @@ which is written in the so-called free-form style: Formulas are superficially pa
|
|||
type-set, but no deeper type-checking and checking with the underlying logical context
|
||||
is undertaken. \<close>
|
||||
|
||||
figure*[fig0::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_source.png''"]
|
||||
figure*[fig0::figure,relative_width="90",file_src="''figures/header_CSP_source.png''"]
|
||||
\<open> A mathematics paper as integrated document source ... \<close>
|
||||
|
||||
figure*[fig0B::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_pdf.png''"]
|
||||
figure*[fig0B::figure,relative_width="90",file_src="''figures/header_CSP_pdf.png''"]
|
||||
\<open> ... and as corresponding \<^pdf>-output. \<close>
|
||||
|
||||
text\<open>The integrated source of this paper-excerpt is shown in \<^figure>\<open>fig0\<close>, while the
|
||||
|
|
@ -382,7 +382,7 @@ standard inductive \<^theory_text>\<open>datatype\<close> definition mechanism i
|
|||
for attribute declarations. Vice-versa, document class definitions imply a corresponding HOL type
|
||||
definition. \<close>
|
||||
|
||||
figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"]
|
||||
figure*[fig01::figure,relative_width="95",file_src="''figures/definition-use-CSP.png''"]
|
||||
\<open> A screenshot of the integrated source with definitions ...\<close>
|
||||
text\<open>An example for a sequence of (Isabelle-formula-)texts, their ontological declarations as
|
||||
\<^typ>\<open>definition\<close>s in terms of the \<^verbatim>\<open>scholarly_paper\<close>-ontology and their type-conform referencing
|
||||
|
|
@ -406,7 +406,7 @@ We refrain ourselves here to briefly describe three freeform antiquotations used
|
|||
\<^item> the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements.
|
||||
\<close>
|
||||
|
||||
figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"]
|
||||
figure*[fig02::figure,relative_width="95",file_src="''figures/definition-use-CSP-pdf.png''"]
|
||||
\<open> ... and the corresponding \<^pdf>-output.\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -431,7 +431,7 @@ doc_class figure = text_section +
|
|||
spawn_columns :: bool <= True
|
||||
\<close>}
|
||||
\<close>
|
||||
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
|
||||
figure*[fig_figures::figure,relative_width="85",file_src="''figures/Dogfood-figures.png''"]
|
||||
\<open> Declaring figures in the integrated source.\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -466,42 +466,40 @@ which signals to \<^isadof> begin and end of the part of the integrated source
|
|||
in which the text-elements instances are expected to appear in the textual ordering
|
||||
defined by \<^typ>\<open>article\<close>.
|
||||
\<close>
|
||||
text*[exploring::float,
|
||||
main_caption="\<open>Exploring text elements.\<close>"]
|
||||
\<open>
|
||||
@{fig_content (width=48, caption="Exploring a reference of a text-element.") "figures/Dogfood-II-bgnd1.png"
|
||||
}\<^hfill>@{fig_content (width=47, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"}
|
||||
\<close>
|
||||
|
||||
side_by_side_figure*[exploring::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''",
|
||||
caption="''Exploring a reference of a text-element.''",relative_width="48",
|
||||
src="''figures/Dogfood-II-bgnd1''",anchor2="''fig-bgnd-text_section''",
|
||||
caption2="''Exploring the class of a text element.''",relative_width2="47",
|
||||
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open>Exploring text elements.\<close>
|
||||
|
||||
|
||||
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
|
||||
caption="''Hyperlink to class-definition.''",relative_width="48",
|
||||
src="''figures/Dogfood-IV-jumpInDocCLass''",
|
||||
anchor2="''fig:Dogfood-V-attribute''",
|
||||
caption2="''Exploring an attribute (hyperlinked to the class).''",
|
||||
relative_width2="47",
|
||||
src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
|
||||
text*[hyperlinks::float,
|
||||
main_caption="\<open>Navigation via generated hyperlinks.\<close>"]
|
||||
\<open>
|
||||
@{fig_content (width=48, caption="Hyperlink to class-definition.") "figures/Dogfood-IV-jumpInDocCLass.png"
|
||||
}\<^hfill>@{fig_content (width=47, caption="Exploring an attribute (hyperlinked to the class).") "figures/Dogfood-V-attribute.png"}
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
From these class definitions, \<^isadof> also automatically generated editing
|
||||
support for Isabelle/jEdit. In
|
||||
@{figure "exploring"}(left)
|
||||
@{float "exploring"}(left)
|
||||
% \autoref{fig-Dogfood-II-bgnd1}
|
||||
and
|
||||
@{figure "exploring"}(right)
|
||||
@{float "exploring"}(right)
|
||||
% \autoref{fig-bgnd-text_section}
|
||||
we show how hovering over links permits to explore its
|
||||
meta-information. Clicking on a document class identifier permits to hyperlink into the
|
||||
corresponding class definition (
|
||||
@{figure "hyperlinks"}(left)
|
||||
@{float "hyperlinks"}(left)
|
||||
%\autoref{fig:Dogfood-IV-jumpInDocCLass})
|
||||
; hovering over an attribute-definition (which is qualified in order to disambiguate; cf.
|
||||
@{figure "hyperlinks"}(right)
|
||||
@{float "hyperlinks"}(right)
|
||||
%\autoref{fig:Dogfood-V-attribute}
|
||||
) shows its type.
|
||||
\<close>
|
||||
|
||||
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-VI-linkappl.png''"]
|
||||
figure*[figDogfoodVIlinkappl::figure,relative_width="80",file_src="''figures/Dogfood-VI-linkappl.png''"]
|
||||
\<open>Exploring an ontological reference.\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -533,7 +531,7 @@ ontologically checked prior arguments \<open>arg\<^sub>1 ... arg\<^sub>n\<^sub>-
|
|||
process; ontologically, they can be used to assure the traceability of, \<^eg>, semi-formal
|
||||
assumptions throughout their way to formalisation and use in lemmas and proofs. \<close>
|
||||
|
||||
figure*[doc_termAq::figure,relative_width="50",src="''figures/doc-mod-term-aq.pdf''"]
|
||||
figure*[doc_termAq::figure,relative_width="50",file_src="''figures/doc-mod-term-aq.pdf''"]
|
||||
\<open>Term-Antiquotations Referencing to Annotated Elements\<close>
|
||||
text\<open>As shown in @{figure \<open>doc_termAq\<close>}, this feature of \<^isadof> substantially increases
|
||||
the expressibility of links between the formal and the informal in \<^dof> documents.\<close>
|
||||
|
|
@ -639,7 +637,7 @@ So its value is that readers can just reuse some of these snippets and adapt the
|
|||
purposes.
|
||||
\<close>
|
||||
|
||||
figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabelle.png''"]
|
||||
figure*[strict_SS::figure, relative_width="95", file_src="''figures/MyCommentedIsabelle.png''"]
|
||||
\<open>A table with a number of SML functions, together with their type.\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
|
|||
Loading…
Reference in New Issue