%% 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}% {% \RequirePackage{amsthm} \newcommand{\institute}[1]{}% \newcommand{\inst}[1]{}% \newcommand{\orcidID}[1]{}% \newcommand{\email}[1]{}% }% {% \@ifclassloaded{lipics-v2021}% {% \RequirePackage{amsthm} \newcommand{\institute}[1]{}% \newcommand{\inst}[1]{}% \newcommand{\orcidID}[1]{}% \newcommand{\email}[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{titleDOTscholarlyUNDERSCOREpaperDOTtitle}% [label=,type=% ,scholarlyUNDERSCOREpaperDOTtitleDOTshortUNDERSCOREtitle=% ][1]{% \immediate\write\@auxout{\noexpand\title{#1}}% } % end: title* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: subtitle* \NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}} \newisadof{subtitleDOTscholarlyUNDERSCOREpaperDOTsubtitle}% [label=,type=% ,scholarlyUNDERSCOREpaperDOTsubtitleDOTabbrev=% ][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{textDOTscholarlyUNDERSCOREpaperDOTauthor}% [label=,type=% ,scholarlyUNDERSCOREpaperDOTauthorDOTemail=% ,scholarlyUNDERSCOREpaperDOTauthorDOTaffiliation=% ,scholarlyUNDERSCOREpaperDOTauthorDOTorcid=% ,scholarlyUNDERSCOREpaperDOTauthorDOThttpUNDERSCOREsite=% ][1]{% \stepcounter{dof@cnt@author} \def\dof@a{\commandkey{scholarlyUNDERSCOREpaperDOTauthorDOTaffiliation}} \ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTauthorDOTorcid}}{}}{% \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{scholarlyUNDERSCOREpaperDOTauthorDOTorcid}}}}% } \protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{scholarlyUNDERSCOREpaperDOTauthorDOTemail}}}}% } % end: scholarly_paper.author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: scholarly_paper.abstract \providecommand{\keywords}[1]{\mbox{}\\[2ex]\mbox{}\noindent{\textbf{Keywords:}} #1} \NewEnviron{isamarkupabstract*}[1][]{\isaDof[env={text},#1]{\BODY}} \newisadof{textDOTscholarlyUNDERSCOREpaperDOTabstract}% [label=,type=% ,scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist=% ][1]{% \begin{isamarkuptext}% \begin{abstract}% #1% \ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist}}{}}{}{% \keywords{\commandkey{scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist}}% }% \end{abstract}% \end{isamarkuptext}% } %\RequirePackage{amsthm} %\newtheorem{example}{Example} %\newtheorem{assumption}{Assumption} %\newtheorem{definition}{Definition} %\newtheorem{theorem}{Theorem} \newtheorem{defn}{Definition} \providecommand{\defnautorefname}{Definition} \NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{axm}{Axiom} \providecommand{\axmautorefname}{Axiom} \NewEnviron{isamarkupAxiom*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{theom}{Theorem} \providecommand{\theomautorefname}{Theorem} \NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{lemm}{Lemma} \providecommand{\lemmautorefname}{Lemma} \NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{corr}{Corollary} \providecommand{\corrautorefname}{Corollary} \NewEnviron{isamarkupCorollary*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{prpo}{Proposition} \providecommand{\prpoautorefname}{Proposition} \NewEnviron{isamarkupProposition*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{rulE}{Rule} \providecommand{\rulEautorefname}{Rule} \NewEnviron{isamarkupRule*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{assn}{Assertion} \providecommand{\assnautorefname}{Assertion} \NewEnviron{isamarkupAssertion*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{hypt}{Hypothesis} \providecommand{\hyptautorefname}{Hypothesis} \NewEnviron{isamarkupHypothesis*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{assm}{Assumption} \providecommand{\assmautorefname}{Assumption} \NewEnviron{isamarkupAssumption*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{prms}{Premise} \providecommand{\prmsautorefname}{Premise} \NewEnviron{isamarkupPremise*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{cons}{Consequence} \providecommand{\consautorefname}{Consequence} \NewEnviron{isamarkupConsequence*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{concUNDERSCOREstmt}{Conclusion} \providecommand{\concUNDERSCOREstmtautorefname}{Conclusion} \NewEnviron{isamarkupConclusion*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{prfUNDERSCOREstmt}{Proof} \providecommand{\prfUNDERSCOREstmtautorefname}{Proof} \NewEnviron{isamarkupProof*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{explUNDERSCOREstmt}{Example} \providecommand{\explUNDERSCOREstmtautorefname}{Example} \NewEnviron{isamarkupExample*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{rmrk}{Remark} \providecommand{\rmrkautorefname}{Remark} \NewEnviron{isamarkupRemark*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{notn}{Notation} \providecommand{\notnautorefname}{Notation} \NewEnviron{isamarkupNotation*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newtheorem{tmgy}{Terminology} \providecommand{\tmgyautorefname}{Terminology} \NewEnviron{isamarkupTerminology*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}} \newisadof{textDOTscholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}% [label=,type=% , scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname ={}% , scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc = % , IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =% , IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable =% , IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants =% , scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTmainUNDERSCOREauthor =% , scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTfixmeUNDERSCORElist =% , IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =% , scholarlyUNDERSCOREpaperDOTtechnicalDOTdefinitionUNDERSCORElist =% , scholarlyUNDERSCOREpaperDOTtechnicalDOTstatus =% ] [1] {% \begin{isamarkuptext}% \ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}} {} } {% \begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}\label{\commandkey{label}} #1 \end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}} }{% \begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}[\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}]\label{\commandkey{label}} #1 \end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}} } \end{isamarkuptext}% } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Miscellaneous \usepackage{xspace} \newcommand{\ie}{i.\,e.\xspace} \newcommand{\eg}{e.\,g.\xspace} \newcommand{\etc}{etc}