Some first test on the COL library, assuring coherence between text* and figure* versiona.
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Burkhart Wolff 2023-05-09 12:59:42 +02:00
parent 7ba220e417
commit b04ff7e31a
4 changed files with 52 additions and 3 deletions

View File

@ -366,7 +366,7 @@ Our model prescribes an optional \<^theory_text>\<open>main_author\<close> and a
text section; since instances of this class are mutable (meta)-objects of text-elements, they
can be modified arbitrarily through subsequent text and of course globally during text evolution.
Since \<^theory_text>\<open>author\<close> is a HOL-type internally generated by \<^isadof> framework and can therefore
appear in the \<^theory_text>\<open>main_author\<close> attribute of the \<^theory_text>\<open>text_section\<close> class;
appear in the \<^theory_text>\<open>main_author\<close> attribute of the \<^theory_text>\<open>text_section\<close> class;
semantic links between concepts can be modeled this way.
The translation of its content to, \<^eg>, Springer's \<^LaTeX> setup for the Lecture Notes in Computer

View File

@ -0,0 +1,48 @@
theory
COL_Test
imports
"Isabelle_DOF_Unit_Tests_document"
begin
print_doc_items
print_doc_classes
figure*[fig1_test::figure,spawn_columns=False,relative_width="95",src="''figures/A''"]
\<open> This is the label text \<close>
text*[fig2_test::figure, spawn_columns=False, relative_width="95",src="''figures/A''"
]\<open> This is the label text\<close>
text\<open>check @{figure fig1_test} cmp to @{figure fig2_test}\<close>
side_by_side_figure*["sbsfig1"::side_by_side_figure,
anchor="''Asub1''",
caption="''First caption.''",
relative_width="48",
src="''figures/A''",
anchor2="''Asub2''",
caption2="''Second caption.''",
relative_width2="47",
src2="''figures/B''"]\<open> Exploring text elements. \<close>
text*["sbsfig2"::side_by_side_figure,
anchor="''fig:Asub1''",
caption="''First caption.''",
relative_width="48",
src="''figures/A''",
anchor2="''fig:Asub2''",
caption2="''Second caption.''",
relative_width2="47",
src2="''figures/B''"]\<open>The final caption\<close>
text\<open>check @{side_by_side_figure sbsfig1} cmp to @{side_by_side_figure sbsfig2}
\autoref{Asub1} vs. \autoref{Asub2}
\autoref{fig:Asub1} vs. \autoref{fig:Asub2}
\<close>
(*<*)
end
(*>*)

View File

@ -15,6 +15,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
"Ontology_Matching_Example"
"Cenelec_Test"
"OutOfOrderPresntn"
"COL_Test"
document_files
"root.bib"
"figures/A.png"

View File

@ -21,7 +21,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: figure*
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
\newisadof{figureDOTIsaUNDERSCORECOLDOTfigure}%
\newisadof{IsaUNDERSCORECOLDOTfigure}%
[label=,type=%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
@ -70,7 +70,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: side_by_side_figure*
\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={sideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure},#1]{\BODY}}
\newisadof{sideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTIsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure}%
\newisadof{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure}%
[label=,type=%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%