%% 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}
  [2020/01/14 Unreleased/Isabelle2020%
  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]{}%
        }%
        {%
          \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}%
 }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung !
\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 !
\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 !
\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}