Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

basic problems on multiple subfloats content solved

This commit is contained in:
Burkhart Wolff 2023-05-11 16:21:37 +02:00
parent 36740bf72b
commit 8bdd40fc20
10 changed files with 70 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isabelle_DOF-Ontologies/document-templates/root-sn-article-UNSUPPORTED.tex
View File

@ -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

4
Isabelle_DOF-Ontologies/document-templates/root-svjour3-UNSUPPORTED.tex
View File

@ -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

23
Isabelle_DOF-Unit-Tests/COL_Test.thy
View File

@ -28,7 +28,7 @@ text*[S5'::"paragraph"]\<open>Paragraph\<close>
section\<open>General Figure COL Elements\<close>
figure*[fig1_test::figure,spawn_columns=False,relative_width="95",src="''figures/A''"]
figure*[fig1_test::figure,relative_width="95",src="''figures/A''"]
\<open> This is the label text \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>
text*[fig2_test::figure, spawn_columns=False, relative_width="95",src="''figures/A''"
@ -65,22 +65,15 @@ text\<open>check @{side_by_side_figure sbsfig1} cmp to @{side_by_side_figure sbs
(* And a side-chick ... *)
text*[inlinefig::float,
caption="\<open>The Caption.\<close>"]
\<open>@{theory_text [display, margin = 5] \<open>lemma A :: "a \<longrightarrow> b"\<close>}\<close>
main_caption="\<open>The Caption.\<close>"]
\<open>@{theory_text [display, margin = 5] \<open>lemma A :: "a \<longrightarrow> b"\<close>}\<close>
text*[fffff::float]\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>)
\<open>figures/A.png\<close>}\<close>
text*[dupl_graphics::float,
main_caption="\<open>The Caption.\<close>"]\<open>
@{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>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/B.png"}
\<close>
(*<*)
text*[inlinegraph::float,
caption="\<open>Another \<sigma>\<^sub>i+2 Caption.\<close>"]
\<open>@{fig_content [display] (scale = 80, width=80, caption=\<open>This is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<close>)
\<open>figures/A.png\<close>}\<close>
(*>*)
(*<*)
end
(*>*)

8
Isabelle_DOF-Unit-Tests/Latex_Tests.thy
View File

@ -418,16 +418,16 @@ Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
(*<*)
text-latex\<open>
@{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>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/A.png"}
Figure*[figxxx::float,main_caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
\<open> @{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>\<open>\<sigma>\<^sub>i + 1\<close> test") "figures/A.png"}
\<close>
(* proposed syntax for sub-figure labels : text\<open> @{figure "ffff(2)"}\<close> *)
Figure*[figxxx::float,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
Figure*[figxxxx::float,main_caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
\<open>@{boxed_theory_text [display]
\<open>lemma inv_c2_preserved : "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^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

4
Isabelle_DOF/latex/document-templates/root-lncs.tex
View File

@ -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}

2
Isabelle_DOF/latex/document-templates/root-scrartcl.tex
View File

@ -26,7 +26,7 @@
\usepackage{textcomp}
\bibliographystyle{abbrvnat}
\RequirePackage[caption]{subfig}
\RequirePackage{subcaption}
\usepackage[numbers, sort&compress, sectionbib]{natbib}

4
Isabelle_DOF/latex/document-templates/root-scrreprt-modern.tex
View File

@ -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

4
Isabelle_DOF/latex/document-templates/root-scrreprt.tex
View File

@ -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}}

11
Isabelle_DOF/latex/styles/DOF-COL.sty
View File

@ -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}
}

94
Isabelle_DOF/thys/Isa_COL.thy
View File

@ -147,25 +147,24 @@ end
section\<open> Library of Standard Text Ontology \<close>
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\<open> "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context>
|> Name_Space.space_of_table)\<close>
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 \<sigma> = graphics"
doc_class side_by_side_figure = figure +
@ -225,7 +224,7 @@ end\<close>
setup\<open> DOF_lib.define_macro \<^binding>\<open>vs\<close> "\\vspace{" "}" (check_latex_measure) \<close>
setup\<open> DOF_lib.define_macro \<^binding>\<open>hs\<close> "\\hspace{" "}" (check_latex_measure) \<close>
define_shortcut* hfill \<rightleftharpoons> \<open>\hfill\<close>
(*<*)
text\<open>Tests: \<^vs>\<open>-0.14cm\<close>\<close>
@ -266,29 +265,29 @@ text\<open>The intermediate development goal is to separate the ontological, top
\<^emph>\<open>import\<close> of a figure. The hope is that this opens the way for more orthogonality and
abstraction from the LaTeX engine.
\<close>
ML\<open>
ML\<open>XML.enclose\<close>
ML\<open>
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
\<close>
ML\<open>\<close>
ML\<open>
val _ = Path.parent
val mdir = Resources.master_directory @{theory}
@ -673,7 +682,7 @@ declare[[tab_cell_placing="left",tab_cell_height="18.0cm"]]
section\<open>Tests\<close>
(*<*)
text\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
text\<open> @{fig_content [display] (height = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
\<open>figures/isabelle-architecture.pdf\<close>}\<close>
text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open>12.0cm\<close>,
cell_height =\<open>13pt\<close>, cell_width = \<open>12.0cm\<close>,
@ -685,11 +694,6 @@ text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open
(*>*)
ML\<open>@{term "side_by_side_figure"};
@{typ "doc_class rexp"};
DOF_core.SPY;
\<close>
text\<open>@{term_ \<open>3 + 4::int\<close>} @{value_ \<open>3 + 4::int\<close>} \<close>
end