%% Copyright (C) 2018 The University of Sheffield
%%               2018 The University of Paris-Sud
%%
%% 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 of the License, or any later version.
%%   OR
%%   The 2-clause BSD-style license.
%%  
%%   SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause

\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-core}
  [0000/00/00 Unreleased v0.0.0+%
  Document-Type Support Framework for Isabelle.]

\RequirePackage{keycommand}
\RequirePackage{environ}
\RequirePackage{graphicx}
\RequirePackage{fp}
\RequirePackage[caption]{subfig}
% Generic dispatcher
\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
\csname isaDof.\commandkey{env}.\commandkey{type}\endcsname[label=\commandkey{label},\commandkey{args}]{#1}%
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: text.text
\expandafter\newkeycommand\csname isaDof.text.text\endcsname%
[label=,type=%
][1]{%
  \begin{isamarkuptext}%
    #1
  \end{isamarkuptext}%
}
% begin: text.text
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: figure*
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
\expandafter\newkeycommand\csname isaDof.figure.Isa_COL.figure\endcsname%
[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{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
\expandafter\newkeycommand\csname isaDof.side_by_side_figure.Isa_COL.side_by_side_figure\endcsname%
[label=,type=%
,Isa_COL.figure.relative_width=%
,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.side_by_side_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*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: Text*
\NewEnviron{isamarkupText*}[1][]{\isaDof[env={Text},#1]{\BODY}}
% end: Text*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: text*
\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}}
% end: text*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newkeycommand\isaDofOpenMonitor[label=,type=]{}
\newkeycommand\isaDofCloseMonitor[label=,type=]{}

\newkeycommand\isaDofDeclareReferenceTextSection[label=,type=]{}
\newkeycommand\isaDofDeclareReferenceFigure[label=,type=]{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: chapter*
\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}}
% end: chapter*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: section*
\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}}
% end: section*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: subsection*
\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}}
% end: subsection*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%