diff --git a/Isabelle_DOF-Example-I/IsaDofApplications.thy b/Isabelle_DOF-Example-I/IsaDofApplications.thy index 63090c3..a842e3c 100644 --- a/Isabelle_DOF-Example-I/IsaDofApplications.thy +++ b/Isabelle_DOF-Example-I/IsaDofApplications.thy @@ -30,6 +30,7 @@ define_shortcut* isadof \ \\isadof\ (* slanted text in contrast to italics *) define_macro* slanted_text \ \\textsl{\ _ \}\ +define_macro* unchecked_label \ \\autoref{\ _ \}\ ML\ @@ -313,30 +314,7 @@ text\ The following ontology is a simple ontology modeling scientific pape Isabelle users to Isabelle users only. Of course, such references can be added easily and represent a particular strength of \<^isadof>.\ -(* -text\\begin{figure} -@{boxed_theory_text [display]\ -doc_class title = - short_title :: "string option" <= None - -doc_class subtitle = - abbrev :: "string option" <= None - -doc_class author = - affiliation :: "string" - -doc_class abstract = - keyword_list :: "string list" <= None - -doc_class text_section = - main_author :: "author option" <= None - todo_list :: "string list" <= "[]" -\} -\caption{The core of the ontology definition for writing scholarly papers.} -\label{fig:paper-onto-core} -\end{figure}\ -*) -text*["paper_onto_core"::figure2, +text*["paper_onto_core"::float, caption="\The core of the ontology definition for writing scholarly papers.\"] \@{boxed_theory_text [display]\ doc_class title = @@ -357,7 +335,7 @@ doc_class text_section = \}\ text\ The first part of the ontology \<^theory_text>\scholarly_paper\ -(see @{figure2 "paper_onto_core"}) +(see @{float "paper_onto_core"}) contains the document class definitions with the usual text-elements of a scientific paper. The attributes \<^theory_text>\short_title\, \<^theory_text>\abbrev\ etc are introduced with their types as well as their default values. @@ -375,7 +353,7 @@ Science Series, as required by many scientific conferences, is mostly straight-f figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"] \ Ouroboros I: This paper from inside \<^dots> \ -(*<*)declare_reference*[paper_onto_sections::figure2](*>*) +(*<*)declare_reference*[paper_onto_sections::float](*>*) text\\<^vs>\-0.8cm\ @{figure \fig1\} shows the corresponding view in the Isabelle/PIDE of the present paper. Note that the text uses \<^isadof>'s own text-commands containing the meta-information provided by the underlying ontology. @@ -405,8 +383,8 @@ of automated forms of validation check for specific categories of papers is envi Since this requires deeper knowledge in Isabelle programming, however, we consider this out of the scope of this paper. -We proceed more or less conventionally by the subsequent sections (@{figure2 (unchecked)\paper_onto_sections\})\ -text*["paper_onto_sections"::figure2, +We proceed more or less conventionally by the subsequent sections (@{float (unchecked)\paper_onto_sections\})\ +text*["paper_onto_sections"::float, caption = "''Various types of sections of a scholarly papers.''"]\ @{boxed_theory_text [display]\ doc_class example = text_section + @@ -421,10 +399,10 @@ doc_class related_work = conclusion + doc_class bibliography = style :: "string option" <= "''LNCS''" \}\ -(*<*)declare_reference*[paper_onto_monitor::figure2](*>*) +(*<*)declare_reference*[paper_onto_monitor::float](*>*) text\... and finish with a monitor class definition that enforces a textual ordering -in the document core by a regular expression (@{figure2 (unchecked) "paper_onto_monitor"}).\ -text*["paper_onto_monitor"::figure2, +in the document core by a regular expression (@{float (unchecked) "paper_onto_monitor"}).\ +text*["paper_onto_monitor"::float, caption = "''A monitor for the scholarly paper ontology.''"]\ @{boxed_theory_text [display]\ doc_class article = @@ -483,7 +461,7 @@ text\ The latter quality assurance mechanism is used in many universities, where for organizational reasons the execution of an exam takes place in facilities 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). \ -text*["onto_exam"::figure2, +text*["onto_exam"::float, caption = "''The core of the ontology modeling math exams.''"]\ @{boxed_theory_text [display]\ doc_class Author = ... @@ -509,14 +487,14 @@ doc_class Exam_item = type_synonym SubQuestion = string \}\ -(*<*)declare_reference*[onto_questions::figure2](*>*) -text\The heart of this ontology (see @{figure2 "onto_exam"}) is an alternation of questions and answers, +(*<*)declare_reference*[onto_questions::float](*>*) +text\The heart of this ontology (see @{float "onto_exam"}) is an alternation of questions and answers, where the answers can consist of simple yes-no answers (QCM style check-boxes) or lists of formulas. Since we do not assume familiarity of the students with Isabelle (\<^theory_text>\term\ would assume that this is a parse-able and type-checkable entity), we basically model a derivation as a sequence of strings -(see @{figure2 (unchecked)"onto_questions"}).\ -text*["onto_questions"::figure2, +(see @{float (unchecked)"onto_questions"}).\ +text*["onto_questions"::float, caption = "''An exam can contain different types of questions.''"]\ @{boxed_theory_text [display]\ doc_class Answer_Formal_Step = Exam_item + @@ -543,15 +521,15 @@ doc_class Exercise = Exam_item + concerns :: "ContentClass set" <= "UNIV" mark :: int \}\ -(*<*)declare_reference*[onto_exam_monitor::figure2](*>*) +(*<*)declare_reference*[onto_exam_monitor::float](*>*) text\ In many institutions, it makes sense to have a rigorous process of validation for exam subjects: is the initial question correct? Is a proof in the sense of the question possible? We model the possibility that the @{term examiner} validates a -question by a sample proof validated by Isabelle (see @{figure2 (unchecked) "onto_exam_monitor"}). +question by a sample proof validated by Isabelle (see @{float (unchecked) "onto_exam_monitor"}). In our scenario this sample proofs are completely \<^emph>\intern\, \<^ie>, not exposed to the students but just additional material for the internal review process of the exam.\ -text*["onto_exam_monitor"::figure2, +text*["onto_exam_monitor"::float, caption = "''Validating exams.''"]\ @{boxed_theory_text [display]\ doc_class Validation = @@ -600,11 +578,11 @@ As in many other cases, formal certification documents come with an own terminol of what has to be demonstrated and where, and how the trace-ability of requirements through design-models over code to system environment assumptions has to be assured. \ -(*<*)declare_reference*["conceptual"::figure2](*>*) +(*<*)declare_reference*["conceptual"::float](*>*) text\ In the sequel, we present a simplified version of an ontological model used in a case-study~ @{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of requirement -(see @{figure2 (unchecked) "conceptual"}). \ -text*["conceptual"::figure2, +(see @{float (unchecked) "conceptual"}). \ +text*["conceptual"::float, caption = "''Modeling requirements.''"]\ @{boxed_theory_text [display]\ doc_class requirement = long_name :: "string option" @@ -657,11 +635,11 @@ text\ We present a selection of interaction scenarios @{example \sc and @{example \cenelec_onto\} with Isabelle/PIDE instrumented by \<^isadof>. \ subsection*[scholar_pide::example]\ A Scholarly Paper \ -text\ In \autoref{fig-Dogfood-II-bgnd1} and \autoref{fig-bgnd-text_section} we show how +text\ In \<^unchecked_label>\fig-Dogfood-II-bgnd1\ and \<^unchecked_label>\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 (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition -(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}). +class definition (\<^unchecked_label>\fig:Dogfood-IV-jumpInDocCLass\; hovering over an attribute-definition +(which is qualified in order to disambiguate; \<^unchecked_label>\fig:Dogfood-V-attribute\). \ side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''", @@ -678,7 +656,7 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV- (*<*)declare_reference*["figDogfoodVIlinkappl"::figure](*>*) -text\ An ontological reference application in \autoref{figDogfoodVIlinkappl}: the ontology-dependant +text\ An ontological reference application in \<^unchecked_label>\figDogfoodVIlinkappl\: the ontology-dependant antiquotation \<^theory_text>\@{example ...}\ refers to the corresponding text-elements. Hovering allows 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. \ @@ -687,7 +665,7 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood- \ Exploring an attribute (hyperlinked to the class). \ subsection*[cenelec_pide::example]\ CENELEC \ (*<*)declare_reference*[figfig3::figure](*>*) -text\ The corresponding view in @{docitem (unchecked) \figfig3\} shows core part of a document, +text\ The corresponding view in @{figure (unchecked) \figfig3\} shows core part of a document, coherent to the @{example \cenelec_onto\}. The first sample shows standard Isabelle antiquotations @{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.\ diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index 23ca83b..2fb20fe 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -207,7 +207,7 @@ 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.figure", "Isa_COL.chapter", "Isa_COL.figure2", "Isa_COL.section", + "Isa_COL.float", "Isa_COL.figure", "Isa_COL.chapter", "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"] diff --git a/Isabelle_DOF-Unit-Tests/COL_Test.thy b/Isabelle_DOF-Unit-Tests/COL_Test.thy index 945dd79..9854625 100644 --- a/Isabelle_DOF-Unit-Tests/COL_Test.thy +++ b/Isabelle_DOF-Unit-Tests/COL_Test.thy @@ -64,12 +64,12 @@ text\check @{side_by_side_figure sbsfig1} cmp to @{side_by_side_figure sbs (* And a side-chick ... *) -text*[inlinefig::figure2, +text*[inlinefig::float, caption="\The Caption.\"] \@{theory_text [display, margin = 5] \lemma A :: "a \ b"\}\ (*<*) -text*[inlinegraph::figure2, +text*[inlinegraph::float, caption="\Another \\<^sub>i+2 Caption.\"] \@{fig_content [display] (scale = 80, width=80, caption=\This is \<^term>\\\<^sub>i+2\ \\) \document/figures/A.png\}\ diff --git a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy index 148ad28..afe3edb 100644 --- a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy +++ b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy @@ -416,13 +416,13 @@ Figure*[fff::figure,src="\this is a side-by-side\"] *) (*<*) -Figure*[ffff::figure2, caption="\this is another 2 side-by-side\"] +Figure*[ffff::float, caption="\this is another 2 side-by-side\"] \@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\ \@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\ (* proposed syntax for sub-figure labels : text\ @{figure "ffff(2)"}\ *) -Figure*[figxxx::figure2,caption="\Proofs establishing an Invariant Preservation.\"] +Figure*[figxxx::float,caption="\Proofs establishing an Invariant Preservation.\"] \@{boxed_theory_text [display] \lemma inv_c2_preserved : "c2_inv \ \ c1_inv (\ \Hardware\\<^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 diff --git a/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy b/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy index 13109d1..b9987c5 100644 --- a/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy +++ b/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy @@ -408,7 +408,7 @@ Figure*[fff::figure,src="\this is a side-by-side\"] *) -Figure*[ffff::figure2, caption="\this is another 2 side-by-side\"] +Figure*[ffff::float, caption="\this is another 2 side-by-side\"] \@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\ \@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\ @@ -416,7 +416,7 @@ Figure*[ffff::figure2, caption="\this is another 2 side-by-side\"] text\ @{figure "ffff(2)"}\ *) -Figure*[figxxx::figure2,caption="\Proofs establishing an Invariant Preservation.\"] +Figure*[figxxx::float,caption="\Proofs establishing an Invariant Preservation.\"] \@{boxed_theory_text [display] \lemma inv_c2_preserved : "c2_inv \ \ c1_inv (\ \Hardware\\<^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 diff --git a/Isabelle_DOF/latex/styles/DOF-COL.sty b/Isabelle_DOF/latex/styles/DOF-COL.sty index 3b08c7c..d42c244 100644 --- a/Isabelle_DOF/latex/styles/DOF-COL.sty +++ b/Isabelle_DOF/latex/styles/DOF-COL.sty @@ -48,18 +48,18 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: figure2* -\NewEnviron{isamarkupfigureTWO*}[1][]{\isaDof[env={figureTWO},#1]{\BODY}} -\newisadof{IsaUNDERSCORECOLDOTfigureTWO}% +\NewEnviron{isamarkupfloat*}[1][]{\isaDof[env={float},#1]{\BODY}} +\newisadof{IsaUNDERSCORECOLDOTfloat}% [label=,type=% ,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=% ,IsaUNDERSCORECOLDOTfigureDOTplacement=% ,IsaUNDERSCORECOLDOTfigureDOTsrc=% -,IsaUNDERSCORECOLDOTfigureTWODOTcaption=% +,IsaUNDERSCORECOLDOTfloatDOTcaption=% ,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True% ][1]{% \begin{figure}[] #1 - \caption{\commandkey{IsaUNDERSCORECOLDOTfigureTWODOTcaption}} + \caption{\commandkey{IsaUNDERSCORECOLDOTfloatDOTcaption}} \label{\commandkey{label}}% \end{figure} } diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 050f468..6416247 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -158,14 +158,13 @@ ML\ "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_class print_doc_classes - doc_class figure = relative_width :: "int" (* percent of textwidth *) src :: "string" placement :: placement spawn_columns :: bool <= True -doc_class figure2 = figure + +doc_class float = figure + caption :: string