Isabelle_DOF/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty

498 lines
20 KiB
TeX
Executable File

%% 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-v2019}%
{%
\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.scholarly_paper.author},#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}