From 060dcbbabc37c4f145c70b5abe0e4ead74511f23 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 30 Mar 2019 16:36:25 +0000 Subject: [PATCH 1/9] Introduced \isadof* command family. --- .../latex/DOF-CENELEC_50128.sty | 10 +++--- document-generator/latex/DOF-core.sty | 19 ++++++++--- .../latex/DOF-scholarly_paper.sty | 32 +++++++++---------- .../latex/DOF-technical_report.sty | 21 +++++++++--- 4 files changed, 52 insertions(+), 30 deletions(-) diff --git a/document-generator/latex/DOF-CENELEC_50128.sty b/document-generator/latex/DOF-CENELEC_50128.sty index a2a00c4..48ea3db 100644 --- a/document-generator/latex/DOF-CENELEC_50128.sty +++ b/document-generator/latex/DOF-CENELEC_50128.sty @@ -44,33 +44,33 @@ \end{isamarkuptext}% } -\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.assumption\endcsname% +\newisadof{text.CENELEC_50128.assumption}% [label=,type=,assumption=][1]{% \begin{isamarkuptext}% #1 \end{isamarkuptext}% } -\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.hypothesis\endcsname% +\newisadof{text.CENELEC_50128.hypothesis}% [label=,type=,assumption=][1]{% \begin{isamarkuptext}% #1 \end{isamarkuptext}% } -\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.srac\endcsname% +\newisadof{text.CENELEC_50128.srac}% [label=,type=,assumption=][1]{% \begin{isamarkuptext}% #1 \end{isamarkuptext}% } -\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.ec\endcsname% +\newisadof{text.CENELEC_50128.ec}% [label=,type=,assumption=][1]{% \begin{isamarkuptext}% #1 \end{isamarkuptext}% } -\expandafter\newkeycommand\csname isaDof.text.CENELEC_50128.test_result\endcsname% +\newisadof{text.CENELEC_50128.test_result}% [label=,type=,assumption=][1]{% \begin{isamarkuptext}% #1 diff --git a/document-generator/latex/DOF-core.sty b/document-generator/latex/DOF-core.sty index dc1557b..e40812f 100644 --- a/document-generator/latex/DOF-core.sty +++ b/document-generator/latex/DOF-core.sty @@ -24,14 +24,25 @@ \newcommand{\isadof}{Isabelle/DOF\xspace} -% Generic dispatcher +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: newcommand wrapper +\newcommand\newisadof[1]{\expandafter\newkeycommand\csname isaDof.#1\endcsname}% +\newcommand\renewisadof[1]{\expandafter\renewkeycommand\csname isaDof.#1\endcsname}% +\newcommand\provideisadof[1]{\expandafter\providekeycommand\csname isaDof.#1\endcsname}% +% end: newcommand wrapper +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: generic dispatcher \newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{% \csname isaDof.\commandkey{env}.\commandkey{type}\endcsname[label=\commandkey{label},\commandkey{args}]{#1}% } +% end: generic dispatcher +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: text.text -\expandafter\newkeycommand\csname isaDof.text.text\endcsname% +\newisadof{text.text}% [label=,type=% ][1]{% \begin{isamarkuptext}% @@ -44,7 +55,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: figure* \NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}} -\expandafter\newkeycommand\csname isaDof.figure.Isa_COL.figure\endcsname% +\newisadof{figure.Isa_COL.figure}% [label=,type=% ,Isa_COL.figure.relative_width=% ,Isa_COL.figure.placement=% @@ -74,7 +85,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: side_by_side_figure* \NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}} -\expandafter\newkeycommand\csname isaDof.side_by_side_figure.Isa_COL.side_by_side_figure\endcsname% +\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}% [label=,type=% ,Isa_COL.figure.relative_width=% ,Isa_COL.figure.src=% diff --git a/document-generator/latex/DOF-scholarly_paper.sty b/document-generator/latex/DOF-scholarly_paper.sty index 146a677..59fc16f 100644 --- a/document-generator/latex/DOF-scholarly_paper.sty +++ b/document-generator/latex/DOF-scholarly_paper.sty @@ -52,7 +52,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: title* \NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}} -\expandafter\newkeycommand\csname isaDof.title.scholarly_paper.title\endcsname% +\newisadof{title.scholarly_paper.title}% [label=,type=% ,keywordlist=% ][1]{% @@ -64,7 +64,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: subtitle* \NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}} -\expandafter\newkeycommand\csname isaDof.subtitle.scholarly_paper.subtitle\endcsname% +\newisadof{subtitle.scholarly_paper.subtitle}% [label=,type=% ,keywordlist=% ][1]{% @@ -106,7 +106,7 @@ } } -\expandafter\providekeycommand\csname isaDof.text.scholarly_paper.author\endcsname% +\provideisadof{text.scholarly_paper.author}% [label=,type=% ,scholarly_paper.author.email=% ,scholarly_paper.author.affiliation=% @@ -127,7 +127,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.abstract \providecommand{\keywords}[1]{\mbox{}\\\medskip\noindent{\textbf{Keywords:}} #1} -\expandafter\newkeycommand\csname isaDof.text.scholarly_paper.abstract\endcsname% +\newisadof{text.scholarly_paper.abstract}% [label=,type=% ,scholarly_paper.abstract.keywordlist=% ][1]{% @@ -145,21 +145,21 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.introduction -\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.introduction\endcsname% +\newisadof{section.scholarly_paper.introduction}% [label=,type=% ,scholarly_paper.introduction.main_author=% ,scholarly_paper.introduction.fixme_list=% ][1]{% \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% } -\expandafter\newkeycommand\csname isaDof.subsection.scholarly_paper.introduction\endcsname% +\newisadof{subsection.scholarly_paper.introduction}% [label=,type=% ,scholarly_paper.introduction.main_author=% ,scholarly_paper.introduction.fixme_list=% ][1]{% \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% } -\expandafter\newkeycommand\csname isaDof.text.scholarly_paper.introduction_elem\endcsname% +\newisadof{text.scholarly_paper.introduction_elem}% [label=,type=% ,scholarly_paper.introduction.main_author=% ,scholarly_paper.introduction.fixme_list=% @@ -168,7 +168,7 @@ #1 \end{isamarkuptext}% } -\expandafter\newkeycommand\csname isaDof.text.scholarly_paper.introduction\endcsname% +\newisadof{text.scholarly_paper.introduction}% [label=,type=% ,scholarly_paper.introduction.main_author=% ,scholarly_paper.introduction.fixme_list=% @@ -182,7 +182,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.introduction -\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.text_section\endcsname% +\newisadof{section.scholarly_paper.text_section}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -194,14 +194,14 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.technical -\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.technical\endcsname% +\newisadof{section.scholarly_paper.technical}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% ][1]{% \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% } -\expandafter\newkeycommand\csname isaDof.subsection.scholarly_paper.technical\endcsname% +\newisadof{subsection.scholarly_paper.technical}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -213,14 +213,14 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.example -\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.example\endcsname% +\newisadof{section.scholarly_paper.example}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% ][1]{% \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% } -\expandafter\newkeycommand\csname isaDof.subsection.scholarly_paper.example\endcsname% +\newisadof{subsection.scholarly_paper.example}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -232,7 +232,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.conclusion -\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.conclusion\endcsname% +\newisadof{section.scholarly_paper.conclusion}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -244,7 +244,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.conclusion -\expandafter\newkeycommand\csname isaDof.subsection.scholarly_paper.conclusion\endcsname% +\newisadof{subsection.scholarly_paper.conclusion}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -255,7 +255,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.bibliography -\expandafter\newkeycommand\csname isaDof.section.scholarly_paper.bibliography\endcsname% +\newisadof{section.scholarly_paper.bibliography}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% diff --git a/document-generator/latex/DOF-technical_report.sty b/document-generator/latex/DOF-technical_report.sty index e89e701..ca5928e 100644 --- a/document-generator/latex/DOF-technical_report.sty +++ b/document-generator/latex/DOF-technical_report.sty @@ -32,7 +32,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.introduction -\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.introduction\endcsname% +\newisadof{chapter.scholarly_paper.introduction}% [label=,type=% ,scholarly_paper.introduction.main_author=% ,scholarly_paper.introduction.fixme_list=% @@ -44,7 +44,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.introduction -\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.text_section\endcsname% +\newisadof{chapter.scholarly_paper.text_section}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -56,7 +56,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.technical -\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.technical\endcsname% +\newisadof{chapter.scholarly_paper.technical}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -68,7 +68,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.example -\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.example\endcsname% +\newisadof{chapter.scholarly_paper.example}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -80,7 +80,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.conclusion -\expandafter\newkeycommand\csname isaDof.chapter.scholarly_paper.conclusion\endcsname% +\newisadof{chapter.scholarly_paper.conclusion}% [label=,type=% ,scholarly_paper.text_section.main_author=% ,scholarly_paper.text_section.fixme_list=% @@ -90,3 +90,14 @@ % end: scholarly_paper.conclusion %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newisadof{text.technical_report.front_matter}% +[label=,type=% +,scholarly_paper.introduction.main_author=% +,scholarly_paper.introduction.fixme_list=% +][1]{% + \begin{isamarkuptext}% + #1 + \end{isamarkuptext}% +} +% end: scholarly_paper.introduction From 8935d8f4e93b7991ee3ae596b181ecbf4f232544 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 30 Mar 2019 17:18:17 +0000 Subject: [PATCH 2/9] Improved error handling. --- document-generator/latex/DOF-core.sty | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/document-generator/latex/DOF-core.sty b/document-generator/latex/DOF-core.sty index e40812f..0e60e40 100644 --- a/document-generator/latex/DOF-core.sty +++ b/document-generator/latex/DOF-core.sty @@ -20,6 +20,7 @@ \RequirePackage{environ} \RequirePackage{graphicx} \RequirePackage{xspace} +\RequirePackage{etoolbox} \RequirePackage{fp} \newcommand{\isadof}{Isabelle/DOF\xspace} @@ -35,7 +36,14 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: generic dispatcher \newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{% -\csname isaDof.\commandkey{env}.\commandkey{type}\endcsname[label=\commandkey{label},\commandkey{args}]{#1}% + \ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname% + \csname isaDof.\commandkey{env}.\commandkey{type}\endcsname% + [label=\commandkey{label},\commandkey{args}]{#1}% + \else% + \errmessage{Isabelle/DOF: No LaTeX representation for concept + "\commandkey{env}.\commandkey{type}" defined:} + + \fi% } % end: generic dispatcher %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% From b5d35dad227ad60e704e98656806374ff22bd3dd Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 30 Mar 2019 19:03:38 +0000 Subject: [PATCH 3/9] Added definition for SRAC. --- document-generator/latex/DOF-CENELEC_50128.sty | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/document-generator/latex/DOF-CENELEC_50128.sty b/document-generator/latex/DOF-CENELEC_50128.sty index 48ea3db..589dead 100644 --- a/document-generator/latex/DOF-CENELEC_50128.sty +++ b/document-generator/latex/DOF-CENELEC_50128.sty @@ -76,3 +76,10 @@ #1 \end{isamarkuptext}% } + +\newisadof{text.CENELEC_50128.SRAC}% +[label=,type=,assumption=][1]{% + \begin{isamarkuptext}% + #1 + \end{isamarkuptext}% +} From e26306debdbc638cfd11ffb264913787b79df87f Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 30 Mar 2019 23:40:01 +0000 Subject: [PATCH 4/9] Refactored LaTeX-Setup and introduced failback to default implementations. --- .../latex/DOF-CENELEC_50128.sty | 2 +- document-generator/latex/DOF-COL.sty | 97 ++++++++++ document-generator/latex/DOF-core.sty | 183 +++++++----------- document-generator/latex/DOF-mathex.sty | 2 +- .../latex/DOF-scholarly_paper.sty | 9 +- 5 files changed, 172 insertions(+), 121 deletions(-) create mode 100644 document-generator/latex/DOF-COL.sty diff --git a/document-generator/latex/DOF-CENELEC_50128.sty b/document-generator/latex/DOF-CENELEC_50128.sty index 589dead..ad5f5e4 100644 --- a/document-generator/latex/DOF-CENELEC_50128.sty +++ b/document-generator/latex/DOF-CENELEC_50128.sty @@ -16,7 +16,7 @@ [0000/00/00 Unreleased v0.0.0+% Document-Type Support Framework for Isabelle (CENELEC 50128).] -\RequirePackage{DOF-core} +\RequirePackage{DOF-COL} \newkeycommand\isaDofSectionRequirement[label=,type=,main_author=,long_name=][1]{% diff --git a/document-generator/latex/DOF-COL.sty b/document-generator/latex/DOF-COL.sty new file mode 100644 index 0000000..a77ae44 --- /dev/null +++ b/document-generator/latex/DOF-COL.sty @@ -0,0 +1,97 @@ +%% Copyright (C) 2018 The University of Sheffield +%% 2018 The University of Paris-Sud +%% +%% License: +%% This program can be redistributed and/or modified under the terms +%% of the LaTeX Project Public License Distributed from CTAN +%% archives in directory macros/latex/base/lppl.txt; either +%% version 1 of the License, or any later version. +%% OR +%% The 2-clause BSD-style license. +%% +%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause + +\NeedsTeXFormat{LaTeX2e}\relax +\ProvidesPackage{DOF-COL} + [0000/00/00 Unreleased v0.0.0+% + Document-Type Support Framework for Isabelle.] + +\RequirePackage{DOF-core} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: figure* +\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}} +\newisadof{figure.Isa_COL.figure}% +[label=,type=% +,Isa_COL.figure.relative_width=% +,Isa_COL.figure.placement=% +,Isa_COL.figure.src=% +,Isa_COL.figure.spawn_columns=enum False True% +][1]{% + \begin{figure}[] + \centering + \ifcommandkey{Isa_COL.figure.relative_width} + {% + \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}} + \gdef\dof@src{\commandkey{Isa_COL.figure.src}} + \FPdiv\scale{\dof@width}{100}% + \includegraphics[width=\scale\textwidth]{\dof@src}% + }{% + \gdef\dof@src{\commandkey{Isa_COL.figure.src}} + \includegraphics[]{\dof@src}% + } + \caption{#1}\label{\commandkey{label}}% + \end{figure} +} +% end: figure* +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: side_by_side_figure* +\NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}} +\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}% +[label=,type=% +,Isa_COL.figure.relative_width=% +,Isa_COL.figure.src=% +,Isa_COL.side_by_side_figure.anchor=% +,Isa_COL.side_by_side_figure.caption=% +,Isa_COL.side_by_side_figure.relative_width2=% +,Isa_COL.side_by_side_figure.src2=% +,Isa_COL.side_by_side_figure.anchor2=% +,Isa_COL.side_by_side_figure.caption2=% +,Isa_COL.side_by_side_figure.placement=% +,Isa_COL.side_by_side_figure.spawn_columns=enum False True% +][1]{% + \begin{figure}[] + \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]% + {\ifcommandkey{Isa_COL.figure.relative_width}% + {% + \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}} + \gdef\dof@src{\commandkey{Isa_COL.figure.src}} + \FPdiv\scale{\dof@width}{100}% + \includegraphics[width=\scale\textwidth]{\dof@src}% + }{% + \gdef\dof@src{\commandkey{Isa_COL.figure.src}} + \includegraphics[]{\dof@src}% + }% + }% + \hfill% + \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor2}}\commandkey{Isa_COL.side_by_side_figure.caption2}]% + {\ifcommandkey{Isa_COL.side_by_side_figure.relative_width2}% + {% + \gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}} + \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}} + \FPdiv\scale{\dof@width}{100}% + \includegraphics[width=\scale\textwidth]{\dof@src}% + }{% + \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}} + \includegraphics[]{\dof@src}% + }% + }% + \caption{#1}\label{\commandkey{label}}% + \end{figure} +} +% end: side_by_side_figure* +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/document-generator/latex/DOF-core.sty b/document-generator/latex/DOF-core.sty index 0e60e40..9932644 100644 --- a/document-generator/latex/DOF-core.sty +++ b/document-generator/latex/DOF-core.sty @@ -35,141 +35,90 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: generic dispatcher -\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{% +\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,level=,type={dummyT},args={}][1]{% \ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname% \csname isaDof.\commandkey{env}.\commandkey{type}\endcsname% [label=\commandkey{label},\commandkey{args}]{#1}% \else% - \errmessage{Isabelle/DOF: No LaTeX representation for concept - "\commandkey{env}.\commandkey{type}" defined:} - + \message{Isabelle/DOF: Using default LaTeX representation for concept % + "\commandkey{env}.\commandkey{type}".}% + \ifcsname isaDof.\commandkey{env}\endcsname% + \csname isaDof.\commandkey{env}\endcsname% + [label=\commandkey{label}]{#1}% + \else% + \errmessage{Isabelle/DOF: No LaTeX representation for concept % + "\commandkey{env}.\commandkey{type}" defined and no default % + definition for "\commandkey{env}" available either.}% + \fi% \fi% } % end: generic dispatcher %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: text.text -\newisadof{text.text}% -[label=,type=% -][1]{% +% begin: text*-dispatcher +\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} +% end: text*-dispatcher +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: chapter*-dispatcher +\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}} +% end: chapter*-dispatcher +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: section*-dispatcher +\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}} +% end: section*-dispatcher +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: subsection*-dispatcher +\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}} +% end: subsection*-dispatcher +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: subsubsection*-dispatcher +\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}} +% end: subsubsection*-dispatcher +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: paragraph*-dispatcher +\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={paragraph},#1]{\BODY}} +% end: paragraph*-dispatcher +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: text default implementation +\newisadof{text}[label=,type=][1]{% \begin{isamarkuptext}% #1 \end{isamarkuptext}% } -% begin: text.text +% end: text default implementation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: figure* -\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}} -\newisadof{figure.Isa_COL.figure}% -[label=,type=% -,Isa_COL.figure.relative_width=% -,Isa_COL.figure.placement=% -,Isa_COL.figure.src=% -,Isa_COL.figure.spawn_columns=enum False True% -][1]{% - \begin{figure}[] - \centering - \ifcommandkey{Isa_COL.figure.relative_width} - {% - \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}} - \gdef\dof@src{\commandkey{Isa_COL.figure.src}} - \FPdiv\scale{\dof@width}{100}% - \includegraphics[width=\scale\textwidth]{\dof@src}% - }{% - \gdef\dof@src{\commandkey{Isa_COL.figure.src}} - \includegraphics[]{\dof@src}% - } - \caption{#1}\label{\commandkey{label}}% - \end{figure} +% begin: chapter/section default implementations +\newisadof{chapter}[label=,type=][1]{% + \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% } -% end: figure* -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: side_by_side_figure* -\NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}} -\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}% -[label=,type=% -,Isa_COL.figure.relative_width=% -,Isa_COL.figure.src=% -,Isa_COL.side_by_side_figure.anchor=% -,Isa_COL.side_by_side_figure.caption=% -,Isa_COL.side_by_side_figure.relative_width2=% -,Isa_COL.side_by_side_figure.src2=% -,Isa_COL.side_by_side_figure.anchor2=% -,Isa_COL.side_by_side_figure.caption2=% -,Isa_COL.side_by_side_figure.placement=% -,Isa_COL.side_by_side_figure.spawn_columns=enum False True% -][1]{% - \begin{figure}[] - \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]% - {\ifcommandkey{Isa_COL.figure.relative_width}% - {% - \gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}} - \gdef\dof@src{\commandkey{Isa_COL.figure.src}} - \FPdiv\scale{\dof@width}{100}% - \includegraphics[width=\scale\textwidth]{\dof@src}% - }{% - \gdef\dof@src{\commandkey{Isa_COL.figure.src}} - \includegraphics[]{\dof@src}% - }% - }% - \hfill% - \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor2}}\commandkey{Isa_COL.side_by_side_figure.caption2}]% - {\ifcommandkey{Isa_COL.side_by_side_figure.relative_width2}% - {% - \gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}} - \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}} - \FPdiv\scale{\dof@width}{100}% - \includegraphics[width=\scale\textwidth]{\dof@src}% - }{% - \gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}} - \includegraphics[]{\dof@src}% - }% - }% - \caption{#1}\label{\commandkey{label}}% - \end{figure} +\newisadof{section}[label=,type=][1]{% + \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% } -% end: side_by_side_figure* +\newisadof{subsection}[label=,type=][1]{% + \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% +} +\newisadof{subsubsection}[label=,type=][1]{% + \isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% +} +\newisadof{paragraph}[label=,type=][1]{% + \isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue% +} +% end: chapter/section default implementations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: Text* -\NewEnviron{isamarkupText*}[1][]{\isaDof[env={Text},#1]{\BODY}} -% end: Text* -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: text* -\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} -% end: text* -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newkeycommand\isaDofOpenMonitor[label=,type=]{} -\newkeycommand\isaDofCloseMonitor[label=,type=]{} - -\newkeycommand\isaDofDeclareReferenceTextSection[label=,type=]{} -\newkeycommand\isaDofDeclareReferenceFigure[label=,type=]{} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: chapter* -\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}} -% end: chapter* -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: section* -\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}} -% end: section* -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: subsection* -\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}} -% end: subsection* -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/document-generator/latex/DOF-mathex.sty b/document-generator/latex/DOF-mathex.sty index 0643471..48b0b85 100644 --- a/document-generator/latex/DOF-mathex.sty +++ b/document-generator/latex/DOF-mathex.sty @@ -16,7 +16,7 @@ [0000/00/00 Unreleased v0.0.0+% Document-Type Support Framework for math classes.] -\RequirePackage{DOF-core} +\RequirePackage{DOF-COL} \usepackage{sfmath} \usepackage{amsmath} \usepackage{lastpage} diff --git a/document-generator/latex/DOF-scholarly_paper.sty b/document-generator/latex/DOF-scholarly_paper.sty index 59fc16f..e6405a2 100644 --- a/document-generator/latex/DOF-scholarly_paper.sty +++ b/document-generator/latex/DOF-scholarly_paper.sty @@ -16,7 +16,7 @@ [0000/00/00 Unreleased v0.0.0+% Document-Type Support Framework for Isabelle (LNCS).] -\RequirePackage{DOF-core} +\RequirePackage{DOF-COL} \RequirePackage{ifthen} \RequirePackage{ifthen} @@ -153,10 +153,15 @@ \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% } \newisadof{subsection.scholarly_paper.introduction}% -[label=,type=% +[label=,type=,level=% +,scholarly_paper.level=% +,scholarly_paper.introduction.level=% ,scholarly_paper.introduction.main_author=% ,scholarly_paper.introduction.fixme_list=% ][1]{% + \typeout{L1: \commandkey{level}} + \typeout{L2: \commandkey{scholarly_paper.level}} + \typeout{L3: \commandkey{scholarly_paper.introdution.level}} \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% } \newisadof{text.scholarly_paper.introduction_elem}% From 57923ad393ebefd60bf5cb9d102da98b5a03f5df Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 31 Mar 2019 00:14:47 +0000 Subject: [PATCH 5/9] Removed all definitions that are semantically equivalent to their default variant. --- .../latex/DOF-CENELEC_50128.sty | 66 --------- .../latex/DOF-scholarly_paper.sty | 126 ------------------ .../latex/DOF-technical_report.sty | 73 ---------- 3 files changed, 265 deletions(-) diff --git a/document-generator/latex/DOF-CENELEC_50128.sty b/document-generator/latex/DOF-CENELEC_50128.sty index ad5f5e4..edb734b 100644 --- a/document-generator/latex/DOF-CENELEC_50128.sty +++ b/document-generator/latex/DOF-CENELEC_50128.sty @@ -17,69 +17,3 @@ Document-Type Support Framework for Isabelle (CENELEC 50128).] \RequirePackage{DOF-COL} - - -\newkeycommand\isaDofSectionRequirement[label=,type=,main_author=,long_name=][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} - -\newkeycommand\isaDofSubSectionRequirement[label=,type=,main_author=,long_name=][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} - -\newkeycommand\isaDofSectionInterface[label=,type=,main_author=,kind=][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} - - -\newkeycommand\isaDofTextEc[label=,type=,assumption=][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} - -\newkeycommand\isaDofTextSrac[label=,type=,assumption=][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} - -\newisadof{text.CENELEC_50128.assumption}% -[label=,type=,assumption=][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} - -\newisadof{text.CENELEC_50128.hypothesis}% -[label=,type=,assumption=][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} - -\newisadof{text.CENELEC_50128.srac}% -[label=,type=,assumption=][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} -\newisadof{text.CENELEC_50128.ec}% -[label=,type=,assumption=][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} -\newisadof{text.CENELEC_50128.test_result}% -[label=,type=,assumption=][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} - -\newisadof{text.CENELEC_50128.SRAC}% -[label=,type=,assumption=][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} diff --git a/document-generator/latex/DOF-scholarly_paper.sty b/document-generator/latex/DOF-scholarly_paper.sty index e6405a2..833765a 100644 --- a/document-generator/latex/DOF-scholarly_paper.sty +++ b/document-generator/latex/DOF-scholarly_paper.sty @@ -142,129 +142,3 @@ } % end: scholarly_paper.abstract %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.introduction -\newisadof{section.scholarly_paper.introduction}% -[label=,type=% -,scholarly_paper.introduction.main_author=% -,scholarly_paper.introduction.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -\newisadof{subsection.scholarly_paper.introduction}% -[label=,type=,level=% -,scholarly_paper.level=% -,scholarly_paper.introduction.level=% -,scholarly_paper.introduction.main_author=% -,scholarly_paper.introduction.fixme_list=% -][1]{% - \typeout{L1: \commandkey{level}} - \typeout{L2: \commandkey{scholarly_paper.level}} - \typeout{L3: \commandkey{scholarly_paper.introdution.level}} - \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -\newisadof{text.scholarly_paper.introduction_elem}% -[label=,type=% -,scholarly_paper.introduction.main_author=% -,scholarly_paper.introduction.fixme_list=% -][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} -\newisadof{text.scholarly_paper.introduction}% -[label=,type=% -,scholarly_paper.introduction.main_author=% -,scholarly_paper.introduction.fixme_list=% -][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} -% end: scholarly_paper.introduction -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.introduction -\newisadof{section.scholarly_paper.text_section}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.introduction -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.technical -\newisadof{section.scholarly_paper.technical}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -\newisadof{subsection.scholarly_paper.technical}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.technical -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.example -\newisadof{section.scholarly_paper.example}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -\newisadof{subsection.scholarly_paper.example}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.example -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.conclusion -\newisadof{section.scholarly_paper.conclusion}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.conclusion -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.conclusion -\newisadof{subsection.scholarly_paper.conclusion}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.conclusion -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.bibliography -\newisadof{section.scholarly_paper.bibliography}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.bibliography diff --git a/document-generator/latex/DOF-technical_report.sty b/document-generator/latex/DOF-technical_report.sty index ca5928e..0c4edf3 100644 --- a/document-generator/latex/DOF-technical_report.sty +++ b/document-generator/latex/DOF-technical_report.sty @@ -28,76 +28,3 @@ }{% {\PackageError{DOF-scholarly_paper}{Scholarly Paper only supports LNCS or scrartcl as document class.}{}\stop}% } - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.introduction -\newisadof{chapter.scholarly_paper.introduction}% -[label=,type=% -,scholarly_paper.introduction.main_author=% -,scholarly_paper.introduction.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.introduction -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.introduction -\newisadof{chapter.scholarly_paper.text_section}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.introduction -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.technical -\newisadof{chapter.scholarly_paper.technical}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.technical -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.example -\newisadof{chapter.scholarly_paper.example}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.example -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% begin: scholarly_paper.conclusion -\newisadof{chapter.scholarly_paper.conclusion}% -[label=,type=% -,scholarly_paper.text_section.main_author=% -,scholarly_paper.text_section.fixme_list=% -][1]{% - \isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue% -} -% end: scholarly_paper.conclusion -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -\newisadof{text.technical_report.front_matter}% -[label=,type=% -,scholarly_paper.introduction.main_author=% -,scholarly_paper.introduction.fixme_list=% -][1]{% - \begin{isamarkuptext}% - #1 - \end{isamarkuptext}% -} -% end: scholarly_paper.introduction From 9edb3442184059c944338523528d61d8cb130492 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 31 Mar 2019 13:34:52 +0100 Subject: [PATCH 6/9] Added generic type hook. --- document-generator/latex/DOF-core.sty | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/document-generator/latex/DOF-core.sty b/document-generator/latex/DOF-core.sty index 9932644..37e000e 100644 --- a/document-generator/latex/DOF-core.sty +++ b/document-generator/latex/DOF-core.sty @@ -35,7 +35,11 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: generic dispatcher -\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,level=,type={dummyT},args={}][1]{% +\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{% + \ifcsname isaDof.\commandkey{type}\endcsname% + \csname isaDof.\commandkey{type}\endcsname% + [label=\commandkey{label},\commandkey{args}]{#1}% + \else\relax\fi% \ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname% \csname isaDof.\commandkey{env}.\commandkey{type}\endcsname% [label=\commandkey{label},\commandkey{args}]{#1}% From 0daaf3d699093cdebc68b2b0536854d8b1c924c4 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 31 Mar 2019 14:08:52 +0100 Subject: [PATCH 7/9] Bug fix: subsubsection was mapped to subsection. --- document-generator/latex/DOF-core.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document-generator/latex/DOF-core.sty b/document-generator/latex/DOF-core.sty index 37e000e..0f96121 100644 --- a/document-generator/latex/DOF-core.sty +++ b/document-generator/latex/DOF-core.sty @@ -85,7 +85,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: subsubsection*-dispatcher -\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}} +\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={subsubsection},#1]{\BODY}} % end: subsubsection*-dispatcher %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% From c3409d1f107529e8eff877aa2a29af6d66a160ac Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 31 Mar 2019 15:13:27 +0100 Subject: [PATCH 8/9] Cleanup: moved outdated code for exporting LaTeX style files into a dedicated functions and disabled file output. --- Isa_DOF.thy | 118 +++++++++++++++++++++------------------------------- 1 file changed, 48 insertions(+), 70 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 7270595..f8ab490 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -13,7 +13,8 @@ text\ Offering \<^item> LaTeX support. \ text\ In this section, we develop on the basis of a management of references Isar-markups -that provide direct support in the PIDE framework. \ +that provide direct support in the PIDE framework. \ + theory Isa_DOF (* Isabelle Document Ontology Framework *) imports Main @@ -636,46 +637,6 @@ val _ = Toplevel.keep (check_doc_global b o Toplevel.context_of))); -fun toStringLaTeXNewKeyCommand env long_name = - "\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n" - -fun toStringMetaArgs true attr_long_names = - enclose "[" "][1]" (commas ("label=,type=%\n" :: attr_long_names)) - |toStringMetaArgs false attr_long_names = - enclose "[" "][1]" (commas attr_long_names) - -fun toStringDocItemBody env = - enclose "{%\n\\isamarkupfalse\\isamarkup" - "{#1}\\label{\\commandkey{label}}\\isamarkuptrue%\n}\n" - env - -fun toStringDocItemCommand env long_name attr_long_names = - toStringLaTeXNewKeyCommand env long_name ^ - toStringMetaArgs true attr_long_names ^ - toStringDocItemBody env ^"\n" - -fun toStringDocItemLabel long_name attr_long_names = - toStringLaTeXNewKeyCommand "Label" long_name ^ - toStringMetaArgs false attr_long_names ^ - "{%\n\\autoref{#1}\n}\n" - -fun toStringDocItemRef long_name label attr_long_namesNvalues = - "\\isaDof.Label." ^ long_name ^ - enclose "[" "]" (commas attr_long_namesNvalues) ^ - enclose "{" "}" label - -fun write_file thy filename content = - let - val filename = Path.explode filename - val master_dir = Resources.master_directory thy - val abs_filename = if (Path.is_absolute filename) - then filename - else Path.append master_dir filename - in - File.write (abs_filename) content - handle (IO.Io{name=name,...}) - => warning ("Could not write \""^(name)^"\".") - end fun write_ontology_latex_sty_template thy = let @@ -688,6 +649,48 @@ fun write_ontology_latex_sty_template thy = *) val curr_thy_name = Context.theory_name thy val {docobj_tab={tab = x, ...},docclass_tab,...}= get_data_global thy; + + fun toStringLaTeXNewKeyCommand env long_name = + "\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n" + + fun toStringMetaArgs true attr_long_names = + enclose "[" "][1]" (commas ("label=,type=%\n" :: attr_long_names)) + |toStringMetaArgs false attr_long_names = + enclose "[" "][1]" (commas attr_long_names) + + fun toStringDocItemBody env = + enclose "{%\n\\isamarkupfalse\\isamarkup" + "{#1}\\label{\\commandkey{label}}\\isamarkuptrue%\n}\n" + env + + fun toStringDocItemCommand env long_name attr_long_names = + toStringLaTeXNewKeyCommand env long_name ^ + toStringMetaArgs true attr_long_names ^ + toStringDocItemBody env ^"\n" + + fun toStringDocItemLabel long_name attr_long_names = + toStringLaTeXNewKeyCommand "Label" long_name ^ + toStringMetaArgs false attr_long_names ^ + "{%\n\\autoref{#1}\n}\n" + + fun toStringDocItemRef long_name label attr_long_namesNvalues = + "\\isaDof.Label." ^ long_name ^ + enclose "[" "]" (commas attr_long_namesNvalues) ^ + enclose "{" "}" label + + fun write_file thy filename content = + let + val filename = Path.explode filename + val master_dir = Resources.master_directory thy + val abs_filename = if (Path.is_absolute filename) + then filename + else Path.append master_dir filename + in + File.write (abs_filename) content + handle (IO.Io{name=name,...}) + => warning ("Could not write \""^(name)^"\".") + end + fun write_attr (n, ty, _) = YXML.content_of(Binding.print n)^ "=\n" fun write_class (n, {attribute_decl,id,inherits_from,name,params,thy_name,rex,rejectS}) = @@ -699,8 +702,10 @@ fun write_ontology_latex_sty_template thy = else "" val content = String.concat(map write_class (Symtab.dest docclass_tab)) (* val _ = writeln content -- for interactive testing only, breaks LaTeX compilation *) - in write_file thy ("Isa-DOF."^curr_thy_name^".template.sty") content - end; + in + warning("LaTeX Style file generation not supported.") + (* write_file thy ("Isa-DOF."^curr_thy_name^".template.sty") content *) + end val _ = @@ -1696,31 +1701,4 @@ val _ = end (* struct *) \ - -section\ Testing and Validation \ - -(* the f ollowing test crashes the LaTeX generation - however, without the latter this output is - instructive -ML\ -writeln (DOF_core.toStringDocItemCommand "section" "scholarly_paper.introduction" []); -writeln (DOF_core.toStringDocItemLabel "scholarly_paper.introduction" []); -writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []); - -(DOF_core.write_ontology_latex_sty_template @{theory}) -\ -*) - - -ML\ - -\ -(* -ML\ -val h = bstring_to_holstring @{context} (Syntax.string_of_term @{context} @{term "A \ A"}); -holstring_to_bstring @{context} h -\ -*) - - - end From 9d7ebc4a4f026ac1ae146b84ba31ec63483fe391 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 31 Mar 2019 17:47:10 +0100 Subject: [PATCH 9/9] Enabled passing of default arguments to LaTeX backend. --- Isa_DOF.thy | 27 ++++++++++++------- document-generator/latex/DOF-COL.sty | 2 +- .../latex/DOF-scholarly_paper.sty | 5 ++-- 3 files changed, 21 insertions(+), 13 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index f8ab490..d30cd8e 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -849,6 +849,8 @@ fun property_list_dest ctxt X = (map (fn Const ("Isa_DOF.ISA_term", _) $ s => HO end; (* struct *) \ + + subsection\ Isar - Setup\ setup\DOF_core.update_isa_global("typ" ,ISA_core.ML_isa_check_typ) \ @@ -873,7 +875,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) = let val l = "label = "^ (enclose "{" "}" lab) val cid_long = case cid_opt of NONE => DOF_core.default_cid - | SOME(cid,_) => DOF_core.name2doc_class_name thy cid + | SOME(cid,_) => DOF_core.name2doc_class_name thy cid val cid_txt = "type = " ^ (enclose "{" "}" cid_long); fun ltx_of_term _ (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t') @@ -885,9 +887,8 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) = ) | ltx_of_term ctxt t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t) fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) (Symbol.explode (YXML.content_of s))) - fun ltx_of_markup s = let - val ctxt = Proof_Context.init_global thy - val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s + fun ltx_of_markup ctxt s = let + val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s val str_of_term = ltx_of_term ctxt term handle _ => "Exception in ltx_of_term" (* For debugging: @@ -903,12 +904,18 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) = end fun toLong n = #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy)) - fun str ((lhs,_),rhs) = (toLong lhs)^" = "^(enclose "{" "}" (ltx_of_markup rhs)) - (* no normalization on lhs (could be long-name) - no paraphrasing on rhs (could be fully paranthesized - pretty-printed formula in LaTeX notation ... *) - in - (enclose "[" "]" (String.concat [ cid_txt, ", args={", (commas ([cid_txt,l] @ (map str attr_list ))), "}"])) + val ctxt = Proof_Context.init_global thy + val actual_args = map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs)) + attr_list + val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), ltx_of_term ctxt t)) + (DOF_core.get_attribute_defaults cid_long thy) + + val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a) + (map (fn (c,_) => c) actual_args))) default_args + val str_args = map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs)) + (actual_args@default_args_filtered) + in + (enclose "[" "]" (String.concat [ cid_txt, ", args={", (commas str_args), "}"])) end val semi = Scan.option (Parse.$$$ ";"); diff --git a/document-generator/latex/DOF-COL.sty b/document-generator/latex/DOF-COL.sty index a77ae44..088dbc8 100644 --- a/document-generator/latex/DOF-COL.sty +++ b/document-generator/latex/DOF-COL.sty @@ -62,7 +62,7 @@ ,Isa_COL.side_by_side_figure.anchor2=% ,Isa_COL.side_by_side_figure.caption2=% ,Isa_COL.side_by_side_figure.placement=% -,Isa_COL.side_by_side_figure.spawn_columns=enum False True% +,Isa_COL.figure.spawn_columns=enum False True% ][1]{% \begin{figure}[] \subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]% diff --git a/document-generator/latex/DOF-scholarly_paper.sty b/document-generator/latex/DOF-scholarly_paper.sty index 833765a..2ce0bcb 100644 --- a/document-generator/latex/DOF-scholarly_paper.sty +++ b/document-generator/latex/DOF-scholarly_paper.sty @@ -54,7 +54,7 @@ \NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}} \newisadof{title.scholarly_paper.title}% [label=,type=% -,keywordlist=% +,scholarly_paper.title.short_title=% ][1]{% \immediate\write\@auxout{\noexpand\title{#1}}% } @@ -66,7 +66,7 @@ \NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}} \newisadof{subtitle.scholarly_paper.subtitle}% [label=,type=% -,keywordlist=% +,scholarly_paper.subtitle.abbrev=% ][1]{% \immediate\write\@auxout{\noexpand\subtitle{#1}}% } @@ -111,6 +111,7 @@ ,scholarly_paper.author.email=% ,scholarly_paper.author.affiliation=% ,scholarly_paper.author.orcid=% +,scholarly_paper.author.http_site=% ][1]{% \stepcounter{dof@cnt@author} \def\dof@a{\commandkey{scholarly_paper.author.affiliation}}