Add latex compilation material to use bbl file
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2022-04-22 16:08:55 +02:00
parent e69808750c
commit 0cc17a136e
7 changed files with 899 additions and 0 deletions

View File

@ -0,0 +1,99 @@
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Saclay
%% 2019 The University of Exeter
%%
%% 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.3c of the License, or (at your option) any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-COL}
[<isadofltxversion>%
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{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[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.placement=%
,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.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*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

View File

@ -0,0 +1,26 @@
%% Copyright (C) 2021 University of Exeter
%% 2021 University of Paris-Saclay
%%
%% 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.3c of the License, or (at your option) any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-amssymb}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle (amssymb wrapper for lualatex/pdflatex).]
\usepackage{ifxetex,ifluatex}
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
\usepackage{amssymb}
\else % if luatex or xetex
\usepackage{unicode-math}
\usepackage{latexsym}
\fi

View File

@ -0,0 +1,160 @@
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Saclay
%% 2019 The University of Exeter
%%
%% 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.3c of the License, or (at your option) any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-core}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle.]
\RequirePackage{keycommand}
\RequirePackage{environ}
\RequirePackage{graphicx}
\RequirePackage{xspace}
\RequirePackage{etoolbox}
\RequirePackage{fp}
\newcommand{\isabelleurl}{UNDEFINED}
\newcommand{\dofurl}{UNDEFINED}
\newcommand{\dof@isabelleversion}{UNDEFINED}
\newcommand{\isabellefullversion}{UNDEFINED\xspace}
\newcommand{\dof@version}{UNDEFINED}
\newcommand{\dof@artifacturl}{UNDEFINED}
\newcommand{\doflatestversion}{UNDEFINED}
\newcommand{\isadoflatestdoi}{UNDEFINED}
\newcommand{\isadofgenericdoi}{UNDEFINED}
\newcommand{\isabellelatestversion}{Isabelle2019}
%%% CONFIG %%%
\newcommand{\isabelleversion}{\dof@isabelleversion\xspace}
\newcommand{\dofversion}{\dof@version\xspace}
\newcommand{\isadofversion}{\dofversion/\isabelleversion}
\newcommand{\isadoflatestversion}{\doflatestversion/\isabellelatestversion}
\newcommand{\isadofdir}{Isabelle_DOF-\dof@version_\dof@isabelleversion}
\newcommand{\isadofdirn}{Isabelle\_DOF-\dof@version\_\dof@isabelleversion}
\newcommand{\isadofarchive}{\isadofdir.tar.xz}
\newcommand{\isadofarchiven}{\isadofdirn.tar.xz}
\newcommand{\isadofarchiveurl}{\dof@artifacturl/\isadofarchive}
\newcommand{\isadof}{Isabelle/DOF\xspace}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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]{%
\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}%
\else%
\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*-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={subsubsection},#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}\label{\commandkey{label}}%
#1
\end{isamarkuptext}%
}
% end: text default implementation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: chapter/section default implementations
\newisadof{chapter}[label=,type=][1]{%
\isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\newisadof{section}[label=,type=][1]{%
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
}
\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: label and ref
\newisadof{label}[label=,type=][1]{\label{#1}}
\newisadof{ref}[label=,type=][1]{\autoref{#1}}
\newisadof{macroDef}[label=,type=][1]{MMM \label{#1}} %% place_holder
\newisadof{macroExp}[label=,type=][1]{MMM \autoref{#1}} %% place_holder
% end: label and ref
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

View File

@ -0,0 +1,499 @@
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Saclay
%% 2019 The University of Exeter
%%
%% 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.3c of the License, or (at your option) any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-scholarly_paper}
[2021/03/22 Unreleased/Isabelle2021%
Document-Type Support Framework for Isabelle (LNCS).]
\RequirePackage{DOF-COL}
\RequirePackage{ifthen}
\RequirePackage{ifthen}
\newboolean{DOF@scholarlypaper@force}
\DeclareOption{force}{\setboolean{DOF@scholarlypaper@force}{true}}
\ProcessOptions\relax
\ifthenelse{\boolean{DOF@scholarlypaper@force}}{%
}{%
\@ifclassloaded{llncs}%
{}%
{%
\@ifclassloaded{scrartcl}%
{%
\newcommand{\institute}[1]{}%
\newcommand{\inst}[1]{}%
\newcommand{\orcidID}[1]{}%
\newcommand{\email}[1]{}%
\RequirePackage{DOF-scholarly_paper-thm}%
}%
{%
\@ifclassloaded{lipics-v2021}%
{%
\newcommand{\institute}[1]{}%
\newcommand{\inst}[1]{}%
\newcommand{\orcidID}[1]{}%
\newcommand{\email}[1]{}%
}%
{%
{%
\@ifclassloaded{eptcs}%
{%
\newcommand{\inst}[1]{}%
\newcommand{\orcidID}[1]{}%
}%
{%
\@ifclassloaded{svjour3}%
{%
\newcommand{\inst}[1]{}%
}%
{%
\PackageError{DOF-scholarly_paper}
{Scholarly Paper only supports LNCS or scrartcl as document class.}
{}\stop%
}%
}%
}%
}%
}
}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: title*
\NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}}
\newisadof{title.scholarly_paper.title}%
[label=,type=%
,scholarly_paper.title.short_title=%
][1]{%
\immediate\write\@auxout{\noexpand\title{#1}}%
}
% end: title*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: subtitle*
\NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}}
\newisadof{subtitle.scholarly_paper.subtitle}%
[label=,type=%
,scholarly_paper.subtitle.abbrev=%
][1]{%
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
}
% end: subtitle*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.author
\def\dof@author{}%
\def\dof@affiliation{}%
\newcommand{\DOFauthor}{\author{\dof@author}}
\newcommand{\DOFinstitute}{\institute{\dof@affiliation}}
\AtBeginDocument{%
\DOFauthor
\DOFinstitute
}
\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}}
\def\leftaddaux#1#2#3{\gdef#3{#1#2}}
\newcounter{dof@cnt@author}
\newcommand{\addauthor}[1]{%
\ifthenelse{\equal{\dof@author}{}}{%
\gdef\dof@author{#1}%
}{%
\leftadd\dof@author{\protect\and #1}%
}
}
\newcommand{\addaffiliation}[1]{%
\ifthenelse{\equal{\dof@affiliation}{}}{%
\gdef\dof@affiliation{#1}%
}{%
\leftadd\dof@affiliation{\protect\and #1}%
}
}
\NewEnviron{isamarkupauthor*}[1][]{\isaDof[env={text},#1]{\BODY}}
\provideisadof{text.scholarly_paper.author}%
[label=,type=%
,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}}
\ifthenelse{\equal{\commandkey{scholarly_paper.author.orcid}}{}}{%
\protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}}}%
}{%
\protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}\string\orcidID{\commandkey{scholarly_paper.author.orcid}}}}%
}
\protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{scholarly_paper.author.email}}}}%
}
% end: scholarly_paper.author
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: scholarly_paper.abstract
\providecommand{\keywords}[1]{\mbox{}\\[2ex]\mbox{}\noindent{\textbf{Keywords:}} #1}
\NewEnviron{isamarkupabstract*}[1][]{\isaDof[env={text.scholarly_paper.abstract},#1]{\BODY}}
\newisadof{text.scholarly_paper.abstract}%
[label=,type=%
,scholarly_paper.abstract.keywordlist=%
][1]{%
\begin{isamarkuptext}%
\begin{abstract}%
#1%
\ifthenelse{\equal{\commandkey{scholarly_paper.abstract.keywordlist}}{}}{}{%
\keywords{\commandkey{scholarly_paper.abstract.keywordlist}}%
}%
\end{abstract}%
\end{isamarkuptext}%
}
\newtheorem{axiom}{Axiom}
\newtheorem{ruleX}{Rule} % apparent name-clash with s th from libraries...
\newtheorem{assertion}{Assertion}
% \newcommand{\formalMathStmt[label, mcc, ]
% end: scholarly_paper.abstract
% | "rule" | "assn" | "expl" | rem | "notation" | "terminology"
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newisadof{text.scholarly_paper.math_content}%
[label=,type=%
, scholarly_paper.math_content.short_name ={} % {} or \relax
, scholarly_paper.math_content.mcc = % "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, Isa_COL.text_element.level =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{definition}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{axm}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{axiom} \label{\commandkey{label}} #1 \end{axiom} }
{\begin{axiom} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{axiom}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
{\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{theorem}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{lemma}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{example}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{cor}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{corrollary} \label{\commandkey{label}} #1 \end{corrollary} }
{\begin{corrollary} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{corrollary}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{prop}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{property} \label{\commandkey{label}} #1 \end{property} }
{\begin{property} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{property}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rule}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{ruleX} \label{\commandkey{label}} #1 \end{ruleX} }
{\begin{ruleX} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{ruleX}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rem}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{remark} \label{\commandkey{label}} #1 \end{remark} }
{\begin{remark} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{remark}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{assertion} \label{\commandkey{label}} #1 \end{assertion} }
{\begin{assertion} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{assertion}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{notation}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{notation} \label{\commandkey{label}} #1 \end{notation} }
{\begin{notation} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{notation}}
}%
}%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{terminology}}
{%
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{terminology} \label{\commandkey{label}} #1 \end{terminology} }
{\begin{terminology} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{terminology}}
}%
}%
{%
\typeout{Internal error: enumeration out of sync with ontology scholarly-paper.}
}%
}%
}%
}%
}%
}%
}%
}%
}%
}%
}%
}%
\end{isamarkuptext}%
}
% end: scholarly_paper.math_content
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\newisadof{text.scholarly_paper.math_example}%
[label=,type=%
, scholarly_paper.math_content.short_name =%
, scholarly_paper.math_content.mcc =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
\label{\commandkey{label}} #1
\end{example}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newisadof{text.scholarly_paper.definition}%
[label=,type=%
, scholarly_paper.math_content.short_name =%
, scholarly_paper.math_content.mcc =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, Isa_COL.text_element.level =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{definition}}
}{%
#1%
}%
\end{isamarkuptext}%
}
% An experiment in inheritance of the default behaviour.
% \newisadof{text.scholarly_paper.definition}%
% [label=,type=%
% , scholarly_paper.math_content.short_name =%
% , scholarly_paper.math_content.mcc =%
% , Isa_COL.text_element.level =%
% , Isa_COL.text_element.referentiable =%
% , Isa_COL.text_element.variants =%
% , scholarly_paper.text_section.main_author =%
% , scholarly_paper.text_section.fixme_list =%
% , scholarly_paper.technical.definition_list =%
% , scholarly_paper.technical.status =%
% ]
% [1]
% {%
% \cscommand{text.scholarly_paper.math_content}%
% [label=\commandkey{label},type=\commandkey{type}%
% , scholarly_paper.math_content.short_name =\commandkey{scholarly_paper.math_content.short_name}%
% , scholarly_paper.math_content.mcc =\commandkey{scholarly_paper.math_content.mcc}%
% , Isa_COL.text_element.level =\commandkey{Isa_COL.text_element.level}%
% , Isa_COL.text_element.referentiable =\commandkey{Isa_COL.text_element.referentiable}%
% , Isa_COL.text_element.variants =\commandkey{Isa_COL.text_element.variants}%
% , scholarly_paper.text_section.main_author =\commandkey{scholarly_paper.text_section.main_author}%
% , scholarly_paper.text_section.fixme_list =\commandkey{scholarly_paper.text_section.fixme_list}%
% , scholarly_paper.technical.definition_list =\commandkey{scholarly_paper.technical.definition_list}%
% , scholarly_paper.technical.status =\commandkey{scholarly_paper.technical.status}%
% ]
% {#1}%
% }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Besser: Einfach durchreichen wg Vererbung !
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text.scholarly_paper.lemma},#1]{\BODY}}
\newisadof{text.scholarly_paper.lemma}%
[label=,type=%
, scholarly_paper.math_content.short_name =%
, scholarly_paper.math_content.mcc =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, Isa_COL.text_element.level =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{lemma}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text.scholarly_paper.theorem},#1]{\BODY}}
\newisadof{text.scholarly_paper.theorem}%
[label=,type=%
, scholarly_paper.math_content.short_name =%
, scholarly_paper.math_content.mcc =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, Isa_COL.text_element.level =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
{\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
{\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{theorem}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Generic Example. Different inheritance hierachy.
\newisadof{text.scholarly_paper.example}%
[label=,type=%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.example.status =%
, scholarly_paper.example.short_name =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.example.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.example.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.example.short_name}] %
\label{\commandkey{label}} #1 %
\end{example}} %
}%
{%
#1%
}%
\end{isamarkuptext}%
}
%% Miscellaneous
\usepackage{xspace}
\newcommand{\ie}{i.\,e.\xspace}
\newcommand{\eg}{e.\,g.\xspace}
\newcommand{\etc}{etc}

View File

@ -0,0 +1,2 @@
\usepackage{DOF-core}
\usepackage{DOF-scholarly_paper}

View File

@ -0,0 +1,113 @@
%% Copyright (c) 2019 University of Exeter
%% 2018-2019 University of Paris-Saclay
%% 2018-2019 The University of Sheffield
%%
%% 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.3c of the License, or (at your option) any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the lncs class.
%%
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\RequirePackage{ifvtex}
\documentclass{llncs}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[USenglish]{babel}
\usepackage{isabelle}
\usepackage{xcolor}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
This is a Isabelle_DOF project. The document preparation requires
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
\hypersetup{%
bookmarksdepth=3
,pdfpagelabels
,pageanchor=true
,bookmarksnumbered
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
\usepackage[caption]{subfig}
\usepackage[size=footnotesize]{caption}
\renewcommand{\topfraction}{0.9} % max fraction of floats at top
\renewcommand{\bottomfraction}{0.8} % max fraction of floats at bottom
\setcounter{topnumber}{2}
\setcounter{bottomnumber}{2}
\setcounter{totalnumber}{4} % 2 may work better
\setcounter{dbltopnumber}{2} % for 2-column pages
\renewcommand{\dbltopfraction}{0.9} % fit big float above 2-col. text
\renewcommand{\textfraction}{0.07} % allow minimal text w. figs
\renewcommand{\floatpagefraction}{0.7} % require fuller float pages
\renewcommand{\dblfloatpagefraction}{0.7} % require fuller float pages
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
%%% etc. should not be used (they are deprecated since more than a
%%% decade)
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\selectlanguage{USenglish}%
\renewcommand{\bibname}{References}%
\renewcommand{\figurename}{Fig.}
\renewcommand{\abstractname}{Abstract.}
\renewcommand{\subsubsectionautorefname}{Sect.}
\renewcommand{\subsectionautorefname}{Sect.}
\renewcommand{\sectionautorefname}{Sect.}
\renewcommand{\figureautorefname}{Fig.}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\newcommand{\lstnumberautorefname}{Line}
\maketitle
\input{session}
% optional bibliography
\IfFileExists{root.bib}{%
{\small
\newcommand{\urlprefix}{}
\bibliographystyle{splncs04}
\bibliography{root}
}}{}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: