From 8bdd40fc20bdd6c69dc10e30661beddef736f91e Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Thu, 11 May 2023 16:21:37 +0200 Subject: [PATCH 01/16] basic problems on multiple subfloats content solved --- .../root-sn-article-UNSUPPORTED.tex | 4 - .../root-svjour3-UNSUPPORTED.tex | 4 - Isabelle_DOF-Unit-Tests/COL_Test.thy | 23 ++--- Isabelle_DOF-Unit-Tests/Latex_Tests.thy | 8 +- .../latex/document-templates/root-lncs.tex | 4 +- .../document-templates/root-scrartcl.tex | 2 +- .../root-scrreprt-modern.tex | 4 +- .../document-templates/root-scrreprt.tex | 4 +- Isabelle_DOF/latex/styles/DOF-COL.sty | 11 +-- Isabelle_DOF/thys/Isa_COL.thy | 94 ++++++++++--------- 10 files changed, 70 insertions(+), 88 deletions(-) diff --git a/Isabelle_DOF-Ontologies/document-templates/root-sn-article-UNSUPPORTED.tex b/Isabelle_DOF-Ontologies/document-templates/root-sn-article-UNSUPPORTED.tex index 891fe196..e8df544e 100644 --- a/Isabelle_DOF-Ontologies/document-templates/root-sn-article-UNSUPPORTED.tex +++ b/Isabelle_DOF-Ontologies/document-templates/root-sn-article-UNSUPPORTED.tex @@ -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 diff --git a/Isabelle_DOF-Ontologies/document-templates/root-svjour3-UNSUPPORTED.tex b/Isabelle_DOF-Ontologies/document-templates/root-svjour3-UNSUPPORTED.tex index 5d554f90..8ee88a33 100644 --- a/Isabelle_DOF-Ontologies/document-templates/root-svjour3-UNSUPPORTED.tex +++ b/Isabelle_DOF-Ontologies/document-templates/root-svjour3-UNSUPPORTED.tex @@ -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 diff --git a/Isabelle_DOF-Unit-Tests/COL_Test.thy b/Isabelle_DOF-Unit-Tests/COL_Test.thy index 9d53e2d6..a70f58d8 100644 --- a/Isabelle_DOF-Unit-Tests/COL_Test.thy +++ b/Isabelle_DOF-Unit-Tests/COL_Test.thy @@ -28,7 +28,7 @@ text*[S5'::"paragraph"]\Paragraph\ section\General Figure COL Elements\ -figure*[fig1_test::figure,spawn_columns=False,relative_width="95",src="''figures/A''"] +figure*[fig1_test::figure,relative_width="95",src="''figures/A''"] \ This is the label text \<^term>\\\<^sub>i+2\ \ text*[fig2_test::figure, spawn_columns=False, relative_width="95",src="''figures/A''" @@ -65,22 +65,15 @@ text\check @{side_by_side_figure sbsfig1} cmp to @{side_by_side_figure sbs (* And a side-chick ... *) text*[inlinefig::float, - caption="\The Caption.\"] -\@{theory_text [display, margin = 5] \lemma A :: "a \ b"\}\ + main_caption="\The Caption.\"] + \@{theory_text [display, margin = 5] \lemma A :: "a \ b"\}\ -text*[fffff::float]\ @{fig_content [display] (scale = 80, width=80, caption=\this is \<^term>\\\<^sub>i+2\ \) - \figures/A.png\}\ +text*[dupl_graphics::float, + main_caption="\The Caption.\"]\ + @{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>\\\<^sub>i + 1\ test") "figures/B.png"} +\ -(*<*) -text*[inlinegraph::float, - caption="\Another \\<^sub>i+2 Caption.\"] - \@{fig_content [display] (scale = 80, width=80, caption=\This is \<^term>\\\<^sub>i+2\ \) - \figures/A.png\}\ -(*>*) - - - -(*<*) end (*>*) diff --git a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy index 2d0ba44f..48b8e67e 100644 --- a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy +++ b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy @@ -418,16 +418,16 @@ Figure*[fff::figure,src="\this is a side-by-side\"] (*<*) -text-latex\ - @{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>\\\<^sub>i + 1\ test") "figures/A.png"} +Figure*[figxxx::float,main_caption="\Proofs establishing an Invariant Preservation.\"] +\ @{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>\\\<^sub>i + 1\ test") "figures/A.png"} \ (* proposed syntax for sub-figure labels : text\ @{figure "ffff(2)"}\ *) -Figure*[figxxx::float,caption="\Proofs establishing an Invariant Preservation.\"] +Figure*[figxxxx::float,main_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/document-templates/root-lncs.tex b/Isabelle_DOF/latex/document-templates/root-lncs.tex index f6ca007c..c2827a02 100644 --- a/Isabelle_DOF/latex/document-templates/root-lncs.tex +++ b/Isabelle_DOF/latex/document-templates/root-lncs.tex @@ -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} diff --git a/Isabelle_DOF/latex/document-templates/root-scrartcl.tex b/Isabelle_DOF/latex/document-templates/root-scrartcl.tex index 237afdae..8b225df0 100644 --- a/Isabelle_DOF/latex/document-templates/root-scrartcl.tex +++ b/Isabelle_DOF/latex/document-templates/root-scrartcl.tex @@ -26,7 +26,7 @@ \usepackage{textcomp} \bibliographystyle{abbrvnat} -\RequirePackage[caption]{subfig} +\RequirePackage{subcaption} \usepackage[numbers, sort&compress, sectionbib]{natbib} diff --git a/Isabelle_DOF/latex/document-templates/root-scrreprt-modern.tex b/Isabelle_DOF/latex/document-templates/root-scrreprt-modern.tex index 795836e8..adf8d49d 100644 --- a/Isabelle_DOF/latex/document-templates/root-scrreprt-modern.tex +++ b/Isabelle_DOF/latex/document-templates/root-scrreprt-modern.tex @@ -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 diff --git a/Isabelle_DOF/latex/document-templates/root-scrreprt.tex b/Isabelle_DOF/latex/document-templates/root-scrreprt.tex index 5f5958cb..f23aa9bf 100644 --- a/Isabelle_DOF/latex/document-templates/root-scrreprt.tex +++ b/Isabelle_DOF/latex/document-templates/root-scrreprt.tex @@ -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}} diff --git a/Isabelle_DOF/latex/styles/DOF-COL.sty b/Isabelle_DOF/latex/styles/DOF-COL.sty index bc75e9dd..a8ae7307 100644 --- a/Isabelle_DOF/latex/styles/DOF-COL.sty +++ b/Isabelle_DOF/latex/styles/DOF-COL.sty @@ -51,15 +51,14 @@ \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}[] #1 - \caption{\commandkey{IsaUNDERSCORECOLDOTfloatDOTcaption}} + \caption{\commandkey{IsaUNDERSCORECOLDOTfloatDOTmainUNDERSCOREcaption}} \label{\commandkey{label}}% \end{figure} } diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 6ffb439e..a28ec3b6 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -147,25 +147,24 @@ end section\ Library of Standard Text Ontology \ -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\ "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context> |> Name_Space.space_of_table)\ -print_doc_classes +datatype float_kind = listing | table | graphics -doc_class figure = - relative_width :: "int" (* percent of textwidth *) - src :: "string" - placement :: placement +doc_class float = + placement :: "placement list" + kind :: float_kind spawn_columns :: bool <= True + main_caption :: string -doc_class float = figure + - caption :: string +doc_class figure = float + + kind :: float_kind + src :: string + relative_width :: int (* to be deleted *) + invariant fig_kind :: "kind \ = graphics" doc_class side_by_side_figure = figure + @@ -225,7 +224,7 @@ end\ setup\ DOF_lib.define_macro \<^binding>\vs\ "\\vspace{" "}" (check_latex_measure) \ setup\ DOF_lib.define_macro \<^binding>\hs\ "\\hspace{" "}" (check_latex_measure) \ - +define_shortcut* hfill \ \\hfill\ (*<*) text\Tests: \<^vs>\-0.14cm\\ @@ -266,29 +265,29 @@ text\The intermediate development goal is to separate the ontological, top \<^emph>\import\ of a figure. The hope is that this opens the way for more orthogonality and abstraction from the LaTeX engine. \ - -ML\ +ML\XML.enclose\ +ML\ 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_scale 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,7 +296,7 @@ fun fig_content_modes (ctxt, toks) = (Parse.list1 ( (Args.$$$ widthN |-- Args.$$$ "=" -- Parse.int >> (fn (_, k) => upd_relative_width k)) - || (Args.$$$ scaleN |-- Args.$$$ "=" -- Parse.int + || (Args.$$$ heightN |-- Args.$$$ "=" -- Parse.int >> (fn (_, k) => upd_scale k)) || (Args.$$$ captionN |-- Args.$$$ "=" -- Parse.document_source >> (fn (_, k) => upd_caption k)) @@ -335,31 +334,41 @@ fun fig_content_antiquotation name scan = (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.") + 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_s = if relative_width = 100 then "" - else "width="^Real.toString((Real.fromInt relative_width) + val wdth_val_s = 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 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 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 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) + 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" cap_txt')) + |> (Latex.environment ("subcaptionblock") ) +(* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *) end ) )); - + +val t = Latex.macro val _ = fig_content_antiquotation : binding -> ((fig_content -> fig_content) * Input.source) context_parser @@ -371,7 +380,7 @@ val _ = Theory.setup \ - +ML\\ ML\ val _ = Path.parent val mdir = Resources.master_directory @{theory} @@ -673,7 +682,7 @@ declare[[tab_cell_placing="left",tab_cell_height="18.0cm"]] section\Tests\ (*<*) -text\ @{fig_content [display] (scale = 80, width=80, caption=\this is \<^term>\\\<^sub>i+2\ \\) +text\ @{fig_content [display] (height = 80, width=80, caption=\this is \<^term>\\\<^sub>i+2\ \\) \figures/isabelle-architecture.pdf\}\ text\ @{table_inline [display] (cell_placing = center,cell_height =\12.0cm\, cell_height =\13pt\, cell_width = \12.0cm\, @@ -685,11 +694,6 @@ text\ @{table_inline [display] (cell_placing = center,cell_height =\*) -ML\@{term "side_by_side_figure"}; - @{typ "doc_class rexp"}; - DOF_core.SPY; - -\ text\@{term_ \3 + 4::int\} @{value_ \3 + 4::int\} \ end From 7e01b7de97d399a080b1d06a4dbde143f1a9c64f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 11 May 2023 18:18:40 +0200 Subject: [PATCH 02/16] Implement long names for classes term-antiquotataions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Examples with value* that now work: value*‹@{scholarly-paper.author ‹church'›}› value*‹@{author ‹church›}› value*‹@{Concept-High-Level-Invariants.author ‹church›}› value*‹@{scholarly-paper.author-instances}› value*‹@{author-instances}› value*‹@{Concept-High-Level-Invariants.author-instances}› --- .../Concept_High_Level_Invariants.thy | 45 ++++-- .../Concept_MonitorTest2.thy | 5 +- .../Concept_TermEvaluation.thy | 8 +- Isabelle_DOF/thys/Isa_DOF.thy | 135 +++++++++++------- 4 files changed, 120 insertions(+), 73 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy b/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy index 9f8b9d3b..6d0d8873 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy @@ -131,7 +131,7 @@ text\Now assume the following ontology:\ 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 \)" and force_level :: "(level \) \ None \ the (level \) > 1" -doc_class claim = Introduction + +doc_class claim = introduction + based_on :: "notion list" doc_class technical = text_section + @@ -181,7 +181,10 @@ text\Next we define some instances (docitems): \ declare[[invariants_checking_with_tactics = true]] -text*[church::Author, email="\church@lambda.org\"]\\ +text*[church::author, email="\church@lambda.org\"]\\ + +text\We can also reference instances of classes defined in parent theories:\ +text*[church'::scholarly_paper.author, email="\church'@lambda.org\"]\\ text*[resultProof::result, evidence = "proof", property="[@{thm \HOL.refl\}]"]\\ text*[resultArgument::result, evidence = "argument"]\\ @@ -193,29 +196,41 @@ text\The invariants \<^theory_text>\author_finite\ and \<^the declare[[invariants_checking_with_tactics = true]] -text*[curry::Author, email="\curry@lambda.org\"]\\ -text*[introduction2::Introduction, authored_by = "{@{Author \church\}}", level = "Some 2"]\\ +text*[curry::author, email="\curry@lambda.org\"]\\ + +text*[introduction2::introduction, authored_by = "{@{author \church\}}", level = "Some 2"]\\ (* When not commented, should violated the invariant: update_instance*[introduction2::Introduction , authored_by := "{@{Author \church\}}" , level := "Some 1"] *) +text\Use of the instance @{docitem_name "church'"} + to instantiate a \<^doc_class>\scholarly_paper.introduction\ class:\ +text*[introduction2'::scholarly_paper.introduction, + main_author = "Some @{scholarly-paper.author \church'\}", level = "Some 2"]\\ +value*\@{scholarly-paper.author \church'\}\ +value*\@{author \church\}\ +value*\@{Concept-High-Level-Invariants.author \church\}\ -text*[introduction3::Introduction, authored_by = "{@{Author \church\}}", level = "Some 2"]\\ -text*[introduction4::Introduction, authored_by = "{@{Author \curry\}}", level = "Some 4"]\\ +value*\@{scholarly-paper.author-instances}\ +value*\@{author-instances}\ +value*\@{Concept-High-Level-Invariants.author-instances}\ + +text*[introduction3::introduction, authored_by = "{@{author \church\}}", level = "Some 2"]\\ +text*[introduction4::introduction, authored_by = "{@{author \curry\}}", level = "Some 4"]\\ text*[resultProof2::result, evidence = "proof", property="[@{thm \HOL.sym\}]"]\\ text\Then we can evaluate expressions with instances:\ -term*\authored_by @{Introduction \introduction2\} = authored_by @{Introduction \introduction3\}\ -value*\authored_by @{Introduction \introduction2\} = authored_by @{Introduction \introduction3\}\ -value*\authored_by @{Introduction \introduction2\} = authored_by @{Introduction \introduction4\}\ +term*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction3\}\ +value*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction3\}\ +value*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction4\}\ -value*\@{Introduction \introduction2\}\ +value*\@{introduction \introduction2\}\ -value*\{@{Author \curry\}} = {@{Author \church\}}\ +value*\{@{author \curry\}} = {@{author \church\}}\ term*\property @{result \resultProof\} = property @{result \resultProof2\}\ value*\property @{result \resultProof\} = property @{result \resultProof2\}\ diff --git a/Isabelle_DOF-Unit-Tests/Concept_MonitorTest2.thy b/Isabelle_DOF-Unit-Tests/Concept_MonitorTest2.thy index afcb77d5..9ceae776 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_MonitorTest2.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_MonitorTest2.thy @@ -22,9 +22,12 @@ begin section\Test Purpose.\ text\ Creation of document parts that are controlled by (nested, locally defined) monitors. \ +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 = diff --git a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy index 1a8e543b..969586b2 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy @@ -200,10 +200,10 @@ Consequently, it has the same limitations as \<^emph>\value*\. text\Using the ontology defined in \<^theory>\Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\ we can check logical statements:\ -term*\authored_by @{Introduction \introduction2\} = authored_by @{Introduction \introduction3\}\ -assert*\authored_by @{Introduction \introduction2\} = authored_by @{Introduction \introduction3\}\ -assert*\\(authored_by @{Introduction \introduction2\} - = authored_by @{Introduction \introduction4\})\ +term*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction3\}\ +assert*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction3\}\ +assert*\\(authored_by @{introduction \introduction2\} + = authored_by @{introduction \introduction4\})\ text\Assertions must be boolean expressions, so the following assertion triggers an error:\ (* Error: diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 26314515..a95d1061 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -806,24 +806,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 +833,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 *) @@ -1115,19 +1113,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 +1149,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 +1163,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 +1190,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>\string\ --> 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>\list class_typ\, Mixfix.mixfix mixfix)] + |> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list) + |> DOF_core.make_isa_transformer) + |> Sign.add_consts [(bind', \<^Type>\list class_typ\, 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 = @@ -2952,6 +2980,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 +3037,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; From bdc8477f388f1da03d6a1b506fe9411e4533a3e1 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Fri, 12 May 2023 09:42:52 +0200 Subject: [PATCH 03/16] Code Cleanup --- Isabelle_DOF/thys/Isa_COL.thy | 33 +++++++-------------------------- 1 file changed, 7 insertions(+), 26 deletions(-) diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index a28ec3b6..bf4e0a31 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -328,13 +328,8 @@ 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 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,relative_height,caption} = cfg_trans mt_fig_content +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) @@ -365,14 +360,12 @@ fun fig_content_antiquotation name scan = |> (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) + (fig_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text)); -val t = Latex.macro -val _ = fig_content_antiquotation - : binding - -> ((fig_content -> fig_content) * Input.source) context_parser - -> theory -> theory val _ = Theory.setup ( fig_content_antiquotation \<^binding>\fig_content\ @@ -380,18 +373,7 @@ val _ = Theory.setup \ -ML\\ ML\ -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) - - -val ppp = (Path.explode "document") fun get_session_dir ctxt path = Resources.check_session_dir ctxt @@ -406,7 +388,6 @@ 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; -get_document_dir @{context} \ subsection\Tables\ (* TODO ! ! ! *) From 514ebee17c61e8751ac64ea64e7e9a8b54eafe24 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Fri, 12 May 2023 15:11:37 +0200 Subject: [PATCH 04/16] pass on new figure implemntation --- .../Conceptual/Conceptual.thy | 3 +- Isabelle_DOF-Unit-Tests/COL_Test.thy | 38 ++---- Isabelle_DOF/thys/Isa_COL.thy | 111 ++++++++++++------ Isabelle_DOF/thys/Isa_DOF.thy | 24 +++- .../thys/manual/M_01_Introduction.thy | 1 + Isabelle_DOF/thys/manual/M_02_Background.thy | 34 +++--- Isabelle_DOF/thys/manual/M_03_GuidedTour.thy | 50 ++++---- 7 files changed, 149 insertions(+), 112 deletions(-) diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index 76522e12..3e499224 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -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"] diff --git a/Isabelle_DOF-Unit-Tests/COL_Test.thy b/Isabelle_DOF-Unit-Tests/COL_Test.thy index a70f58d8..c04d40e4 100644 --- a/Isabelle_DOF-Unit-Tests/COL_Test.thy +++ b/Isabelle_DOF-Unit-Tests/COL_Test.thy @@ -28,39 +28,15 @@ text*[S5'::"paragraph"]\Paragraph\ section\General Figure COL Elements\ -figure*[fig1_test::figure,relative_width="95",src="''figures/A''"] +figure*[fig1_test::figure,relative_width="95",file_src="''figures/A.png''"] \ This is the label text \<^term>\\\<^sub>i+2\ \ -text*[fig2_test::figure, spawn_columns=False, relative_width="95",src="''figures/A''" +text*[fig2_test::figure, spawn_columns=False, relative_width="95",file_src="''figures/A.png''" ]\ This is the label text\ -text\check @{figure fig1_test} cmp to @{figure fig2_test}\ - -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''"]\ Exploring text elements. \ +text\check @{figure [display] fig1_test} cmp to @{figure fig2_test}\ -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''"]\The global caption\ - -text\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} - \ (* And a side-chick ... *) @@ -69,11 +45,13 @@ text*[inlinefig::float, \@{theory_text [display, margin = 5] \lemma A :: "a \ b"\}\ text*[dupl_graphics::float, - main_caption="\The Caption.\"]\ - @{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>\\\<^sub>i + 1\ test") "figures/B.png"} + main_caption="\The Caption.\"] +\ +@{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>\\\<^sub>i + 1\ test") "figures/B.png"} \ + end (*>*) diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index bf4e0a31..dcfeef6b 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -141,10 +141,12 @@ val _ = heading_command \<^command_keyword>\subsection*\ "subsectio val _ = heading_command \<^command_keyword>\subsubsection*\ "subsubsection heading" (SOME (SOME 3)); val _ = heading_command \<^command_keyword>\paragraph*\ "paragraph" (SOME (SOME 4)); + end end \ + section\ Library of Standard Text Ontology \ datatype placement = here | top | bottom @@ -154,19 +156,26 @@ ML\ "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_class datatype float_kind = listing | table | graphics -doc_class float = - placement :: "placement list" - kind :: float_kind - spawn_columns :: bool <= True - main_caption :: string +doc_class float = + placement :: "placement list" + kind :: float_kind + spawn_columns :: bool <= True + main_caption :: string <= "''''" -doc_class figure = float + - kind :: float_kind - src :: string - relative_width :: int (* to be deleted *) - invariant fig_kind :: "kind \ = graphics" +doc_class figure = float + + kind :: float_kind <= graphics + file_src :: string + relative_width :: int + relative_height :: int + invariant fig_kind :: "kind \ = graphics" +doc_class listing = float + + kind :: float_kind + invariant fig_kind' :: "kind \ = float_kind.listing" + + +(* obsolete *) doc_class side_by_side_figure = figure + anchor :: "string" caption :: "string" @@ -237,17 +246,6 @@ define_macro* hs2 \ \\hspace{\ _ \}\Figures\ -ML\open Args\ - -ML\ -(* *********************************************************************** *) -(* Ontological Macro Command Support *) -(* *********************************************************************** *) - -val _ = Onto_Macros.heading_command \<^command_keyword>\figure*\ "figure" NONE; -val _ = Onto_Macros.heading_command \<^command_keyword>\side_by_side_figure*\ "multiple figures" NONE; -\ - (*<*) ML\ @@ -265,7 +263,6 @@ text\The intermediate development goal is to separate the ontological, top \<^emph>\import\ of a figure. The hope is that this opens the way for more orthogonality and abstraction from the LaTeX engine. \ -ML\XML.enclose\ ML\ type fig_content = {relative_width : int, (* percent of textwidth, default 100 *) @@ -279,7 +276,7 @@ val mt_fig_content = {relative_width = 100, 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,relative_height,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,relative_height,caption} : fig_content = @@ -297,7 +294,7 @@ fun fig_content_modes (ctxt, toks) = ( (Args.$$$ widthN |-- Args.$$$ "=" -- Parse.int >> (fn (_, k) => upd_relative_width k)) || (Args.$$$ heightN |-- Args.$$$ "=" -- Parse.int - >> (fn (_, k) => upd_scale k)) + >> (fn (_, k) => upd_relative_height k)) || (Args.$$$ captionN |-- Args.$$$ "=" -- Parse.document_source >> (fn (_, k) => upd_caption k)) ))) [K mt_fig_content]) @@ -373,22 +370,66 @@ val _ = Theory.setup \ + ML\ -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) +(* +type fig_content = {relative_width : int, (* percent of textwidth, default 100 *) + relative_height : int, (* percent, default 100 *) + caption : Input.source (* default empty *)} -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; +*) +val SPY = Unsynchronized.ref("") + +(* ML\snd(HOLogic.dest_number(Syntax.read_term @{context} (!SPY)))\ + *) +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 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 text, + convert_src_from_margs margs) + in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex + end \ + + +ML\ +(* *********************************************************************** *) +(* Ontological Macro Command Support *) +(* *********************************************************************** *) + +float_command \<^command_keyword>\figure*\ "figure" "Isa_COL.figure" ; +val _ = Onto_Macros.heading_command \<^command_keyword>\side_by_side_figure*\ "multiple figures" NONE; +\ + subsection\Tables\ (* TODO ! ! ! *) (* dito the future monitor: table - block *) diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 26314515..594de4b9 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -2172,16 +2172,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 *) diff --git a/Isabelle_DOF/thys/manual/M_01_Introduction.thy b/Isabelle_DOF/thys/manual/M_01_Introduction.thy index cbd42314..49bd081f 100644 --- a/Isabelle_DOF/thys/manual/M_01_Introduction.thy +++ b/Isabelle_DOF/thys/manual/M_01_Introduction.thy @@ -17,6 +17,7 @@ theory "M_01_Introduction" begin (*>*) + chapter*[intro::introduction]\ Introduction \ text*[introtext::introduction]\ The linking of the \<^emph>\formal\ to the \<^emph>\informal\ is perhaps the most pervasive challenge in the diff --git a/Isabelle_DOF/thys/manual/M_02_Background.thy b/Isabelle_DOF/thys/manual/M_02_Background.thy index 86af4e4d..dfe91bdb 100644 --- a/Isabelle_DOF/thys/manual/M_02_Background.thy +++ b/Isabelle_DOF/thys/manual/M_02_Background.thy @@ -20,7 +20,7 @@ begin chapter*[background::text_section]\ Background\ section*[bgrnd1::introduction]\The Isabelle System Architecture\ -figure*[architecture::figure,relative_width="95",src="''figures/isabelle-architecture''"]\ +figure*[architecture::figure,relative_width="95",file_src="''figures/isabelle-architecture.pdf''"]\ The system architecture of Isabelle (left-hand side) and the asynchronous communication between the Isabelle system and the IDE (right-hand side). \ @@ -45,7 +45,7 @@ The current system framework offers moreover the following features: the most prominent and deeply integrated system component. \ text\ -The Isabelle system architecture shown in @{docitem \architecture\} comes with many layers, +The Isabelle system architecture shown in @{figure \architecture\} comes with many layers, with Standard ML (SML) at the bottom layer as implementation language. The architecture actually foresees a \<^emph>\Nano-Kernel\ (our terminology) which resides in the SML structure \<^boxed_sml>\Context\. This structure provides a kind of container called \<^emph>\context\ providing an identity, an @@ -102,17 +102,18 @@ text\ \<^boxed_theory_text>\keywords\ are used to separate commands from each other. \ -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''"]\A Representation of a Document Model.\ +text*[docModGenConcr::float, + main_caption="\A Representation of a Document Model.\"] +\ +@{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"} +\ text\The body of a theory file consists of a sequence of \<^emph>\commands\ that must be introduced by a command keyword such as \<^boxed_theory_text>\requirement\ 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)). \ +code and text-elements (see @{float "docModGenConcr"}(right)). \ text\ A simple text-element \<^index>\text-element\ may look like this: @@ -182,17 +183,18 @@ text\Antiquotations seen as semantic macros are partial functions of type typeset. They represent the device for linking formal with the informal content. \ -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''"]\Documents conform to Ontologies.\ +text*[docModOnto::float, + main_caption="\Documents conform to Ontologies.\"] +\ +@{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"} +\ text\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>\ODL\ that \<^emph>\generates\ 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.\ section*[bgrnd21::introduction]\Implementability of the Document Model in other ITP's\ @@ -207,13 +209,13 @@ text\ in many features over-accomplishes the required features of \<^dof>. \ -figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\ +figure*["fig:dof-ide",relative_width="95",file_src="''figures/cicm2018-combined.png''"]\ The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page of~@{cite "brucker.ea:isabelle-ontologies:2018"}.\ text\ We call the present implementation of \<^dof> on the Isabelle platform \<^isadof> . - @{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. diff --git a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy index 6b84db9f..59718001 100644 --- a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy +++ b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy @@ -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. \ -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''"] \ A mathematics paper as integrated document source ... \ -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''"] \ ... and as corresponding \<^pdf>-output. \ text\The integrated source of this paper-excerpt is shown in \<^figure>\fig0\, while the @@ -382,7 +382,7 @@ standard inductive \<^theory_text>\datatype\ definition mechanism i for attribute declarations. Vice-versa, document class definitions imply a corresponding HOL type definition. \ -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''"] \ A screenshot of the integrated source with definitions ...\ text\An example for a sequence of (Isabelle-formula-)texts, their ontological declarations as \<^typ>\definition\s in terms of the \<^verbatim>\scholarly_paper\-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. \ -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''"] \ ... and the corresponding \<^pdf>-output.\ text\ @@ -431,7 +431,7 @@ doc_class figure = text_section + spawn_columns :: bool <= True \} \ -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''"] \ Declaring figures in the integrated source.\ text\ @@ -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>\article\. \ +text*[exploring::float, + main_caption="\Exploring text elements.\"] +\ +@{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"} +\ -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''"]\Exploring text elements.\ - - -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''"]\Navigation via generated hyperlinks.\ +text*[hyperlinks::float, + main_caption="\Navigation via generated hyperlinks.\"] +\ +@{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"} +\ text\ 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. \ -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''"] \Exploring an ontological reference.\ text\ @@ -533,7 +531,7 @@ ontologically checked prior arguments \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. \ -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''"] \Term-Antiquotations Referencing to Annotated Elements\ text\As shown in @{figure \doc_termAq\}, this feature of \<^isadof> substantially increases the expressibility of links between the formal and the informal in \<^dof> documents.\ @@ -639,7 +637,7 @@ So its value is that readers can just reuse some of these snippets and adapt the purposes. \ -figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabelle.png''"] +figure*[strict_SS::figure, relative_width="95", file_src="''figures/MyCommentedIsabelle.png''"] \A table with a number of SML functions, together with their type.\ text\ From f7141f0df8a9506fe96a6d66ceaf7f0e639713dd Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Fri, 12 May 2023 16:19:14 +0200 Subject: [PATCH 05/16] debugging the LaTeX generation for COL --- Isabelle_DOF-Unit-Tests/COL_Test.thy | 2 +- .../figures/isabelle-architecture.pdf | Bin 35434 -> 36026 bytes Isabelle_DOF/thys/Isa_COL.thy | 28 +++++++++++------- 3 files changed, 19 insertions(+), 11 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/COL_Test.thy b/Isabelle_DOF-Unit-Tests/COL_Test.thy index c04d40e4..44a38a4c 100644 --- a/Isabelle_DOF-Unit-Tests/COL_Test.thy +++ b/Isabelle_DOF-Unit-Tests/COL_Test.thy @@ -34,7 +34,7 @@ figure*[fig1_test::figure,relative_width="95",file_src="''figures/A.png''"] text*[fig2_test::figure, spawn_columns=False, relative_width="95",file_src="''figures/A.png''" ]\ This is the label text\ -text\check @{figure [display] fig1_test} cmp to @{figure fig2_test}\ +text\check @{figure fig1_test} cmp to @{figure fig2_test}\ diff --git a/Isabelle_DOF/document/figures/isabelle-architecture.pdf b/Isabelle_DOF/document/figures/isabelle-architecture.pdf index 6082333781c05595fa0bfb847291a6a27950194f..826297f002c5911f196fd24c02c798156c54a24e 100644 GIT binary patch delta 480 zcmYL`&1%~~6onzHGP`WrEKe7qHU!U~MwWsw*pVH)C`s**MUoPPJqDLXBSs_VXA|6I zw(6#D(RCgo50a1(lRJ+}1T8zZrYevmp3Fg0y;(2x?05uvc3)`F z7SlPQXEw{rqN%&M2PIQDTWJgisBgEQA8)e7$sFg}mTQxP%bx6UTy?UmuD?gs`sWft zjQf2Na@HijRhe}UI87&Sg6`Y_hDD+Cz8e(KKS(^A?$x3R7xtWKm>T3mnx8c?k13f#PK@_MO5!TecVh_Tqc7g z9LF(Fr5X-nF&YJGJPhJgh=`^AqcC7{@MgO)&hLS>PR`d4UOD65eXBQ+Qi=d{ny(Ce aqh>AMEK)i@_?^`&B2~mAvcEq*nUH^Dr-Bmz delta 9 Qcmdlrlj+qIrVUwL02e<5dH?_b diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index dcfeef6b..878b3838 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -325,6 +325,15 @@ 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.") @@ -335,12 +344,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) = else "height="^Real.toString((Real.fromInt relative_height) / (Real.fromInt 100)) ^"\\textheight" val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_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 + 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 @@ -353,7 +357,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) = |> (fn X => (Latex.string ("{"^wdth_val_s^"}")) @ (Latex.string "\\centering") @ (XML.enclose ("\\includegraphics"^arg^"{") "}" X) - @ (Latex.macro "caption" cap_txt')) + @ (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 @@ -412,9 +416,13 @@ fun float_command (name, pos) descr cid = {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 text, - convert_src_from_margs margs) + 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 From 33fd1453a02c038dac9702343b626ad4c9c3c909 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Fri, 12 May 2023 17:04:30 +0200 Subject: [PATCH 06/16] Global remove of side-by-side-figures, fixing various bugs - Caveat: no correspondance figure* - class figure. --- Isabelle_DOF-Example-I/IsaDofApplications.thy | 59 ++++++++++--------- Isabelle_DOF-Example-I/document/preamble.tex | 3 - .../CENELEC_50128_Documentation.thy | 6 +- Isabelle_DOF-Unit-Tests/Attributes.thy | 20 +++---- Isabelle_DOF-Unit-Tests/COL_Test.thy | 7 ++- Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy | 4 +- Isabelle_DOF/thys/Isa_COL.thy | 2 +- 7 files changed, 51 insertions(+), 50 deletions(-) diff --git a/Isabelle_DOF-Example-I/IsaDofApplications.thy b/Isabelle_DOF-Example-I/IsaDofApplications.thy index a842e3ca..e354adfa 100644 --- a/Isabelle_DOF-Example-I/IsaDofApplications.thy +++ b/Isabelle_DOF-Example-I/IsaDofApplications.thy @@ -206,7 +206,7 @@ The current system framework offers moreover the following features: the most prominent and deeply integrated system component. \ -figure*[architecture::figure,relative_width="100",src="''figures/isabelle-architecture''"]\ +figure*[architecture::figure,relative_width="100",file_src="''figures/isabelle-architecture.pdf''"]\ The system architecture of Isabelle (left-hand side) and the asynchronous communication between the Isabelle system and the IDE (right-hand side). \ @@ -315,7 +315,7 @@ Isabelle users to Isabelle users only. Of course, such references can be added e represent a particular strength of \<^isadof>.\ text*["paper_onto_core"::float, - caption="\The core of the ontology definition for writing scholarly papers.\"] + main_caption="\The core of the ontology definition for writing scholarly papers.\"] \@{boxed_theory_text [display]\ 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>\-0.8cm\\ -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''"] \ Ouroboros I: This paper from inside \<^dots> \ (*<*)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)\paper_onto_sections\})\ text*["paper_onto_sections"::float, - caption = "''Various types of sections of a scholarly papers.''"]\ + main_caption = "''Various types of sections of a scholarly papers.''"]\ @{boxed_theory_text [display]\ doc_class example = text_section + comment :: string @@ -403,7 +403,7 @@ doc_class bibliography = text\... 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"}).\ text*["paper_onto_monitor"::float, - caption = "''A monitor for the scholarly paper ontology.''"]\ + main_caption = "''A monitor for the scholarly paper ontology.''"]\ @{boxed_theory_text [display]\ 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.\ -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''"] \ Ouroboros II: figures \<^dots> \ text\ The document class \<^theory_text>\figure\ --- 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). \ text*["onto_exam"::float, - caption = "''The core of the ontology modeling math exams.''"]\ + main_caption = "''The core of the ontology modeling math exams.''"]\ @{boxed_theory_text [display]\ doc_class Author = ... datatype Subject = algebra | geometry | statistical @@ -495,7 +495,7 @@ assume familiarity of the students with Isabelle (\<^theory_text>\term\ text*["onto_questions"::float, - caption = "''An exam can contain different types of questions.''"]\ + main_caption = "''An exam can contain different types of questions.''"]\ @{boxed_theory_text [display]\ 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>\intern\, \<^ie>, not exposed to the students but just additional material for the internal review process of the exam.\ text*["onto_exam_monitor"::float, - caption = "''Validating exams.''"]\ + main_caption = "''Validating exams.''"]\ @{boxed_theory_text [display]\ 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. \ -figure*[fig_qcm::figure,spawn_columns=False, - relative_width="90",src="''figures/InteractiveMathSheet''"] - \ A Generated QCM Fragment \<^dots> \ +figure*[fig_qcm::figure, + relative_width="90",file_src="''figures/InteractiveMathSheet.png''"] + \A Generated QCM Fragment \<^dots> \ subsection*[cenelec_onto::example]\ The Certification Scenario following CENELEC \ text\ Documents to be provided in formal certifications (such as CENELEC @@ -583,7 +583,7 @@ text\ 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"}). \ text*["conceptual"::float, - caption = "''Modeling requirements.''"]\ + main_caption = "''Modeling requirements.''"]\ @{boxed_theory_text [display]\ 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>\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''", - 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''"]\ Exploring text elements. \ -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''"]\ Hyperlinks.\ +text*["text-elements"::float, + main_caption="\Exploring text elements.\"] +\ +@{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"} +\ + +text*["hyperlinks"::float, + main_caption="\Hyperlinks.\"] +\ +@{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"} +\ (*<*)declare_reference*["figDogfoodVIlinkappl"::figure](*>*) @@ -661,8 +663,9 @@ antiquotation \<^theory_text>\@{example ...}\ 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. \ -figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"] +figure*[figDogfoodVIlinkappl::figure,relative_width="80",file_src="''figures/Dogfood-V-attribute.png''"] \ Exploring an attribute (hyperlinked to the class). \ + subsection*[cenelec_pide::example]\ CENELEC \ (*<*)declare_reference*[figfig3::figure](*>*) text\ The corresponding view in @{figure (unchecked) \figfig3\} shows core part of a document, @@ -670,7 +673,7 @@ coherent to the @{example \cenelec_onto\}. 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.\ -figure*[figfig3::figure,relative_width="80",src="''figures/antiquotations-PIDE''"] +figure*[figfig3::figure,relative_width="80",file_src="''figures/antiquotations-PIDE.png''"] \ Standard antiquotations referring to theory elements.\ (*<*)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.\ -figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"] +figure*[figfig5::figure, relative_width="80", file_src="''figures/srac-definition.png''"] \ Defining a SRAC reference \<^dots> \ -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''"] \ Using a SRAC as EC document reference. \ text\ Now we reference in @{figure \figfig7\} this safety-related condition; diff --git a/Isabelle_DOF-Example-I/document/preamble.tex b/Isabelle_DOF-Example-I/document/preamble.tex index 489e71b7..c037d319 100644 --- a/Isabelle_DOF-Example-I/document/preamble.tex +++ b/Isabelle_DOF-Example-I/document/preamble.tex @@ -22,9 +22,6 @@ \usepackage{listings} \usepackage{lstisadof-manual} -\usepackage[caption]{subfig} -\usepackage[size=footnotesize]{caption} - \providecommand{\isactrlemph}[1]{\emph{#1}} \usepackage[LNCS, orcidicon, diff --git a/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128_Documentation.thy b/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128_Documentation.thy index b8c5331a..800e081b 100644 --- a/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128_Documentation.thy +++ b/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128_Documentation.thy @@ -194,17 +194,17 @@ result communication times \ldots \ text\Note that this \<^pdf>-output is the result of a specific setup for \<^typ>\SRAC\s.\ subsection*[ontopide::technical]\Editing Support for CENELEC 50128\ -figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"] +figure*[figfig3::figure,relative_width="95",file_src="''figures/antiquotations-PIDE.png''"] \ Standard antiquotations referring to theory elements.\ text\ The corresponding view in @{docitem \figfig3\} shows core part of a document conforming to the \<^verbatim>\CENELEC_50128\ 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.\ -figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"] +figure*[figfig5::figure, relative_width="95", file_src="''figures/srac-definition.png''"] \ Defining a \<^typ>\SRAC\ in the integrated source ... \ -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''"] \ Using a \<^typ>\SRAC\ as \<^typ>\EC\ document element. \ text\ The subsequent sample in @{figure \figfig5\} shows the definition of a \<^emph>\safety-related application condition\, a side-condition of a theorem which diff --git a/Isabelle_DOF-Unit-Tests/Attributes.thy b/Isabelle_DOF-Unit-Tests/Attributes.thy index 031a2fcd..5bada7e7 100644 --- a/Isabelle_DOF-Unit-Tests/Attributes.thy +++ b/Isabelle_DOF-Unit-Tests/Attributes.thy @@ -182,29 +182,29 @@ open_monitor*[figs1::figure_group, caption="''Sample ''"] ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ text*[testFreeA::A]\\ -figure*[fig_A::figure, spawn_columns=False, +figure*[fig_A::figure, relative_width="90", - src="''figures/A.png''"] + file_src="''figures/A.png''"] \ The A train \ldots \ figure*[fig_B::figure, - spawn_columns=False,relative_width="90", - src="''figures/B.png''"] + relative_width="90", + file_src="''figures/B.png''"] \ The B train \ldots \ open_monitor*[figs2::figure_group, caption="''Sample ''"] ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ -figure*[fig_C::figure, spawn_columns=False, +figure*[fig_C::figure, relative_width="90", - src="''figures/A.png''"] + file_src="''figures/A.png''"] \ The C train \ldots \ open_monitor*[figs3::figure_group, caption="''Sample ''"] ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ figure*[fig_D::figure, - spawn_columns=False,relative_width="90", - src="''figures/B.png''"] + relative_width="90", + file_src="''figures/B.png''"] \ The D train \ldots \ close_monitor*[figs3] @@ -216,8 +216,8 @@ text*[testRejected1::figure_group, caption="''document/figures/A.png''"] \ The A train \ldots \ figure*[fig_E::figure, - spawn_columns=False,relative_width="90", - src="''figures/B.png''"] + relative_width="90", + file_src="''figures/B.png''"] \ The E train \ldots \ close_monitor*[figs4] close_monitor*[figs2] diff --git a/Isabelle_DOF-Unit-Tests/COL_Test.thy b/Isabelle_DOF-Unit-Tests/COL_Test.thy index 44a38a4c..9e37dd53 100644 --- a/Isabelle_DOF-Unit-Tests/COL_Test.thy +++ b/Isabelle_DOF-Unit-Tests/COL_Test.thy @@ -28,12 +28,13 @@ text*[S5'::"paragraph"]\Paragraph\ section\General Figure COL Elements\ -figure*[fig1_test::figure,relative_width="95",file_src="''figures/A.png''"] +figure*[fig1_test,relative_width="95",file_src="''figures/A.png''"] \ This is the label text \<^term>\\\<^sub>i+2\ \ -text*[fig2_test::figure, spawn_columns=False, relative_width="95",file_src="''figures/A.png''" +(*<*) +text*[fig2_test::figure, relative_width="95",file_src="''figures/A.png''" ]\ This is the label text\ - +(*>*) text\check @{figure fig1_test} cmp to @{figure fig2_test}\ diff --git a/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy b/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy index b9987c56..511466a7 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::float, caption="\this is another 2 side-by-side\"] +Figure*[ffff::float, main_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::float, caption="\this is another 2 side-by-side\"] text\ @{figure "ffff(2)"}\ *) -Figure*[figxxx::float,caption="\Proofs establishing an Invariant Preservation.\"] +Figure*[figxxx::float,main_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/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 878b3838..5d3b3753 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -159,7 +159,7 @@ datatype float_kind = listing | table | graphics doc_class float = placement :: "placement list" kind :: float_kind - spawn_columns :: bool <= True + spawn_columns :: bool <= False main_caption :: string <= "''''" doc_class figure = float + From e97cca1a2c09cc24416459f6f5e604309a7a4ec4 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Fri, 12 May 2023 17:17:57 +0200 Subject: [PATCH 07/16] reactivated Cenelec_Test --- Isabelle_DOF-Unit-Tests/ROOT | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Isabelle_DOF-Unit-Tests/ROOT b/Isabelle_DOF-Unit-Tests/ROOT index 55922678..9fb90524 100644 --- a/Isabelle_DOF-Unit-Tests/ROOT +++ b/Isabelle_DOF-Unit-Tests/ROOT @@ -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 From fcc25f7450ee255aa5677fb3376e62a204748b52 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Fri, 12 May 2023 17:47:18 +0200 Subject: [PATCH 08/16] Removed implementation of figure* and side_by_side_figure. --- Isabelle_DOF/latex/styles/DOF-COL.sty | 80 +-------------------------- 1 file changed, 1 insertion(+), 79 deletions(-) diff --git a/Isabelle_DOF/latex/styles/DOF-COL.sty b/Isabelle_DOF/latex/styles/DOF-COL.sty index a8ae7307..603a9c38 100644 --- a/Isabelle_DOF/latex/styles/DOF-COL.sty +++ b/Isabelle_DOF/latex/styles/DOF-COL.sty @@ -18,34 +18,6 @@ \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}} @@ -56,7 +28,7 @@ ,IsaUNDERSCORECOLDOTfloatDOTmainUNDERSCOREcaption=% ,IsaUNDERSCORECOLDOTfloatDOTspawnUNDERSCOREcolumns=enum False True% ][1]{% - \begin{figure}[] + \begin{figure} #1 \caption{\commandkey{IsaUNDERSCORECOLDOTfloatDOTmainUNDERSCOREcaption}} \label{\commandkey{label}}% @@ -64,53 +36,3 @@ } % 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* -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% From 6bab138af668c483a8b30a4adbebf8a829ef20ec Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Fri, 12 May 2023 17:50:17 +0200 Subject: [PATCH 09/16] Removed default author. --- Isabelle_DOF/latex/styles/DOF-core.sty | 1 - 1 file changed, 1 deletion(-) diff --git a/Isabelle_DOF/latex/styles/DOF-core.sty b/Isabelle_DOF/latex/styles/DOF-core.sty index f1f81e5e..0bfa98c6 100644 --- a/Isabelle_DOF/latex/styles/DOF-core.sty +++ b/Isabelle_DOF/latex/styles/DOF-core.sty @@ -167,7 +167,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \title{No Title Given} -\author{No Author Given} \input{ontologies} \IfFileExists{preamble.tex}{\input{preamble.tex}}{}% From e9044e8d5a25a0f53b66d47f15d3a2cb73a915fa Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Fri, 12 May 2023 17:50:42 +0200 Subject: [PATCH 10/16] Updating odo --- .../CENELEC_50128/mini_odo/mini_odo.thy | 4 +-- .../TR_MyCommentedIsabelle.thy | 25 ++++++++----------- 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy index f36e0049..0495e106 100644 --- a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy +++ b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy @@ -126,7 +126,7 @@ text\ subsection\Capturing ``System Architecture.''\ -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''"] \An odometer with three sensors \C1\, \C2\, and \C3\.\ text\ @@ -162,7 +162,7 @@ text\ 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"}).\ -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''"] \Real distance vs. discrete distance vs. shaft-encoder sequence\ diff --git a/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index d1702f77..a80b722b 100644 --- a/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -79,7 +79,7 @@ text\ \<^vs>\-0.5cm\ maximum of formal content which makes this text re-checkable at each load and easier maintainable. \ -figure*[architecture::figure,relative_width="70",src="''figures/isabelle-architecture''"]\ +figure*[architecture::figure,relative_width="70",file_src="''figures/isabelle-architecture.pdf''"]\ The system architecture of Isabelle (left-hand side) and the asynchronous communication between the Isabelle system and the IDE (right-hand side). \ @@ -148,7 +148,7 @@ text\ \*\This is a text.\\\ text\and displayed in the Isabelle/jEdit front-end at the sceen by:\ -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''"] \A text-element as presented in Isabelle/jEdit.\ text\The text-commands, ML-commands (and in principle any other command) can be seen as @@ -807,18 +807,13 @@ text\ They reflect the Pure logic depicted in a number of presentations s Notated as logical inference rules, these operations were presented as follows: \ -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''"]\ \ +text*["text-elements"::float, + main_caption="\Kernel Inference Rules.\"] +\ +@{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"} +\ -(* -figure*[kir1::figure,relative_width="100",src="''figures/pure-inferences-I''"] - \ Pure Kernel Inference Rules I.\ -figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"] - \ Pure Kernel Inference Rules II. \ - *) text\Note that the transfer rule: \[ @@ -1440,7 +1435,7 @@ text\The document model forsees a number of text files, which are organize secondary formats can be \<^verbatim>\.sty\,\<^verbatim>\.tex\, \<^verbatim>\.png\, \<^verbatim>\.pdf\, or other files processed by Isabelle and listed in a configuration processed by the build system.\ -figure*[fig3::figure, relative_width="100",src="''figures/document-model''"] +figure*[fig3::figure, relative_width="100",file_src="''figures/document-model.pdf''"] \A Theory-Graph in the Document Model\ text\A \<^verbatim>\.thy\ file consists of a \<^emph>\header\, a \<^emph>\context-definition\ and @@ -1535,7 +1530,7 @@ text\ ... 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. \ -figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"] +figure*[hyplinkout::figure,relative_width="40",file_src="''figures/markup-demo.png''"] \Output with hyperlinked position.\ text\@{figure \hyplinkout\} shows the produced output where the little house-like symbol in the From b8282b771eac788079812286dd55baef4457e6d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 12 May 2023 20:04:44 +0200 Subject: [PATCH 11/16] Cleanup --- Isabelle_DOF-Proofs/Reification_Test.thy | 16 +-- Isabelle_DOF-Proofs/Very_Deep_DOF.thy | 1 - .../Very_Deep_Interpretation.thy | 109 ++---------------- Isabelle_DOF/thys/Isa_DOF.thy | 23 ---- 4 files changed, 20 insertions(+), 129 deletions(-) diff --git a/Isabelle_DOF-Proofs/Reification_Test.thy b/Isabelle_DOF-Proofs/Reification_Test.thy index f4087298..768748e4 100644 --- a/Isabelle_DOF-Proofs/Reification_Test.thy +++ b/Isabelle_DOF-Proofs/Reification_Test.thy @@ -4,10 +4,10 @@ theory Reification_Test begin ML\ -val ty1 = ISA_core.reify_typ @{typ "int"} -val ty2 = ISA_core.reify_typ @{typ "int \ 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 \ bool"} +val ty3 = Meta_ISA_core.reify_typ @{typ "prop"} +val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"} \ term*\@{typ \int\}\ @@ -19,9 +19,9 @@ term*\@{typ \'a list\}\ value*\@{typ \'a list\}\ ML\ -val t1 = ISA_core.reify_term @{term "1::int"} -val t2 = ISA_core.reify_term @{term "\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 "\x. x = 1"} +val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"} \ term*\@{term \1::int\}\ value*\@{term \1::int\}\ @@ -45,7 +45,7 @@ value*\@{thms-of \HOL.refl\}\ ML\ 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 \ diff --git a/Isabelle_DOF-Proofs/Very_Deep_DOF.thy b/Isabelle_DOF-Proofs/Very_Deep_DOF.thy index 73690058..74e9dcb1 100644 --- a/Isabelle_DOF-Proofs/Very_Deep_DOF.thy +++ b/Isabelle_DOF-Proofs/Very_Deep_DOF.thy @@ -15,6 +15,5 @@ term "@{term \\x. P x \ Q\}" term "@{thm \refl\}" term "@{docitem \doc_ref\}" ML\ @{term "@{docitem \doc_ref\}"}\ -(**) end \ No newline at end of file diff --git a/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy b/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy index 2d1e9eae..51ff20a6 100644 --- a/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy +++ b/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy @@ -32,89 +32,9 @@ consts Isabelle_DOF_trace_attribute :: "string \ (string * string) l subsection\ Semantics \ ML\ -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>\fun _ T\ => 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>\Ty\ $ HOLogic.mk_literal s $ HOLogic.mk_list \<^Type>\typ\ (map reify_typ typ_list) | reify_typ (TFree (name, sort)) = @@ -273,16 +188,16 @@ end; (* struct *) \ ML\ -val ty1 = ISA_core.reify_typ @{typ "int"} -val ty2 = ISA_core.reify_typ @{typ "int \ 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 \ bool"} +val ty3 = Meta_ISA_core.reify_typ @{typ "prop"} +val ty4 = Meta_ISA_core.reify_typ @{typ "'a list"} \ ML\ -val t1 = ISA_core.reify_term @{term "1::int"} -val t2 = ISA_core.reify_term @{term "\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 "\x. x = 1"} +val t3 = Meta_ISA_core.reify_term @{term "[2, 3::int]"} \ subsection\ Isar - Setup\ @@ -290,8 +205,8 @@ subsection\ Isar - Setup\ They must be declared in the same theory file as the one of the declaration of Isabelle_DOF term anti-quotations !!! *) setup\ -[(\<^type_name>\thm\, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thm) - , (\<^type_name>\thms_of\, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_thms_of) +[(\<^type_name>\thm\, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thm) + , (\<^type_name>\thms_of\, ISA_core.ML_isa_check_thm, Meta_ISA_core.ML_isa_elaborate_thms_of) , (\<^type_name>\file\, 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>\Isabelle_DOF_typ\, ISA_core.ML_isa_check_typ, ISA_core.ML_isa_elaborate_typ) - ,(\<^const_name>\Isabelle_DOF_term\, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_term) +([(\<^const_name>\Isabelle_DOF_typ\, ISA_core.ML_isa_check_typ, Meta_ISA_core.ML_isa_elaborate_typ) + ,(\<^const_name>\Isabelle_DOF_term\, ISA_core.ML_isa_check_term, Meta_ISA_core.ML_isa_elaborate_term) ,(\<^const_name>\Isabelle_DOF_docitem\, ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic) ,(\<^const_name>\Isabelle_DOF_trace_attribute\, diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index cf2f4a55..ccb47748 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -670,8 +670,6 @@ fun typ_to_cid (Type(s,[\<^Type>\unit\])) = 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) @@ -1064,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: " From 43da6d3197acf0d03439e9e5a038bed5afa153a4 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sat, 13 May 2023 18:20:29 +0200 Subject: [PATCH 12/16] ... --- Isabelle_DOF-Unit-Tests/COL_Test.thy | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/COL_Test.thy b/Isabelle_DOF-Unit-Tests/COL_Test.thy index 9d53e2d6..803d3a4e 100644 --- a/Isabelle_DOF-Unit-Tests/COL_Test.thy +++ b/Isabelle_DOF-Unit-Tests/COL_Test.thy @@ -66,16 +66,15 @@ text\check @{side_by_side_figure sbsfig1} cmp to @{side_by_side_figure sbs text*[inlinefig::float, caption="\The Caption.\"] -\@{theory_text [display, margin = 5] \lemma A :: "a \ b"\}\ + \@{theory_text [display, margin = 5] \lemma A :: "a \ b"\}\ text*[fffff::float]\ @{fig_content [display] (scale = 80, width=80, caption=\this is \<^term>\\\<^sub>i+2\ \) \figures/A.png\}\ - (*<*) text*[inlinegraph::float, caption="\Another \\<^sub>i+2 Caption.\"] - \@{fig_content [display] (scale = 80, width=80, caption=\This is \<^term>\\\<^sub>i+2\ \) + \@{fig_content [display] (scale = 80, width=80, caption=\This is \<^term>\\\<^sub>i+2\ \\) \figures/A.png\}\ (*>*) From d0cd28a45c4921dbd54e88eb34fee9f4c9149144 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sun, 14 May 2023 17:35:00 +0200 Subject: [PATCH 13/16] eliminated side_by_side figure, actualized refman. --- .../Conceptual/Conceptual.thy | 5 +- .../technical_report/technical_report.thy | 2 +- Isabelle_DOF/thys/Isa_COL.thy | 137 ++++++++---------- Isabelle_DOF/thys/manual/M_04_RefMan.thy | 45 +++++- 4 files changed, 98 insertions(+), 91 deletions(-) diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index 3e499224..f6d91728 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -209,9 +209,8 @@ let val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Co "Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M", "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"] + "Isa_COL.paragraph", "Isa_COL.subsection", + "Isa_COL.text_element", "Isa_COL.subsubsection"] val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>)); in @{assert} (class_ids_so_far = docclass_tab) end\ diff --git a/Isabelle_DOF/ontologies/technical_report/technical_report.thy b/Isabelle_DOF/ontologies/technical_report/technical_report.thy index 35715e88..8fb209b5 100644 --- a/Isabelle_DOF/ontologies/technical_report/technical_report.thy +++ b/Isabelle_DOF/ontologies/technical_report/technical_report.thy @@ -75,7 +75,7 @@ doc_class report = abstract ~~ \table_of_contents\ ~~ \introduction\\<^sup>+ ~~ - \technical || figure || side_by_side_figure\\<^sup>+ ~~ + \technical || figure \\<^sup>+ ~~ \conclusion\\<^sup>+ ~~ \index\\<^sup>* ~~ bibliography)" diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 5d3b3753..5b335e29 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -26,7 +26,7 @@ theory Isa_COL keywords "title*" "subtitle*" "chapter*" "section*" "paragraph*" "subsection*" "subsubsection*" - "figure*" "side_by_side_figure*" :: document_body + "figure*" "listing*" :: document_body begin @@ -147,56 +147,6 @@ end \ -section\ Library of Standard Text Ontology \ - -datatype placement = here | top | bottom - -ML\ "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context> - |> Name_Space.space_of_table)\ - -datatype float_kind = listing | table | graphics - -doc_class float = - placement :: "placement list" - kind :: float_kind - spawn_columns :: bool <= False - main_caption :: string <= "''''" - -doc_class figure = float + - kind :: float_kind <= graphics - file_src :: string - relative_width :: int - relative_height :: int - invariant fig_kind :: "kind \ = graphics" - - -doc_class listing = float + - kind :: float_kind - invariant fig_kind' :: "kind \ = float_kind.listing" - - -(* obsolete *) -doc_class side_by_side_figure = figure + - anchor :: "string" - caption :: "string" - relative_width2 :: "int" (* percent of textwidth *) - src2 :: "string" - anchor2 :: "string" - caption2 :: "string" - -print_doc_classes - -doc_class figure_group = - (* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *) - caption :: "string" - rejects figure_group (* this forbids recursive figure-groups not supported - by the current LaTeX style-file. *) - accepts "\figure\\<^sup>+" - -print_doc_classes - - - section\Layout Trimming Commands (with syntactic checks)\ ML\ @@ -244,6 +194,52 @@ define_macro* hs2 \ \\hspace{\ _ \}\*) +define_shortcut* clearpage \ \\clearpage{}\ + hf \ \\hfill\ + br \ \\break\ + + +section\ Library of Standard Figure Ontology \ + +datatype placement = here | top | bottom + +(* +ML\ "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context> + |> Name_Space.space_of_table)\ +*) + +datatype float_kind = listing | table | graphics + +doc_class float = + placement :: "placement list" + kind :: float_kind + spawn_columns :: bool <= False + main_caption :: string <= "''''" + +doc_class figure = float + + kind :: float_kind <= graphics + file_src :: string + relative_width :: int + relative_height :: int + invariant fig_kind :: "kind \ = graphics" + + +doc_class listing = float + + kind :: float_kind + invariant fig_kind' :: "kind \ = float_kind.listing" + + +(* obsolete +doc_class side_by_side_figure = figure + + anchor :: "string" + caption :: "string" + relative_width2 :: "int" (* percent of textwidth *) + src2 :: "string" + anchor2 :: "string" + caption2 :: "string" +*) + + subsection\Figures\ (*<*) @@ -257,11 +253,11 @@ fun setup source = (*>*) -subsubsection\Figure Content\ +subsubsection\The Figure Content Antiquotation\ text\The intermediate development goal is to separate the ontological, top-level construct \figure*\, which will remain a referentiable, ontological document unit, from the more versatile -\<^emph>\import\ of a figure. The hope is that this opens the way for more orthogonality and -abstraction from the LaTeX engine. +\<^emph>\import\ of a figure. This opens the way for more orthogonality and abstraction from the LaTeX +engine. \ ML\ @@ -310,8 +306,6 @@ fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Pat Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)) |> Latex.macro "isatt")); -val SPY = Unsynchronized.ref([XML.Text ""]) - fun get_session_dir ctxt path = Resources.check_session_dir ctxt (SOME (path)) @@ -377,16 +371,7 @@ val _ = Theory.setup ML\ -(* -type fig_content = {relative_width : int, (* percent of textwidth, default 100 *) - relative_height : int, (* percent, default 100 *) - caption : Input.source (* default empty *)} -*) -val SPY = Unsynchronized.ref("") - -(* ML\snd(HOLogic.dest_number(Syntax.read_term @{context} (!SPY)))\ - *) 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." @@ -426,22 +411,18 @@ fun float_command (name, pos) descr cid = in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex end -\ - -ML\ (* *********************************************************************** *) (* Ontological Macro Command Support *) (* *********************************************************************** *) -float_command \<^command_keyword>\figure*\ "figure" "Isa_COL.figure" ; -val _ = Onto_Macros.heading_command \<^command_keyword>\side_by_side_figure*\ "multiple figures" NONE; +val _ = float_command \<^command_keyword>\figure*\ "figure" "Isa_COL.figure" ; +val _ = float_command \<^command_keyword>\listing*\ "figure" "Isa_COL.listing" ; (* Hack ! *) \ + subsection\Tables\ -(* TODO ! ! ! *) -(* dito the future monitor: table - block *) -(* some studies *) +(* Under development *) text\Tables are (sub) document-elements represented inside the documentation antiquotation language. The used technology is similar to the existing railroad-diagram support @@ -701,16 +682,13 @@ val _ = Theory.setup end \ -text\ @{file "../ROOT"} \ -define_shortcut* clearpage \ \\clearpage{}\ - hf \ \\hfill\ - br \ \\break\ +(*<*) + declare[[tab_cell_placing="left",tab_cell_height="18.0cm"]] -section\Tests\ -(*<*) +section\Some Rudimentary Tests\ text\ @{fig_content [display] (height = 80, width=80, caption=\this is \<^term>\\\<^sub>i+2\ \\) \figures/isabelle-architecture.pdf\}\ @@ -725,5 +703,4 @@ text\ @{table_inline [display] (cell_placing = center,cell_height =\*) -text\@{term_ \3 + 4::int\} @{value_ \3 + 4::int\} \ end diff --git a/Isabelle_DOF/thys/manual/M_04_RefMan.thy b/Isabelle_DOF/thys/manual/M_04_RefMan.thy index 521885a5..57f63b08 100644 --- a/Isabelle_DOF/thys/manual/M_04_RefMan.thy +++ b/Isabelle_DOF/thys/manual/M_04_RefMan.thy @@ -659,9 +659,9 @@ text\ .2 Isa\_COL.section. .2 Isa\_COL.subsection. .2 Isa\_COL.subsubsection. -.1 Isa\_COL.figure. -.2 Isa\_COL.side\_by\_side\_figure. -.1 Isa\_COL.figure\_group. +.1 Isa\_COL.float{...}. +.2 Isa\_COL.figure{...}. +.2 Isa\_COL.listing{...}. .1 \ldots. } \end{minipage} @@ -692,9 +692,40 @@ elements such as, \<^ie>, paragraphs (this mirrors restrictions of the target \< The attribute \<^const>\variants\ refers to an Isabelle-configuration attribute that permits to steer the different versions of a \<^LaTeX>-presentation of the integrated source. -For further information of the root classes such as \<^typ>\figure\'s, please consult the ontology in - \<^theory>\Isabelle_DOF.Isa_COL\ directly. \<^verbatim>\COL\ finally provides macros that extend the command-language -of the DOF core by the following +For further information of the root classes such as \<^bindex>\float\ \<^typ>\float\'s, please consult +the ontology in \<^theory>\Isabelle_DOF.Isa_COL\ directly and consult the Example I and II for +their pragmatics. The \<^theory>\Isabelle_DOF.Isa_COL\ also provides the subclasses +\<^typ>\figure\ \<^bindex>\figure\ and \<^bindex>\listing\ \<^typ>\listing\ which together with specific +text-antiquotations like: + \<^enum> \@{theory_text [options] "path"}\ (Isabelle) + \<^enum> \@{fig_content (width=\, height=\, caption=\) "path"}\ (COL) + \<^enum> \@{boxed_theory_text [display] \ ... \ }\ (local, e.g. manual) + \<^enum> \@{boxed_sml [display] \ ... \ }\ (local, e.g. manual) + \<^enum> \@{boxed_pdf [display] \ ... \ }\ (local, e.g. manual) + \<^enum> \@{boxed_latex [display] \ ... \ }\ (local, e.g. manual) + \<^enum> \@{boxed_bash [display] \ ... \ }\ (local, e.g. manual)\ + +(*<*) +text\With these primitives, it is possible to compose listing-like text-elements or +side-by-side-figures as shown in the subsequent example: + +@{boxed_theory_text [display]\ +text*[inlinefig::float, + main_caption="\The Caption.\"] + \@{theory_text [display, margin = 5] \lemma A :: "a \ b"\}\ + +text*[dupl_graphics::float, + main_caption="\The Caption.\"] +\ +@{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>\\\<^sub>i + 1\ test") "figures/B.png"} +\\}\ +(*>*) + +text\Note that the \<^theory_text>\side_by_side_figure*\-command \<^bindex>\side\_by\_side\_figure\ used in earlier +versions of \<^dof> thus became obsolete. + +\<^verbatim>\COL\ finally provides macros that extend the command-language of the DOF core by the following abbreviations: \<^item> \derived_text_element\ : @@ -702,7 +733,7 @@ abbreviations: ( ( @@{command "chapter*"} | @@{command "section*"} | @@{command "subsection*"} | @@{command "subsubsection*"} | @@{command "paragraph*"} - | @@{command "figure*"} | @@{command "side_by_side_figure*"} + | @@{command "figure*"} | @@{command "listing*"} ) \ '[' meta_args ']' '\' text '\' From 641bea4a58677b237c98e6164c73251c9572bc01 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 15 May 2023 00:01:30 +0200 Subject: [PATCH 14/16] Improved documentation and fixed width-bug of figure* macro. --- Isabelle_DOF/document/preamble.tex | 17 ++++---- Isabelle_DOF/thys/Isa_COL.thy | 6 ++- .../thys/manual/M_01_Introduction.thy | 6 --- Isabelle_DOF/thys/manual/M_02_Background.thy | 15 ++++--- Isabelle_DOF/thys/manual/M_03_GuidedTour.thy | 42 ++++--------------- README.md | 7 ++-- 6 files changed, 31 insertions(+), 62 deletions(-) diff --git a/Isabelle_DOF/document/preamble.tex b/Isabelle_DOF/document/preamble.tex index eceb26bf..22f830e2 100644 --- a/Isabelle_DOF/document/preamble.tex +++ b/Isabelle_DOF/document/preamble.tex @@ -1,6 +1,6 @@ -%% Copyright (C) 2019 University of Exeter, UK -%% 2018 The University of Sheffield, UK -%% 2018 The University of Paris-Saclay, France +%% Copyright (C) University of Exeter, UK +%% The University of Sheffield, UK +%% The University of Paris-Saclay, France %% %% License: %% This program can be redistributed and/or modified under the terms @@ -39,8 +39,8 @@ \pagestyle{headings} \uppertitleback{ -Copyright \copyright{} 2019--2022 University of Exeter, UK\\ -\phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\ +Copyright \copyright{} 2019--2023 University of Exeter, UK\\ +\phantom{Copyright \copyright{}} 2018--2023 Universit\'e Paris-Saclay, France\\ \phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\ \smallskip @@ -74,14 +74,11 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. } \lowertitleback{% -This manual describes \isadof version \isadofversion. The latest official -release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). -The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest -release. The latest development version as well as official releases are available at +This manual describes \isadof as available in the Archive of Formal Proofs (AFP). The latest development version as well as releases that can be installed as Isabelle component are available at \url{\dofurl}. \paragraph*{Contributors.} We would like to thank the following contributors to \isadof -(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric. +(in alphabetical order): Idir Ait-Sadoune and Paolo Crisafulli. \paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay, France, and therefore granted with public funds of the Program ``Investissements d'Avenir.'' diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 5b335e29..981f7790 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -337,6 +337,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) = val ht_s= if relative_height = 100 then "" else "height="^Real.toString((Real.fromInt relative_height) / (Real.fromInt 100)) ^"\\textheight" + val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s]) 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, ... *) @@ -344,7 +345,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) = in if Input.string_of(caption) = "" then file |> (Latex.string o Input.string_of) - |> (XML.enclose ("\\includegraphics"^arg^"{") "}") + |> (XML.enclose ("\\includegraphics"^arg_single^"{") "}") else file |> (Latex.string o Input.string_of) @@ -401,12 +402,13 @@ fun float_command (name, pos) descr cid = {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 + fun parse_and_tex _ (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))) + (* TODO: add label *) |> (Latex.environment ("figure") ) in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex end diff --git a/Isabelle_DOF/thys/manual/M_01_Introduction.thy b/Isabelle_DOF/thys/manual/M_01_Introduction.thy index 49bd081f..6f60b9db 100644 --- a/Isabelle_DOF/thys/manual/M_01_Introduction.thy +++ b/Isabelle_DOF/thys/manual/M_01_Introduction.thy @@ -150,12 +150,6 @@ text\ \<^url>\https://doi.org/10.1007/978-3-030-34968-4_4\. \end{quote} \ -subsubsection\Availability\ -text\ - The implementation of the framework is available at - \url{\<^dofurl>}. The website also provides links to the latest releases. \<^isadof> is licensed - under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause). -\ (*<*) end diff --git a/Isabelle_DOF/thys/manual/M_02_Background.thy b/Isabelle_DOF/thys/manual/M_02_Background.thy index dfe91bdb..69cd237d 100644 --- a/Isabelle_DOF/thys/manual/M_02_Background.thy +++ b/Isabelle_DOF/thys/manual/M_02_Background.thy @@ -51,10 +51,9 @@ foresees a \<^emph>\Nano-Kernel\ (our terminology) which resides in This structure provides a kind of container called \<^emph>\context\ providing an identity, an ancestor-list as well as typed, user-defined state for plugins such as \<^isadof>. On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific -support for higher specification constructs were built. -\<^footnote>\We use the term \<^emph>\plugin\ for a collection of HOL-definitions, SML and Scala code in order -to distinguish it from the official Isabelle term \<^emph>\component\ which implies a particular -format and support by the Isabelle build system.\ +support for higher specification constructs were built.\<^footnote>\We use the term \<^emph>\plugin\ for a collection +of HOL-definitions, SML and Scala code in order to distinguish it from the official Isabelle +term \<^emph>\component\ which implies a particular format and support by the Isabelle build system.\ \ section*[dof::introduction]\The Document Model Required by \<^dof>\ @@ -87,7 +86,7 @@ text\ main sub-document type, for historical reasons, \<^emph>\theory\-files. A theory file\<^bindex>\theory!file\ consists of a \<^emph>\header\\<^bindex>\header\, a \<^emph>\context definition\\<^index>\context\, and a body consisting of a sequence of document elements called - \<^emph>\command\s (see @{figure (unchecked) "docModGenConcr"}(left)). Even + \<^emph>\command\s (see @{figure (unchecked) "docModGenConcr"} (left-hand side)). Even the header consists of a sequence of commands used for introductory text elements not depending on any context. The context-definition contains an \<^boxed_theory_text>\import\ and a \<^boxed_theory_text>\keyword\ section, for example: @@ -113,7 +112,7 @@ text\The body of a theory file consists of a sequence of \<^emph>\co by a command keyword such as \<^boxed_theory_text>\requirement\ 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 @{float "docModGenConcr"}(right)). \ +code and text-elements (see @{float "docModGenConcr"} (right-hand side)). \ text\ A simple text-element \<^index>\text-element\ may look like this: @@ -148,8 +147,8 @@ Its Its general syntactic format reads as follows: The sub-context may be different from the surrounding one; therefore, it is possible to switch from a text-context to a term-context, for example. Therefore, antiquotations allow - the nesting of cartouches, albeit not all combinations are actually supported. -\<^footnote>\In the literature, this concept has been referred to \Cascade-Syntax\ and was used in the + the nesting of cartouches, albeit not all combinations are actually supported.\<^footnote>\In the +literature, this concept has been referred to \Cascade-Syntax\ and was used in the Centaur-system and is existing in some limited form in some Emacs-implementations these days. \ Isabelle comes with a number of built-in antiquotations for text- and code-contexts; a detailed overview can be found in @{cite "wenzel:isabelle-isar:2020"}. \<^dof> reuses this general diff --git a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy index 59718001..aa669c55 100644 --- a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy +++ b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy @@ -70,7 +70,7 @@ text\ subsubsection*[isadof::technical]\Installing \<^isadof>\ text\ By installing the AFP in the previous steps, you already installed \<^isadof>. In fact, \<^isadof> -is currently consisting out of two AFP entries: +is currently consisting out of three AFP entries: \<^item> \<^verbatim>\Isabelle_DOF\: This entry contains the \<^isadof> system itself, including the \<^isadof> manual. @@ -87,15 +87,6 @@ is currently consisting out of two AFP entries: are ontologically tracked. However, wrt. the possible linking between the underlying formal theory and this mathematical presentation, it follows a pragmatic path without any ``deep'' linking to types, terms and theorems, and therefore does deliberately not exploit \<^isadof> 's full potential. -\<^item> \<^verbatim>\Isabelle_DOF-Examples-Extra\: This sessen contains a collection of other examples; - but is only accessible at the developer git - \<^url>\https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/src/branch/main/Isabelle_DOF-Examples-Extra\. - - -% The \<^isadof> distribution contains both examples using the ontology \<^verbatim>\scholarly_paper\ in -% the directory \<^nolinkurl>\examples/scholarly_paper/2018-cicm-isabelle_dof-applications/\ or -% \<^nolinkurl>\examples/scholarly_paper/2020-iFM-CSP\. - It is recommended to follow the structure these examples.\ @@ -236,32 +227,21 @@ subsection\Editing Major Examples\ text\ The ontology \<^verbatim>\scholarly_paper\ \<^index>\ontology!scholarly\_paper\ is an ontology modeling academic/scientific papers, with a slight bias towards texts in the domain of mathematics and - engineering. We explain first the principles of its underlying ontology, for examples - using these ontologies we refer to the example sessions described in \<^technical>\isadof\. + engineering. You can inspect/edit the example in Isabelle's IDE, by either \<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the Isabelle-Icon provided by the Isabelle installation) and loading the file \<^nolinkurl>\Isabelle_DOF-Example-I/IsaDofApplications.thy"\ - \<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling: - -@{boxed_bash [display]\ë\prompt{\isadofdirn}ë - isabelle jedit -d . Isabelle_DOF-Example-II/paper.thy \} - -% bu assumes a particular organisation of Isabelle_DOF, Isabelle_DOF-Example-I, ... and an according ROOTS here ... -\ - - -text\ You can build the \<^pdf>-document at the command line by calling: -@{boxed_bash [display] \ë\prompt{}ë isabelle build -d . IsaDofApplications \} +\ +text\ You can build the \<^pdf>-document at the command line by calling: +@{boxed_bash [display] \ë\prompt{}ë isabelle build Isabelle_DOF-Example-I\} \ subsection*[sss::technical]\A Bluffers Guide to the \<^verbatim>\scholarly_paper\ Ontology\ -text\ In this section we give a minimal overview of the ontology formalized in - \<^theory>\Isabelle_DOF.scholarly_paper\.\ - -text\ We start by modeling the usual text-elements of an academic paper: the title and author - information, abstract, and text section: +text\ In this section we give a minimal overview of the ontology formalized in + \<^theory>\Isabelle_DOF.scholarly_paper\. We start by modeling the usual text-elements of an + academic paper: the title and author information, abstract, and text section: @{boxed_theory_text [display] \doc_class title = short_title :: "string option" <= "None" @@ -313,13 +293,9 @@ as follows: \<^item> subsubsection \<^index>\subsubsection\ \Some 3\ \<^vs>\-0.3cm\ Additional means assure that the following invariant is maintained in a document -conforming to \<^verbatim>\scholarly_paper\: - -\<^center>\\level > 0\\ +conforming to \<^verbatim>\scholarly_paper\: \level > 0\. \ -text\\<^vs>\1.0cm\\ - text\ The rest of the ontology introduces concepts for \<^typ>\introduction\, \<^typ>\conclusion\, \<^typ>\related_work\, \<^typ>\bibliography\ etc. More details can be found in \<^verbatim>\scholarly_paper\ contained in the theory \<^theory>\Isabelle_DOF.scholarly_paper\. \ diff --git a/README.md b/README.md index 70286f5d..842acd70 100644 --- a/README.md +++ b/README.md @@ -2,8 +2,6 @@ Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting and formal development. -The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available -online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf) ## Pre-requisites @@ -31,13 +29,16 @@ distribution for your operating system from the [Isabelle website](https://isabelle.in.tum.de/). Furthermore, please install the AFP following the instructions given at . -Isabelle/DOF is currently consisting out of two AFP entries: +Isabelle/DOF is currently consisting out of three AFP entries: * [Isabelle_DOF:](https://www.isa-afp.org/entries/Isabelle_DOF.html) This entry contains the Isabelle/DOF system itself, including the Isabelle/DOF manual. * [Isabelle_DOF-Example-I:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-I.html) This entry contains an example of an academic paper written using the Isabelle/DOF system. +* [Isabelle_DOF-Example-II:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-II.html) + This entry contains an example of an academic paper written using the + Isabelle/DOF system. --> From 9cd34d7815878fb017e4771740fb99d0bf7e7a7d Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 15 May 2023 07:35:11 +0200 Subject: [PATCH 15/16] Run latexmk in error mode for checking for undefined references and other errors after build. --- .woodpecker/build.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.woodpecker/build.yml b/.woodpecker/build.yml index d1824644..92391ea5 100644 --- a/.woodpecker/build.yml +++ b/.woodpecker/build.yml @@ -12,6 +12,7 @@ pipeline: - echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings - isabelle build -x HOL-Proofs -x Isabelle_DOF-Proofs -D . -o browser_info - if [ "$LATEX" = "lualatex" ]; then isabelle build -o 'timeout_scale=2' -D . -o browser_info; else echo "Skipping Isabelle_DOF-Proofs for pdflatex build."; fi + - find . -name 'root.tex' -prune -o -name 'output' -type f | xargs latexmk -$LATEX -cd -quiet -Werror - isabelle components -u . - isabelle dof_mkroot -q DOF_test - isabelle build -D DOF_test From bbac65e233de8f908515f58b6264d6004cada2a6 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 15 May 2023 08:30:33 +0200 Subject: [PATCH 16/16] Proof reading. --- Isabelle_DOF/document/preamble.tex | 3 +- Isabelle_DOF/thys/manual/M_03_GuidedTour.thy | 87 ++++++++----------- Isabelle_DOF/thys/manual/M_04_RefMan.thy | 42 +++------ .../thys/manual/M_05_Implementation.thy | 5 +- 4 files changed, 52 insertions(+), 85 deletions(-) diff --git a/Isabelle_DOF/document/preamble.tex b/Isabelle_DOF/document/preamble.tex index 22f830e2..f2a8e25a 100644 --- a/Isabelle_DOF/document/preamble.tex +++ b/Isabelle_DOF/document/preamble.tex @@ -121,5 +121,6 @@ France, and therefore granted with public funds of the Program ``Investissements \expandafter\index\expandafter{\expanded{#2 (#1)}}% }% - +\sloppy +\raggedbottom \AtBeginDocument{\isabellestyle{literal}\newcommand{\lstnumberautorefname}{Line}} diff --git a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy index aa669c55..1b0e167f 100644 --- a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy +++ b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy @@ -30,14 +30,13 @@ section*[getting_started::technical]\Getting Started\ subsection*[installation::technical]\Installation\ text\ - In this section, we will show how to install \<^isadof> and its pre-requisites: Isabelle and - \<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell). - Furthermore, we focus on the installation of the latest official release of \<^isadof> as + In this section, we will show how to install \<^isadof>. We assume a basic familiarity with a + Linux/Unix-like command line (i.e., a shell). + We focus on the installation of the latest official release of \<^isadof> as available in the Archive of Formal Proofs (AFP).\<^footnote>\If you want to work with the development version of \<^isadof>, please obtain its source code from the \<^isadof> Git repostitory (\<^url>\https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF\ and follow the instructions in provided \<^verbatim>\README.MD\ file.\ - \<^isadof> requires Isabelle\<^bindex>\Isabelle\ with a recent \<^LaTeX>-distribution (e.g., Tex Live 2022 or later). \ @@ -55,14 +54,13 @@ full qualified path. \ text\ -Furthermore, download the latest version of the AFP from \<^url>\https://www.isa-afp.org/download/\ and +Next, download the the AFP from \<^url>\https://www.isa-afp.org/download/\ and follow the instructions given at \<^url>\https://www.isa-afp.org/help/\ for installing the AFP as an Isabelle component.\ paragraph\Installing \<^TeXLive>.\ text\ - Modern Linux distribution will allow you to install \<^TeXLive> using their respective package - managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command + On a Debian-based Linux system (\<^eg>, Ubuntu), the following command should install all required \<^LaTeX> packages: @{boxed_bash [display]\ë\prompt{}ë sudo aptitude install texlive-full\} \ @@ -76,19 +74,17 @@ is currently consisting out of three AFP entries: contains the \<^isadof> system itself, including the \<^isadof> manual. \<^item> \<^verbatim>\Isabelle_DOF-Example-I\: This entry contains an example of an academic paper written using the \<^isadof> system oriented towards an - introductory paper. The text is based on the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}; + introductory paper. The text is based on~@{cite "brucker.ea:isabelle-ontologies:2018"}; in the document, we deliberately refrain from integrating references to formal content in order - to demonstrate that \<^isadof> is not a framework from Isabelle users to Isabelle users only, but - people just avoiding as much as possible \<^LaTeX> notation. + to demonstrate that \<^isadof> can be used for writing documents with very little direct use of + \<^LaTeX>. \<^item> \<^verbatim>\Isabelle_DOF-Example-II\: This entry contains another example of - a mathematics-oriented academic paper. It is based on the iFM 2020 paper~@{cite "taha.ea:philosophers:2020"}. + a mathematics-oriented academic paper. It is based on~@{cite "taha.ea:philosophers:2020"}. It represents a typical mathematical text, heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing between statements, definitions and proofs which are ontologically tracked. However, wrt. the possible linking between the underlying formal theory and this mathematical presentation, it follows a pragmatic path without any ``deep'' linking to - types, terms and theorems, and therefore does deliberately not exploit \<^isadof> 's full potential. - -It is recommended to follow the structure these examples.\ + types, terms and theorems, and therefore does deliberately not exploit \<^isadof> 's full potential.\ section*[writing_doc::technical]\Writing Documents\ @@ -107,27 +103,18 @@ session example = Isabelle_DOF + options [document = pdf, document_output = "output", document_build = dof] (*theories [document = false] A - B theories - C - D*) + B*) \end{config} The document template and ontology can be selected as follows: @{boxed_theory_text [display] \ -theory - C -imports - Isabelle_DOF.technical_report - Isabelle_DOF.scholarly_paper -begin - -list_templates -use_template "scrreprt-modern" -list_ontologies -use_ontology "technical_report" and "scholarly_paper" - +theory C imports Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper begin + list_templates + use_template "scrreprt-modern" + list_ontologies + use_ontology "technical_report" and "scholarly_paper" end \} @@ -161,7 +148,6 @@ session example = HOL + options [document = pdf, document_output = "output", document_build = dof] session Isabelle_DOF.scholarly_paper - Isabelle_DOF.technical_report theories C \end{config} @@ -308,10 +294,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. \ -figure*[fig0::figure,relative_width="90",file_src="''figures/header_CSP_source.png''"] +figure*[fig0::figure,relative_width="85",file_src="''figures/header_CSP_source.png''"] \ A mathematics paper as integrated document source ... \ -figure*[fig0B::figure,relative_width="90",file_src="''figures/header_CSP_pdf.png''"] +figure*[fig0B::figure,relative_width="85",file_src="''figures/header_CSP_pdf.png''"] \ ... and as corresponding \<^pdf>-output. \ text\The integrated source of this paper-excerpt is shown in \<^figure>\fig0\, while the @@ -445,15 +431,15 @@ defined by \<^typ>\article\. text*[exploring::float, main_caption="\Exploring text elements.\"] \ -@{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"} +@{fig_content (width=45, caption="Exploring a reference of a text-element.") "figures/Dogfood-II-bgnd1.png" +}\<^hfill>@{fig_content (width=45, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"} \ text*[hyperlinks::float, main_caption="\Navigation via generated hyperlinks.\"] \ -@{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"} +@{fig_content (width=45, caption="Hyperlink to class-definition.") "figures/Dogfood-IV-jumpInDocCLass.png" +}\<^hfill>@{fig_content (width=45, caption="Exploring an attribute (hyperlinked to the class).") "figures/Dogfood-V-attribute.png"} \ text\ @@ -498,16 +484,14 @@ text\The present version of \<^isadof> is the first version that supports \<^dof>-generated term-antiquotations\<^bindex>\term-antiquotations\, \<^ie>, antiquotations embedded in HOL-\\\-terms possessing arguments that were validated in the ontological context. These \\\-terms may occur in definitions, lemmas, or in values to define attributes -in class instances. They have the format:\ - -text\\<^center>\\@{name arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1} arg\<^sub>n\\\ +in class instances. They have the format: \@{name arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1} arg\<^sub>n\\ text\Logically, they are defined as an identity in the last argument \arg\<^sub>n\; thus, ontologically checked prior arguments \arg\<^sub>1 ... arg\<^sub>n\<^sub>-\<^sub>1\ can be ignored during a proof 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. \ -figure*[doc_termAq::figure,relative_width="50",file_src="''figures/doc-mod-term-aq.pdf''"] +figure*[doc_termAq::figure,relative_width="35",file_src="''figures/doc-mod-term-aq.pdf''"] \Term-Antiquotations Referencing to Annotated Elements\ text\As shown in @{figure \doc_termAq\}, this feature of \<^isadof> substantially increases the expressibility of links between the formal and the informal in \<^dof> documents.\ @@ -541,14 +525,13 @@ Isabelle/Isar \<^theory_text>\theorem\-command will in contrast to Note that the \<^theory_text>\declare_reference*\ command will appear in the \<^LaTeX> generated from this document fragment. In order to avoid this, one has to enclose this command into the -document comments :\ -text\\<^center>\\(*<*) ... (*>*)\\\ +document comments : \(*<*) ... (*>*)\.\ section*[tech_onto::example]\Writing Technical Reports in \<^boxed_theory_text>\technical_report\\ text\While it is perfectly possible to write documents in the -\<^verbatim>\technical_report\ ontology in freeform-style (the present manual is mostly an -example for this category), we will briefly explain here the tight-checking-style in which +\<^verbatim>\technical_report\ ontology in freeform-style (this manual is mostly such an +example), we will briefly explain here the tight-checking-style in which most Isabelle reference manuals themselves are written. The idea has already been put forward by Isabelle itself; besides the general infrastructure on @@ -601,9 +584,8 @@ text\They are text-contexts equivalents to the \<^theory_text>\term* for term-contexts introduced in @{technical (unchecked) \subsec:onto-term-ctxt\}\ subsection\A Technical Report with Tight Checking\ -text\An example of tight checking is a small programming manual developed by the -second author in order to document programming trick discoveries while implementing in Isabelle. -While not necessarily a meeting standards of a scientific text, it appears to us that this information +text\An example of tight checking is a small programming manual to document programming trick +discoveries while implementing in Isabelle. While not necessarily a meeting standards of a scientific text, it appears to us that this information is often missing in the Isabelle community. So, if this text addresses only a very limited audience and will never be famous for its style, @@ -613,13 +595,13 @@ So its value is that readers can just reuse some of these snippets and adapt the purposes. \ -figure*[strict_SS::figure, relative_width="95", file_src="''figures/MyCommentedIsabelle.png''"] +figure*[strict_em::figure, relative_width="95", file_src="''figures/MyCommentedIsabelle.png''"] \A table with a number of SML functions, together with their type.\ text\ -\TR_MyCommentedIsabelle\ is written according to the \<^verbatim>\technical_report\ ontology in +This manual is written according to the \<^verbatim>\technical_report\ ontology in \<^theory>\Isabelle_DOF.technical_report\. -\<^figure>\strict_SS\ shows a snippet from this integrated source and gives an idea why +\<^figure>\strict_em\ shows a snippet from this integrated source and gives an idea why its tight-checking allows for keeping track of underlying Isabelle changes: Any reference to an SML operation in some library module is type-checked, and the displayed SML-type really corresponds to the type of the operations in the underlying SML environment. @@ -647,8 +629,7 @@ text\ This is *\emphasized\ and this is a citation @{cite "brucker.ea:isabelle-ontologies:2018"}.\ \} The list of standard Isabelle document antiquotations, as well as their options and styles, -can be found in the Isabelle reference manual @{cite "wenzel:isabelle-isar:2020"}, also be found -under \<^url>\https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2022/doc/isar-ref.pdf\, +can be found in the Isabelle reference manual @{cite "wenzel:isabelle-isar:2020"}, section 4.2. In practice, \<^isadof> documents with ambitious layout will contain a certain number of @@ -657,7 +638,7 @@ not possible. As far as possible, raw \<^LaTeX> should be restricted to the defi of ontologies and macros (see @{docitem (unchecked) \isadof_ontologies\}). If raw \<^LaTeX> commands can not be avoided, it is recommended to use the Isabelle document comment \<^latex>\\verb+\+\verb+<^latex>+\\\argument\\ to isolate these parts -(cf. \<^url>\https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2022/doc/isar-ref.pdf\). +(cf. @{cite "wenzel:isabelle-isar:2020"}). Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can diff --git a/Isabelle_DOF/thys/manual/M_04_RefMan.thy b/Isabelle_DOF/thys/manual/M_04_RefMan.thy index 57f63b08..07478cf7 100644 --- a/Isabelle_DOF/thys/manual/M_04_RefMan.thy +++ b/Isabelle_DOF/thys/manual/M_04_RefMan.thy @@ -309,8 +309,8 @@ text\ Moreover, as usual, special care has to be taken for commands that write into aux-files that are included in a following \<^LaTeX>-run. For such complex examples, we refer the interested reader to the style files provided in the \<^isadof> distribution. In particular - the definitions of the concepts \<^boxed_theory_text>\title*\ and \<^boxed_theory_text>\author*\ in the - file \<^file>\../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\ show examples of protecting + the definitions of the concepts \<^boxed_theory_text>\title*\ and \<^boxed_theory_text>\author*\ in \<^LaTeX>-style + for the ontology @{theory \Isabelle_DOF.scholarly_paper\} shows examples of protecting special characters in definitions that need to make use of a entries in an aux-file. \ @@ -720,11 +720,11 @@ text*[dupl_graphics::float, @{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>\\\<^sub>i + 1\ test") "figures/B.png"} \\}\ + +text\The \<^theory_text>\side_by_side_figure*\-command \<^bindex>\side\_by\_side\_figure\ has been deprecated.\ (*>*) -text\Note that the \<^theory_text>\side_by_side_figure*\-command \<^bindex>\side\_by\_side\_figure\ used in earlier -versions of \<^dof> thus became obsolete. - +text\ \<^verbatim>\COL\ finally provides macros that extend the command-language of the DOF core by the following abbreviations: @@ -1432,35 +1432,22 @@ text\ \<^LaTeX>-packages that are (strictly) required by the used \<^LaTeX>-setup. In general, we recommend to only add \<^LaTeX>-packages that are always necessary for this particular template, as loading packages in the templates minimizes the freedom users have by adapting the \<^path>\preample.tex\. - Moreover, you might want to add/modify the template specific configuration - (\autoref{lst:config-start}-\ref{lst:config-end}). The new template should be stored in - \<^path>\src/document-templates\ and its file name should start with the prefix \<^path>\root-\. After - adding a new template, call the \<^boxed_bash>\install\ script (see \<^technical>\infrastructure\). - The common structure of an \<^isadof> document template looks as follows: + The file name of the new template should start with the prefix \<^path>\root-\ and need to be + registered using the \<^theory_text>\define_template\ command. + a typical \<^isadof> document template looks as follows: \<^latex>\ \begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm] \documentclass{article} % The LaTeX-class of your template ë\label{lst:dc}ë -%% The following part is (mostly) required by Isabelle/DOF, do not modify -\usepackage[T1]{fontenc} % Font encoding -\usepackage[utf8]{inputenc} % UTF8 support -\usepackage{xcolor} -\usepackage{isabelle,isabellesym,amssymb} % Required (by Isabelle) -\usepackage{amsmath} % Used by some ontologies -\bibliographystyle{abbrv} -\input{dof-common} % setup shared between all Isabelle/DOF templates -\usepackage{graphicx} % Required for images. -\usepackage[caption]{subfig} +\usepackage{DOF-core} +\usepackage{subcaption} \usepackage[size=footnotesize]{caption} -\usepackage{hyperref} % Required by Isabelle/DOF - -%% Begin of template specific configuration ë\label{lst:config-start}ë -\urlstyle{rm} -\isabellestyle{it} ë\label{lst:config-end}ë +\usepackage{hyperref} %% Main document, do not modify \begin{document} -\maketitle\input{session} +\maketitle +\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}} \IfFileExists{root.bib}{\bibliography{root}}{} \end{document} \end{ltx}\ @@ -1607,9 +1594,6 @@ text\ } \end{ltx}\ - For a real-world example testing for multiple classes, see - \<^file>\../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\: - We encourage this clear and machine-checkable enforcement of restrictions while, at the same time, we also encourage to provide a package option to overwrite them. The latter allows inherited ontologies to overwrite these restrictions and, therefore, to provide also support diff --git a/Isabelle_DOF/thys/manual/M_05_Implementation.thy b/Isabelle_DOF/thys/manual/M_05_Implementation.thy index 942a78af..fc1207a7 100644 --- a/Isabelle_DOF/thys/manual/M_05_Implementation.thy +++ b/Isabelle_DOF/thys/manual/M_05_Implementation.thy @@ -144,9 +144,10 @@ text\ @{boxed_sml [display] \val _ = Theory.setup - (docitem_antiquotation @{binding "docitem"} DOF_core.default_cid #> + (docitem_antiquotation @{binding "docitem"} DOF_core.default_cid #> - ML_Antiquotation.inline @{binding "docitem_value"} ML_antiquotation_docitem_value)\} + ML_Antiquotation.inline @{binding "docitem_value"} + ML_antiquotation_docitem_value)\} the text antiquotation \<^boxed_sml>\docitem\ is declared and bounded to a parser for the argument syntax and the overall semantics. This code defines a generic antiquotation to be used in text elements such as