From 8bdd40fc20bdd6c69dc10e30661beddef736f91e Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Thu, 11 May 2023 16:21:37 +0200 Subject: [PATCH 01/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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: "