From 8bdd40fc20bdd6c69dc10e30661beddef736f91e Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Thu, 11 May 2023 16:21:37 +0200 Subject: [PATCH] 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 891fe19..e8df544 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 5d554f9..8ee88a3 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 9d53e2d..a70f58d 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 2d0ba44..48b8e67 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 f6ca007..c2827a0 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 237afda..8b225df 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 795836e..adf8d49 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 5f5958c..f23aa9b 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 bc75e9d..a8ae730 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 6ffb439..a28ec3b 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