forked from Isabelle_DOF/Isabelle_DOF
Improved fig_content, fix backend bugs in COL_Test
This commit is contained in:
parent
5b519fcbe6
commit
b8da1a304a
|
@ -19,7 +19,7 @@ text*[S2'::"section"]\<open>Section\<close>
|
||||||
subsection*[S3::"subsection"]\<open>Subsection\<close>
|
subsection*[S3::"subsection"]\<open>Subsection\<close>
|
||||||
text*[S3'::"subsection"]\<open>Subsection\<close>
|
text*[S3'::"subsection"]\<open>Subsection\<close>
|
||||||
|
|
||||||
subsubsection*[S4::"subsubsection"]\<open>Subsection\<close>
|
subsubsection*[S4::"subsubsection"]\<open>Subsubsection\<close>
|
||||||
text*[S4'::"subsubsection"]\<open>Subsubsection\<close>
|
text*[S4'::"subsubsection"]\<open>Subsubsection\<close>
|
||||||
|
|
||||||
paragraph*[S5::"paragraph"]\<open>PAragraph\<close>
|
paragraph*[S5::"paragraph"]\<open>PAragraph\<close>
|
||||||
|
@ -29,7 +29,7 @@ text*[S5'::"paragraph"]\<open>Paragraph\<close>
|
||||||
section\<open>General Figure COL Elements\<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,spawn_columns=False,relative_width="95",src="''figures/A''"]
|
||||||
\<open> This is the label text \<close>
|
\<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''"
|
text*[fig2_test::figure, spawn_columns=False, relative_width="95",src="''figures/A''"
|
||||||
]\<open> This is the label text\<close>
|
]\<open> This is the label text\<close>
|
||||||
|
@ -68,6 +68,9 @@ text*[inlinefig::float,
|
||||||
caption="\<open>The Caption.\<close>"]
|
caption="\<open>The Caption.\<close>"]
|
||||||
\<open>@{theory_text [display, margin = 5] \<open>lemma A :: "a \<longrightarrow> b"\<close>}\<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>document/figures/A.png\<close>}\<close>
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
text*[inlinegraph::float,
|
text*[inlinegraph::float,
|
||||||
caption="\<open>Another \<sigma>\<^sub>i+2 Caption.\<close>"]
|
caption="\<open>Another \<sigma>\<^sub>i+2 Caption.\<close>"]
|
||||||
|
|
|
@ -420,6 +420,10 @@ Figure*[ffff::float, caption="\<open>this is another 2 side-by-side\<close>"]
|
||||||
\<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\<close>
|
\<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\<close>
|
||||||
\<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\<close>
|
\<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\<close>
|
||||||
|
|
||||||
|
|
||||||
|
text*[fffff::float]\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
|
||||||
|
\<open>document/figures/A.png\<close>}\<close>
|
||||||
|
|
||||||
(* proposed syntax for sub-figure labels : text\<open> @{figure "ffff(2)"}\<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*[figxxx::float,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
|
||||||
|
|
|
@ -13,7 +13,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
|
||||||
"Attributes"
|
"Attributes"
|
||||||
"AssnsLemmaThmEtc"
|
"AssnsLemmaThmEtc"
|
||||||
"Ontology_Matching_Example"
|
"Ontology_Matching_Example"
|
||||||
"Cenelec_Test"
|
"Cenelec_Test"
|
||||||
"OutOfOrderPresntn"
|
"OutOfOrderPresntn"
|
||||||
"COL_Test"
|
"COL_Test"
|
||||||
document_files
|
document_files
|
||||||
|
|
|
@ -94,7 +94,7 @@
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% begin: chapter*-dispatcher
|
% begin: chapter*-dispatcher
|
||||||
\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}}
|
\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTchapter},#1]{\BODY}}
|
||||||
% end: chapter*-dispatcher
|
% end: chapter*-dispatcher
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
@ -106,19 +106,19 @@
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% begin: subsection*-dispatcher
|
% begin: subsection*-dispatcher
|
||||||
\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}}
|
\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsection},#1]{\BODY}}
|
||||||
% end: subsection*-dispatcher
|
% end: subsection*-dispatcher
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% begin: subsubsection*-dispatcher
|
% begin: subsubsection*-dispatcher
|
||||||
\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={subsubsection},#1]{\BODY}}
|
\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTsubsubsection},#1]{\BODY}}
|
||||||
% end: subsubsection*-dispatcher
|
% end: subsubsection*-dispatcher
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% begin: paragraph*-dispatcher
|
% begin: paragraph*-dispatcher
|
||||||
\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={paragraph},#1]{\BODY}}
|
\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={IsaUNDERSCORECOLDOTparagraph},#1]{\BODY}}
|
||||||
% end: paragraph*-dispatcher
|
% end: paragraph*-dispatcher
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
@ -135,19 +135,19 @@
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% begin: chapter/section default implementations
|
% begin: chapter/section default implementations
|
||||||
\newisadof{chapter}[label=,type=][1]{%
|
\newisadof{IsaUNDERSCORECOLDOTchapter}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
|
||||||
\isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
|
\isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||||
}
|
}
|
||||||
\newisadof{IsaUNDERSCORECOLDOTsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
|
\newisadof{IsaUNDERSCORECOLDOTsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
|
||||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||||
}
|
}
|
||||||
\newisadof{subsection}[label=,type=][1]{%
|
\newisadof{IsaUNDERSCORECOLDOTsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
|
||||||
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||||
}
|
}
|
||||||
\newisadof{subsubsection}[label=,type=][1]{%
|
\newisadof{IsaUNDERSCORECOLDOTsubsubsection}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
|
||||||
\isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
\isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||||
}
|
}
|
||||||
\newisadof{paragraph}[label=,type=][1]{%
|
\newisadof{IsaUNDERSCORECOLDOTparagraph}[label=,type=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=][1]{%
|
||||||
\isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue%
|
\isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||||
}
|
}
|
||||||
% end: chapter/section default implementations
|
% end: chapter/section default implementations
|
||||||
|
|
|
@ -325,7 +325,7 @@ fun fig_content_antiquotation name scan =
|
||||||
else ()
|
else ()
|
||||||
val wdth_s = if relative_width = 100 then ""
|
val wdth_s = if relative_width = 100 then ""
|
||||||
else "width="^Real.toString((Real.fromInt relative_width)
|
else "width="^Real.toString((Real.fromInt relative_width)
|
||||||
/ (Real.fromInt 100))^"\textwidth"
|
/ (Real.fromInt 100))^"\\textwidth"
|
||||||
val scale_s= if scale = 100 then ""
|
val scale_s= if scale = 100 then ""
|
||||||
else "scale="^Real.toString((Real.fromInt scale) / (Real.fromInt 100))
|
else "scale="^Real.toString((Real.fromInt scale) / (Real.fromInt 100))
|
||||||
val arg = enclose "[" "]" (commas [wdth_s,scale_s])
|
val arg = enclose "[" "]" (commas [wdth_s,scale_s])
|
||||||
|
@ -333,10 +333,11 @@ fun fig_content_antiquotation name scan =
|
||||||
val path = Resources.check_file ctxt NONE file
|
val path = Resources.check_file ctxt NONE file
|
||||||
val _ = writeln("file "^Path.file_name path)
|
val _ = writeln("file "^Path.file_name path)
|
||||||
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
|
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
|
||||||
|
|
||||||
in file
|
in file
|
||||||
|> (Latex.string o Input.string_of)
|
|> (Latex.string o Input.string_of)
|
||||||
|> (XML.enclose ("\\includegraphics"^arg^"{") "}")
|
|> (XML.enclose ("\\includegraphics"^arg^"{") "}")
|
||||||
|> (fn X => X @ Latex.macro "capture" lab)
|
|> (fn X => X @ Latex.macro "caption" lab)
|
||||||
end
|
end
|
||||||
)
|
)
|
||||||
));
|
));
|
||||||
|
|
Loading…
Reference in New Issue