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

Basic convertion to a setup without the Scala converter.

This commit is contained in:
Achim D. Brucker 2018-09-18 14:29:54 +01:00
parent 85f332fe5e
commit 42b993c289
2 changed files with 208 additions and 136 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

156
document-generator/latex/DOF-core.sty
View File

@ -17,87 +17,113 @@
Document-Type Support Framework for Isabelle.]
\RequirePackage{keycommand}
\RequirePackage{environ}
\RequirePackage{graphicx}
\RequirePackage{fp}
\newkeycommand\isaDofChapter[label=,type=][1]{%
\isamarkupchapter{#1}\label{\commandkey{label}}%
}
\newkeycommand\isaDofSection[label=,type=][1]{%
\isamarkupsection{#1}\label{\commandkey{label}}%
}
\newkeycommand\isaDofSubSection[label=,type=][1]{%
\isamarkupsubsection{#1}\label{\commandkey{label}}%
}
\newkeycommand\isaDofSubSubSection[label=,type=][1]{%
\isamarkupsubsubsection{#1}\label{\commandkey{label}}%
}
\newkeycommand\isaDofParagraph[label=,type=][1]{%
\isamarkupparagraph{#1}\label{\commandkey{label}}%
}
\newkeycommand\isaDofSubParagraph[label=,type=][1]{%
\isamarkupsubparagraph{#1}\label{\commandkey{label}}%
% Generic dispatcher
\newkeycommand+[\|]\isaDof[label=,type=,args={}][1]{%
\csname isaDof\commandkey{type}\endcsname[label=\commandkey{label},\commandkey{args}]{#1}%
}
\newkeycommand\isaDofFigure
[label=,type=,relative_width=,placement=,src=,spawn_columns=enum False True][1]{%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: figure*
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[#1]{\BODY}}
\expandafter\newkeycommand\csname isaDofIsa_DOF.figure\endcsname%
[label=,type=%
,Isa_DOF.figure.relative_width=%
,Isa_DOF.figure.placement=%
,Isa_DOF.figure.src=%
,Isa_DOF.figure.spawn_columns=enum False True%
][1]{%
% TODO:
% \begin{figure}[]
% \centering
% \ifcommandkey{Isa_DOF.figure.relative_width}
% {%
% \FPdiv\scale{\commandkey{Isa_DOF.figure.relative_width}}{100}
% \includegraphics[width=\scale\textwidth]{\commandkey{Isa_DOF.figure.src}}
% }{%
% \includegraphics[]{\commandkey{Isa_DOF.figure.src}}
% }
% \caption{#1}\label{\commandkey{Isa_DOF.figure.label}}%
% \end{figure}
}
% end: figure*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: side_by_side_figure*
\NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[#1]{\BODY}}
\expandafter\newkeycommand\csname isaDofIsa_DOF.side_by_side_figure\endcsname%
[label=,type=%
,Isa_DOF.figure.relative_width=%
,Isa_DOF.figure.src=%
,Isa_DOF.side_by_side_figure.anchor=%
,Isa_DOF.side_by_side_figure.caption=%
,Isa_DOF.side_by_side_figure.relative_width2=%
,Isa_DOF.side_by_side_figure.src2=%
,Isa_DOF.side_by_side_figure.anchor2=%
,Isa_DOF.side_by_side_figure.caption2=%
,Isa_DOF.side_by_side_figure.placement=%
,Isa_DOF.side_by_side_figure.spawn_columns=enum False True%
][1]{%
\begin{figure}[]
\centering
\ifcommandkey{relative_width}
{%
\FPdiv\scale{\commandkey{relative_width}}{100}
\includegraphics[width=\scale\textwidth]{\commandkey{src}}
}{%
\includegraphics[]{\commandkey{src}}
}
\caption{#1}\label{\commandkey{label}}%
% TODO
% \subfloat[\label{\commandkey{anchor}}\commandkey{caption}]%
% {\ifcommandkey{relative_width}%
% {%
% \FPdiv\scale{\commandkey{relative_width}}{100}%
% \includegraphics[width=\scale\textwidth]{\commandkey{src}}%
% }{%
% \includegraphics[]{\commandkey{src}}%
% }%
% }%
% \hfill%
% \subfloat[\label{\commandkey{anchor2}}\commandkey{caption2}]%
% {\ifcommandkey{relative_width2}%
% {%
% \FPdiv\scale{\commandkey{relative_width2}}{100}%
% \includegraphics[width=\scale\textwidth]{\commandkey{src2}}%
% }{%
% \includegraphics[]{\commandkey{src2}}%
% }%
% }%
% \caption{#1}\label{\commandkey{label}}%
\end{figure}
}
% end: side_by_side_figure*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newkeycommand\isaDofDeclareReferenceFigure[label=,type=]{}
\newkeycommand\isaDofSideBySideFigure
[label=,type=
,relative_width=,src=,anchor=,caption=,
,relative_width2=,src2=,anchor2=,caption2=,
,placement=,spawn_columns=enum False True][1]{%
\begin{figure}[]
\subfloat[\label{\commandkey{anchor}}\commandkey{caption}]%
{\ifcommandkey{relative_width}%
{%
\FPdiv\scale{\commandkey{relative_width}}{100}%
\includegraphics[width=\scale\textwidth]{\commandkey{src}}%
}{%
\includegraphics[]{\commandkey{src}}%
}%
}%
\hfill%
\subfloat[\label{\commandkey{anchor2}}\commandkey{caption2}]%
{\ifcommandkey{relative_width2}%
{%
\FPdiv\scale{\commandkey{relative_width2}}{100}%
\includegraphics[width=\scale\textwidth]{\commandkey{src2}}%
}{%
\includegraphics[]{\commandkey{src2}}%
}%
}%
\caption{#1}\label{\commandkey{label}}%
\end{figure}
}
\newkeycommand\isaDofText[label=][1]{%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: Text*
\NewEnviron{isamarkupText*}[1][]{\isaDof[#1]{\BODY}}
\newkeycommand\isaDofText[label=,type=][1]{%
\begin{isamarkuptext}%
#1
\end{isamarkuptext}%
}
% end: Text*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newkeyenvironment{isamarkupText*}[label=][0]
\newenvironment{isamarkupText*}%[][0]
{\par\isastyletext\begin{isapar}}
{\end{isapar}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: text*
\NewEnviron{isamarkuptext*}[1][]{\isaDof[#1]{\BODY}}
\newkeycommand\isaDoftext[label=,type=][1]{%
\begin{isamarkuptext}%
#1
\end{isamarkuptext}%
}
% end: text*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newkeycommand\isaDofOpenMonitor[label=,type=]{}
\newkeycommand\isaDofCloseMonitor[label=,type=]{}
\newkeycommand\isaDofDeclareReferenceTextSection[label=,type=]{}
\newkeycommand\isaDofDeclareReferenceFigure[label=,type=]{}
\NewEnviron{isamarkupsection*}[1][]{\isaDof[#1]{\BODY}}
\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[#1]{\BODY}}

188
document-generator/latex/DOF-scholarly_paper.sty
View File

@ -18,6 +18,8 @@
\RequirePackage{DOF-core}
\RequirePackage{ifthen}
\@ifclassloaded{llncs}%
{}%
{%
@ -31,79 +33,40 @@
{\PackageError{DOF-scholarly_paper}{Scholarly Paper only supports LNCS or scrartcl as document class.}{}\stop}%
}
\newkeycommand\isaDofSectionIntroduction[label=,type=,main_author=,fixme_list=][1]{%
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: title*
\NewEnviron{isamarkuptitle*}[1][]{\isaDof[#1]{\BODY}}
\expandafter\newkeycommand\csname isaDofscholarly_paper.title\endcsname%
[label=,type=%
,keywordlist=%
][1]{%
\immediate\write\@auxout{\noexpand\title{#1}}%
}
% end: title*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newkeycommand\isaDofSectionExample[label=,type=,main_author=,fixme_list=][1]{%
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSectionTechnical[label=,type=,main_author=,fixme_list=][1]{%
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSectionConclusion[label=,type=,main_author=,fixme_list=][1]{%
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSectionTextSection[label=,type=,main_author=,text_section.main_author=,fixme_list=][1]{%
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSectionRelatedWork[label=,type=,main_author=,fixme_list=][1]{%
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSubSectionIntroduction[label=,type=][1]{%
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSubsectionExample[label=,type=][1]{%
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSubsectionTechnical[label=,type=][1]{%
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSubSectionConclusion[label=,type=][1]{%
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSubSectionTextSection[label=,type=,main_author=,text_section.main_author=,fixme_list=][1]{%
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofSubSectionRelatedwork[label=,type=,main_author=,fixme_list=][1]{%
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newkeycommand\isaDofTextIntroduction[label=,type=,keywordlist=][1]{%
\begin{isamarkuptext}%
#1
\end{isamarkuptext}%
}
\newkeycommand\isaDofTextAbstract[label=,type=,keywordlist=][1]{%
\begin{isamarkuptext}%
\begin{abstract}%
#1%
\ifthenelse{\equal{\commandkey{keywordlist}}{}}{}{%
\mbox{}\\\medskip\noindent{\textbf{Keywords:}} \commandkey{keywordlist}%
}%
\end{abstract}%
\end{isamarkuptext}%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: subtitle*
\NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[#1]{\BODY}}
\expandafter\newkeycommand\csname isaDofscholarly_paper.subtitle\endcsname%
[label=,type=%
,keywordlist=%
][1]{%
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
}
% end: subtitle*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.author
\def\dof@author{}%
\def\dof@affiliation{}%
\AtBeginDocument{%
\author{\dof@author}
\institute{\dof@affiliation}
}
}
\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}}
\def\leftaddaux#1#2#3{\gdef#3{#1#2}}
@ -125,21 +88,104 @@
}
}
\newkeycommand\isaDofTextAuthor[label=,type=,email=,affiliation=,orcid=][1]{%
\expandafter\newkeycommand\csname isaDofscholarly_paper.author\endcsname%
[label=,type=%
,scholarly_paper.author.email=%
,scholarly_paper.author.affiliation=%
,scholarly_paper.author.orcid=%
][1]{%
\stepcounter{dof@cnt@author}
\def\dof@a{\commandkey{affiliation}}
\ifthenelse{\equal{\commandkey{orcid}}{}}{%
\def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
\ifthenelse{\equal{\commandkey{scholarly_paper.author.orcid}}{}}{%
\immediate\write\@auxout{\noexpand\addauthor{#1\noexpand\inst{\thedof@cnt@author}}}%
}{%
\immediate\write\@auxout{\noexpand\addauthor{#1\noexpand\inst{\thedof@cnt@author}\orcidID{\commandkey{orcid}}}}%
\immediate\write\@auxout{\noexpand\addauthor{#1\noexpand\inst{\thedof@cnt@author}\orcidID{\commandkey{scholarly_paper.author.orcid}}}}%
}
\protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{email}}}}%
\protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{scholarly_paper.author.email}}}}%
}
% end: scholarly_paper.author
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newkeycommand\isaDofSubtitle[label=,type=,keywordlist=][1]{%
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.abstract
\expandafter\newkeycommand\csname isaDofscholarly_paper.abstract\endcsname%
[label=,type=%
,scholarly_paper.abstract.keywordlist=%
][1]{%
\begin{isamarkuptext}%
\begin{abstract}%
#1%
\ifthenelse{\equal{\commandkey{scholarly_paper.abstract.keywordlist}}{}}{}{%
\mbox{}\\\medskip\noindent{\textbf{Keywords:}} \commandkey{scholarly_paper.abstract.keywordlist}%
}%
\end{abstract}%
\end{isamarkuptext}%
}
% end: scholarly_paper.abstract
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newkeycommand\isaDofTitle[label=,type=,keywordlist=][1]{%
\immediate\write\@auxout{\noexpand\title{#1}}%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.introduction
\expandafter\newkeycommand\csname isaDofscholarly_paper.introduction\endcsname%
[label=,type=%
,scholarly_paper.introduction.main_author=%
,scholarly_paper.introduction.fixme_list=%
][1]{%
\gdef\dof@section#1
\isamarkupfalse\isamarkupsection{\gdef\dof@section#1}\label{\commandkey{label}}\isamarkuptrue%
}
% end: scholarly_paper.introduction
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.introduction
\expandafter\newkeycommand\csname isaDofscholarly_paper.text_section\endcsname%
[label=,type=%
,scholarly_paper.text_section.main_author=%
,scholarly_paper.text_section.fixme_list=%
][1]{%
\gdef\dof@section#1
\isamarkupfalse\isamarkupsection{\gdef\dof@section#1}\label{\commandkey{label}}\isamarkuptrue%
}
% end: scholarly_paper.introduction
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.technical
\expandafter\newkeycommand\csname isaDofscholarly_paper.technical\endcsname%
[label=,type=%
,scholarly_paper.text_section.main_author=%
,scholarly_paper.text_section.fixme_list=%
][1]{%
\gdef\dof@section#1
\isamarkupfalse\isamarkupsection{\gdef\dof@section#1}\label{\commandkey{label}}\isamarkuptrue%
}
% end: scholarly_paper.technical
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.example
\expandafter\newkeycommand\csname isaDofscholarly_paper.example\endcsname%
[label=,type=%
,scholarly_paper.text_section.main_author=%
,scholarly_paper.text_section.fixme_list=%
][1]{%
\gdef\dof@section#1
\isamarkupfalse\isamarkupsection{\gdef\dof@section#1}\label{\commandkey{label}}\isamarkuptrue%
}
% end: scholarly_paper.example
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.conclusion
\expandafter\newkeycommand\csname isaDofscholarly_paper.conclusion\endcsname%
[label=,type=%
,scholarly_paper.text_section.main_author=%
,scholarly_paper.text_section.fixme_list=%
][1]{%
\gdef\dof@section#1
\isamarkupfalse\isamarkupsection{\gdef\dof@section#1}\label{\commandkey{label}}\isamarkuptrue%
}
% end: scholarly_paper.conclusion
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%