Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Burkhart Wolff 2023-04-19 21:50:51 +02:00
parent a6aca1407e 77e8844687
commit 1acf863845
10 changed files with 235 additions and 221 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
Isabelle_DOF-Ontologies/CC_v3_1_R5/DOF-CC_terminology.sty
View File

@ -23,35 +23,35 @@
\newkeycommand*{\mathcc}[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 =%
, CC_terminology.concept_definition.tag=%
, CC_terminology.concept_definition.short_tag=%
, scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname ={}%
, scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc = %
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants =%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTmainUNDERSCOREauthor =%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTfixmeUNDERSCORElist =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTdefinitionUNDERSCORElist =%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTstatus =%
, CCUNDERSCOREterminologyDOTconceptUNDERSCOREdefinitionDOTtag=%
, CCUNDERSCOREterminologyDOTconceptUNDERSCOREdefinitionDOTshortUNDERSCOREtag=%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
\ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}} {} }
{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}\label{\commandkey{label}}
\begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
\end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}
}{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}[\commandkey{scholarly_paper.math_content.short_name}]\label{\commandkey{label}}
\begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}[\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}]\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
\end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}
}
\end{isamarkuptext}%
}
\expandafter\def\csname isaDof.text.scholarly_paper.math_content\endcsname{\mathcc}
\expandafter\def\csname isaDofDOTtextDOTscholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent\endcsname{\mathcc}

104
Isabelle_DOF-Ontologies/CENELEC_50128/DOF-CENELEC_50128.sty
View File

@ -60,26 +60,26 @@
}
\newcommand{\SRACautorefname}{SRAC}
\newisadof{text.CENELEC_50128.SRAC}%
\newisadof{textDOTCENELECUNDERSCORE50128DOTSRAC}%
[label=,type=%
,Isa_COL.text_element.level=%
,Isa_COL.text_element.referentiable=%
,Isa_COL.text_element.variants=%
,CENELEC_50128.requirement.is_concerned=%
,CENELEC_50128.requirement.long_name=%
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.EC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTECDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
\ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
\begin{SRAC}%
\addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}}%
}{%
\begin{SRAC}[\commandkey{CENELEC_50128.requirement.long_name}]%
\addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELEC_50128.requirement.long_name}}%
\DOFindex{SRAC}{\commandkey{CENELEC_50128.requirement.long_name}}%
\begin{SRAC}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
\addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
\DOFindex{SRAC}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
}\label{\commandkey{label}}%
#1%
\end{SRAC}
@ -113,26 +113,26 @@
}
\newcommand{\ECautorefname}{EC}
\newisadof{text.CENELEC_50128.EC}%
\newisadof{textDOTCENELECUNDERSCORE50128DOTEC}%
[label=,type=%
,Isa_COL.text_element.level=%
,Isa_COL.text_element.referentiable=%
,Isa_COL.text_element.variants=%
,CENELEC_50128.requirement.is_concerned=%
,CENELEC_50128.requirement.long_name=%
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.EC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTECDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
\ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
\begin{EC}%
\addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}}%
}{%
\begin{EC}[\commandkey{CENELEC_50128.requirement.long_name}]%
\addxcontentsline{toe}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELEC_50128.requirement.long_name}}%
\DOFindex{EC}{\commandkey{CENELEC_50128.requirement.long_name}}%
\begin{EC}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
\addxcontentsline{toe}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
\DOFindex{EC}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
}\label{\commandkey{label}}%
#1%
\end{EC}
@ -155,23 +155,23 @@
}
\newcommand{\assumptionautorefname}{assumption}
\newisadof{text.CENELEC_50128.assumption}%
\newisadof{textDOTCENELECUNDERSCORE50128DOTassumption}%
[label=,type=%
,Isa_COL.text_element.level=%
,Isa_COL.text_element.referentiable=%
,Isa_COL.text_element.variants=%
,CENELEC_50128.requirement.is_concerned=%
,CENELEC_50128.requirement.long_name=%
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
\ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
\begin{assumption}%
}{%
\begin{assumption}[\commandkey{CENELEC_50128.requirement.long_name}]%
\DOFindex{assumption}{\commandkey{CENELEC_50128.requirement.long_name}}%
\begin{assumption}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
\DOFindex{assumption}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
}\label{\commandkey{label}}%
#1%
\end{assumption}
@ -196,23 +196,23 @@
\newcommand{\hypothesisautorefname}{hypothesis}
\newisadof{text.CENELEC_50128.hypothesis}%
\newisadof{textDOTCENELECUNDERSCORE50128DOThypothesis}%
[label=,type=%
,Isa_COL.text_element.level=%
,Isa_COL.text_element.referentiable=%
,Isa_COL.text_element.variants=%
,CENELEC_50128.requirement.is_concerned=%
,CENELEC_50128.requirement.long_name=%
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.hypothesis_kind=%
,CENELEC_50128.hypothesis.hyp_type=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
,CENELECUNDERSCORE50128DOTSRACDOThypothesisUNDERSCOREkind=%
,CENELECUNDERSCORE50128DOThypothesisDOThypUNDERSCOREtype=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
\ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
\begin{hypothesis}%
}{%
\begin{hypothesis}[\commandkey{CENELEC_50128.requirement.long_name}]%
\DOFindex{hypothesis}{\commandkey{CENELEC_50128.requirement.long_name}}%
\begin{hypothesis}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
\DOFindex{hypothesis}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
}\label{\commandkey{label}}%
#1%
\end{hypothesis}

64
Isabelle_DOF/latex/styles/DOF-COL.sty
View File

@ -21,23 +21,23 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: figure*
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
\newisadof{figure.Isa_COL.figure}%
\newisadof{figureDOTIsaUNDERSCORECOLDOTfigure}%
[label=,type=%
,Isa_COL.figure.relative_width=%
,Isa_COL.figure.placement=%
,Isa_COL.figure.src=%
,Isa_COL.figure.spawn_columns=enum False True%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True%
][1]{%
\begin{figure}[]
\centering
\ifcommandkey{Isa_COL.figure.relative_width}
\ifcommandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}
{%
\gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\FPdiv\scale{\dof@width}{100}%
\includegraphics[width=\scale\textwidth]{\dof@src}%
}{%
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\includegraphics[]{\dof@src}%
}
\caption{#1}\label{\commandkey{label}}%
@ -50,44 +50,44 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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}%
\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={sideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure},#1]{\BODY}}
\newisadof{sideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTIsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure}%
[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%
,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=%
,IsaUNDERSCORECOLDOTfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTsrc=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchor=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaption=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchorTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaptionTWO=%
,IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTplacement=%
,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=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}%
\subfloat[\label{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchor}}\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaption}]%
{\ifcommandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}%
{%
\gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\FPdiv\scale{\dof@width}{100}%
\includegraphics[width=\scale\textwidth]{\dof@src}%
}{%
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTfigureDOTsrc}}
\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}%
\subfloat[\label{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTanchorTWO}}\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTcaptionTWO}]%
{\ifcommandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO}%
{%
\gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}}
\gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
\gdef\dof@width{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTrelativeUNDERSCOREwidthTWO}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO}}
\FPdiv\scale{\dof@width}{100}%
\includegraphics[width=\scale\textwidth]{\dof@src}%
}{%
\gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
\gdef\dof@src{\commandkey{IsaUNDERSCORECOLDOTsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigureDOTsrcTWO}}
\includegraphics[]{\dof@src}%
}%
}%

18
Isabelle_DOF/latex/styles/DOF-core.sty
View File

@ -53,27 +53,27 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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}%
\newcommand\newisadof[1]{\expandafter\newkeycommand\csname isaDofDOT#1\endcsname}%
\newcommand\renewisadof[1]{\expandafter\renewkeycommand\csname isaDofDOT#1\endcsname}%
\newcommand\provideisadof[1]{\expandafter\providekeycommand\csname isaDofDOT#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%
\ifcsname isaDofDOT\commandkey{type}\endcsname%
\csname isaDofDOT\commandkey{type}\endcsname%
[label=\commandkey{label},\commandkey{args}]{#1}%
\else%
\ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
\csname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
\ifcsname isaDofDOT\commandkey{env}DOT\commandkey{type}\endcsname%
\csname isaDofDOT\commandkey{env}DOT\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%
\ifcsname isaDofDOT\commandkey{env}\endcsname%
\csname isaDofDOT\commandkey{env}\endcsname%
[label=\commandkey{label}]{#1}%
\else%
\errmessage{Isabelle/DOF: No LaTeX representation for concept %

114
Isabelle_DOF/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -73,9 +73,9 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: title*
\NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}}
\newisadof{title.scholarly_paper.title}%
\newisadof{titleDOTscholarlyUNDERSCOREpaperDOTtitle}%
[label=,type=%
,scholarly_paper.title.short_title=%
,scholarlyUNDERSCOREpaperDOTtitleDOTshortUNDERSCOREtitle=%
][1]{%
\immediate\write\@auxout{\noexpand\title{#1}}%
}
@ -85,9 +85,9 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: subtitle*
\NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}}
\newisadof{subtitle.scholarly_paper.subtitle}%
\newisadof{subtitleDOTscholarlyUNDERSCOREpaperDOTsubtitle}%
[label=,type=%
,scholarly_paper.subtitle.abbrev=%
,scholarlyUNDERSCOREpaperDOTsubtitleDOTabbrev=%
][1]{%
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
}
@ -128,21 +128,21 @@
}
\NewEnviron{isamarkupauthor*}[1][]{\isaDof[env={text},#1]{\BODY}}
\provideisadof{text.scholarly_paper.author}%
\provideisadof{textDOTscholarlyUNDERSCOREpaperDOTauthor}%
[label=,type=%
,scholarly_paper.author.email=%
,scholarly_paper.author.affiliation=%
,scholarly_paper.author.orcid=%
,scholarly_paper.author.http_site=%
,scholarlyUNDERSCOREpaperDOTauthorDOTemail=%
,scholarlyUNDERSCOREpaperDOTauthorDOTaffiliation=%
,scholarlyUNDERSCOREpaperDOTauthorDOTorcid=%
,scholarlyUNDERSCOREpaperDOTauthorDOThttpUNDERSCOREsite=%
][1]{%
\stepcounter{dof@cnt@author}
\def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
\ifthenelse{\equal{\commandkey{scholarly_paper.author.orcid}}{}}{%
\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{scholarly_paper.author.orcid}}}}%
\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{scholarly_paper.author.email}}}}%
\protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{scholarlyUNDERSCOREpaperDOTauthorDOTemail}}}}%
}
% end: scholarly_paper.author
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@ -151,15 +151,15 @@
% begin: scholarly_paper.abstract
\providecommand{\keywords}[1]{\mbox{}\\[2ex]\mbox{}\noindent{\textbf{Keywords:}} #1}
\NewEnviron{isamarkupabstract*}[1][]{\isaDof[env={text},#1]{\BODY}}
\newisadof{text.scholarly_paper.abstract}%
\newisadof{text.scholarlyUNDERSCOREpaperDOTabstract}%
[label=,type=%
,scholarly_paper.abstract.keywordlist=%
,scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist=%
][1]{%
\begin{isamarkuptext}%
\begin{abstract}%
#1%
\ifthenelse{\equal{\commandkey{scholarly_paper.abstract.keywordlist}}{}}{}{%
\keywords{\commandkey{scholarly_paper.abstract.keywordlist}}%
\ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist}}{}}{}{%
\keywords{\commandkey{scholarlyUNDERSCOREpaperDOTabstractDOTkeywordlist}}%
}%
\end{abstract}%
\end{isamarkuptext}%
@ -172,84 +172,84 @@
%\newtheorem{theorem}{Theorem}
\newtheorem{defn}{Definition}
\newcommand{\defnautorefname}{Definition}
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{axm}{Axiom}
\newcommand{\axmautorefname}{Axiom}
\NewEnviron{isamarkupAxiom*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupAxiom*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{theom}{Theorem}
\newcommand{\theomautorefname}{Theorem}
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{lemm}{Lemma}
\newcommand{\lemmautorefname}{Lemma}
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{corr}{Corollary}
\newcommand{\corrautorefname}{Corollary}
\NewEnviron{isamarkupCorollary*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupCorollary*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{prpo}{Proposition}
\newcommand{\prpoautorefname}{Proposition}
\NewEnviron{isamarkupProposition*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupProposition*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{rulE}{Rule}
\newcommand{\rulEautorefname}{Rule}
\NewEnviron{isamarkupRule*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupRule*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{assn}{Assertion}
\newcommand{\assnautorefname}{Assertion}
\NewEnviron{isamarkupAssertion*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupAssertion*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{hypt}{Hypothesis}
\newcommand{\hyptautorefname}{Hypothesis}
\NewEnviron{isamarkupHypothesis*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupHypothesis*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{assm}{Assumption}
\newcommand{\assmautorefname}{Assumption}
\NewEnviron{isamarkupAssumption*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupAssumption*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{prms}{Premise}
\newcommand{\prmsautorefname}{Premise}
\NewEnviron{isamarkupPremise*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupPremise*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{cons}{Consequence}
\newcommand{\consautorefname}{Consequence}
\NewEnviron{isamarkupConsequence*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\newtheorem{conc_stmt}{Conclusion}
\newcommand{\concstmtautorefname}{Conclusion}
\NewEnviron{isamarkupConclusion*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\newtheorem{prf_stmt}{Proof}
\newcommand{\prfstmtautorefname}{Proof}
\NewEnviron{isamarkupProof*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\newtheorem{expl_stmt}{Example}
\newcommand{\explstmtautorefname}{Example}
\NewEnviron{isamarkupExample*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupConsequence*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{concUNDERSCOREstmt}{Conclusion}
\newcommand{\concUNDERSCOREstmtautorefname}{Conclusion}
\NewEnviron{isamarkupConclusion*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{prfUNDERSCOREstmt}{Proof}
\newcommand{\prfUNDERSCOREstmtautorefname}{Proof}
\NewEnviron{isamarkupProof*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{explUNDERSCOREstmt}{Example}
\newcommand{\explUNDERSCOREstmtautorefname}{Example}
\NewEnviron{isamarkupExample*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{rmrk}{Remark}
\newcommand{\rmrkautorefname}{Remark}
\NewEnviron{isamarkupRemark*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupRemark*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{notn}{Notation}
\newcommand{\notnautorefname}{Notation}
\NewEnviron{isamarkupNotation*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupNotation*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newtheorem{tmgy}{Terminology}
\newcommand{\tmgyautorefname}{Terminology}
\NewEnviron{isamarkupTerminology*}[1][]{\isaDof[env={text},#1,type={scholarly_paper.math_content}]{\BODY}}
\NewEnviron{isamarkupTerminology*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
\newisadof{text.scholarly_paper.math_content}%
\newisadof{textDOTscholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}%
[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 =%
, scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname ={}%
, scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc = %
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants =%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTmainUNDERSCOREauthor =%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTfixmeUNDERSCORElist =%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel =%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTdefinitionUNDERSCORElist =%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTstatus =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
\ifthenelse{\equal{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}} {} }
{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}\label{\commandkey{label}}
\begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
\end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}
}{%
\begin{\commandkey{scholarly_paper.math_content.mcc}}[\commandkey{scholarly_paper.math_content.short_name}]\label{\commandkey{label}}
\begin{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}[\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTshortUNDERSCOREname}]\label{\commandkey{label}}
#1
\end{\commandkey{scholarly_paper.math_content.mcc}}
\end{\commandkey{scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontentDOTmcc}}
}
\end{isamarkuptext}%
}

34
Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -53,12 +53,12 @@ ML\<open>
val _ =
Monitor_Command_Parser.document_command \<^command_keyword>\<open>abstract*\<close> "Textual Definition"
{markdown = true, body = true}
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []) (K(K I));
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []) [] I;
val _ =
Monitor_Command_Parser.document_command \<^command_keyword>\<open>author*\<close> "Textual Definition"
{markdown = true, body = true}
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []) (K(K I));
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []) [] I;
\<close>
text\<open>Scholarly Paper is oriented towards the classical domains in science:
@ -203,7 +203,6 @@ datatype math_content_class =
| "notn" \<comment>\<open>notation\<close>
| "tmgy" \<comment>\<open>terminology\<close>
text\<open>Instances of the \<open>doc_class\<close> \<^verbatim>\<open>math_content\<close> are by definition @{term "semiformal"}; they may
be non-referential, but in this case they will not have a @{term "short_name"}.\<close>
@ -444,49 +443,50 @@ fun doc_cmd kwd txt flag key =
in
Onto_Macros.enriched_formal_statement_command default [("mcc",key)] meta_args thy
end)
(Onto_Macros.transform_attr [("mcc",key)])
[\<^const_name>\<open>mcc\<close>]
(Onto_Macros.transform_attr [(\<^const_name>\<open>mcc\<close>,key)])
in
val _ = doc_cmd \<^command_keyword>\<open>Definition*\<close> "Freeform Definition"
Definition_default_class "defn";
Definition_default_class \<^const_name>\<open>defn\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Lemma*\<close> "Freeform Lemma Description"
Lemma_default_class "lemm";
Lemma_default_class \<^const_name>\<open>lemm\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Theorem*\<close> "Freeform Theorem"
Theorem_default_class "theom";
Theorem_default_class \<^const_name>\<open>theom\<close>;
(* cut and paste to make it runnable, but nonsensical so far: *)
val _ = doc_cmd \<^command_keyword>\<open>Proposition*\<close> "Freeform Proposition"
Proposition_default_class "prpo";
Proposition_default_class \<^const_name>\<open>prpo\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Premise*\<close> "Freeform Premise"
Premise_default_class "prms";
Premise_default_class \<^const_name>\<open>prms\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Corollary*\<close> "Freeform Corollary"
Corollary_default_class "corr";
Corollary_default_class \<^const_name>\<open>corr\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Consequence*\<close> "Freeform Consequence"
Consequence_default_class "cons";
Consequence_default_class \<^const_name>\<open>cons\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Conclusion*\<close> "Freeform Conclusion"
Conclusion_default_class "conc_stmt";
Conclusion_default_class \<^const_name>\<open>conc_stmt\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Assumption*\<close> "Freeform Assumption"
Assumption_default_class "assm";
Assumption_default_class \<^const_name>\<open>assm\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Hypothesis*\<close> "Freeform Hypothesis"
Hypothesis_default_class "prpo";
Hypothesis_default_class \<^const_name>\<open>prpo\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Assertion*\<close> "Freeform Assertion"
Assertion_default_class "assn";
Assertion_default_class \<^const_name>\<open>assn\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Proof*\<close> "Freeform Proof"
Proof_default_class "prf_stmt";
Proof_default_class \<^const_name>\<open>prf_stmt\<close>;
val _ = doc_cmd \<^command_keyword>\<open>Example*\<close> "Freeform Example"
Example_default_class "expl_stmt";
Example_default_class \<^const_name>\<open>expl_stmt\<close>;
end
end
\<close>

20
Isabelle_DOF/ontologies/technical_report/DOF-technical_report.sty
View File

@ -34,16 +34,16 @@
\newisadof{text.technical_report.SML}%
[ 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.technical.status=%
, scholarly_paper.technical.formal_results=%
, technical_report.code.checked=%
, technical_report.code.caption=%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
, IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTmainUNDERSCOREauthor=%
, scholarlyUNDERSCOREpaperDOTtextUNDERSCOREsectionDOTfixmeUNDERSCORElist=%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTdefinitionUNDERSCORElist=%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTstatus=%
, scholarlyUNDERSCOREpaperDOTtechnicalDOTformalUNDERSCOREresults=%
, technicalUNDERSCOREreportDOTcodeDOTchecked=%
, technicalUNDERSCOREreportDOTcodeDOTcaption=%
]
[1]
{%

12
Isabelle_DOF/thys/Isa_COL.thy
View File

@ -103,17 +103,11 @@ fun transform_cid thy NONE X = X
end
in
fun transform_attr S cid_long thy doc_attrs =
fun transform_attr S doc_attrs =
let
fun transform_attr' [] doc_attrs = doc_attrs
| transform_attr' (s::S) (doc_attrs) =
let fun markup2string s = s |> YXML.content_of
|> Symbol.explode
|> List.filter (fn c => c <> Symbol.DEL)
|> String.concat
fun toLong n = DOF_core.get_attribute_info cid_long (markup2string n) thy
|> the |> #long_name
val (name', value) = s |> (fn (n, v) => (toLong n, v))
let val (name', value) = s
val doc_attrs' = doc_attrs
|> map (fn (name, term) => if name = name'
then (name, value)
@ -154,7 +148,7 @@ end (* local *)
fun heading_command (name, pos) descr level =
Monitor_Command_Parser.document_command (name, pos) descr
{markdown = false, body = true} (enriched_text_element_cmd level) (K(K I));
{markdown = false, body = true} (enriched_text_element_cmd level) [] I;
val _ = heading_command \<^command_keyword>\<open>title*\<close> "section heading" NONE;
val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "section heading" NONE;

52
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -841,6 +841,10 @@ val check_opening_ml_invs = check_invs get_opening_ml_invariants
val check_closing_ml_invs = check_invs get_closing_ml_invariants
(* Output name for LaTeX macros.
Also rewrite "." to allow macros with objects long names *)
val output_name = Latex.output_name o translate_string (fn "." => "DOT" | s => s)
val ISA_prefix = "Isabelle_DOF_"
val doc_class_prefix = ISA_prefix ^ "doc_class_"
@ -2137,19 +2141,21 @@ fun close_monitor_command (args as (((oid, pos), cid_pos),
end
fun meta_args_2_latex thy transform_attr
fun meta_args_2_latex thy sem_attrs transform_attr
((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) =
(* for the moment naive, i.e. without textual normalization of
attribute names and adapted term printing *)
let val l = DOF_core.get_instance_name_global lab thy |> enclose "{" "}"
let val l = DOF_core.get_instance_name_global lab thy |> DOF_core.output_name
|> enclose "{" "}"
|> prefix "label = "
(* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *)
val cid_long = case cid_opt of
NONE => DOF_core.cid_of lab thy
| SOME(cid,_) => DOF_core.get_onto_class_name_global' cid thy
(* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *)
val cid_txt = "type = " ^ (enclose "{" "}" cid_long);
val cid_txt = cid_long |> DOF_core.output_name
|> enclose "{" "}"
|> prefix "type = "
fun ltx_of_term _ _ (c as \<^Const_>\<open>Cons \<^Type>\<open>char\<close> for _ _\<close>) = HOLogic.dest_string c
| ltx_of_term _ _ \<^Const_>\<open>Nil _\<close> = ""
| ltx_of_term _ _ \<^Const_>\<open>numeral _ for t\<close> = Int.toString(HOLogic.dest_numeral t)
@ -2194,8 +2200,24 @@ fun meta_args_2_latex thy transform_attr
val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a)
(map (fn (c,_) => c) actual_args))) default_args
val transformed_args = (actual_args@default_args_filtered)
|> transform_attr cid_long thy
val str_args = transformed_args
|> transform_attr
fun update_sem_std_attrs [] attrs = attrs
| update_sem_std_attrs (attr::attrs) attrs' =
let val attrs'' = attrs' |> map (fn (name, value) =>
let val value' = value |> Long_Name.base_name
in
if name = attr
then if value' (*|> Symbol_Pos.is_identifier*)
|> Symbol.is_ascii_identifier
then (name, DOF_core.output_name value')
else ISA_core.err ("Bad name of semantic attribute"
^ name ^ ": " ^ value
^ ". Name must be ASCII") pos
else (name, value') end)
in update_sem_std_attrs attrs attrs'' end
val updated_sem_std_attrs = update_sem_std_attrs sem_attrs transformed_args
val updated_sem_std_attrs' = updated_sem_std_attrs |> map (apfst DOF_core.output_name)
val str_args = updated_sem_std_attrs'
|> map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs))
val label_and_type = String.concat [ l, ",", cid_txt]
@ -2221,15 +2243,15 @@ fun gen_enriched_document_cmd' {inline} cid_transform attr_transform
(* {markdown = true} sets the parsing process such that in the text-core
markdown elements are accepted. *)
fun document_output {markdown: bool, markup: Latex.text -> Latex.text} transform_attr meta_args text ctxt =
fun document_output {markdown: bool, markup: Latex.text -> Latex.text} sem_attrs transform_attr meta_args text ctxt =
let
val thy = Proof_Context.theory_of ctxt;
val _ = Context_Position.reports ctxt (Document_Output.document_reports text);
val output_meta = meta_args_2_latex thy transform_attr meta_args;
val output_meta = meta_args_2_latex thy sem_attrs transform_attr meta_args;
val output_text = Document_Output.output_document ctxt {markdown = markdown} text;
in markup (output_meta @ output_text) end;
fun document_output_reports name {markdown, body} transform_attr meta_args text ctxt =
fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_args text ctxt =
let
(*val pos = Input.pos_of text;
val _ =
@ -2239,16 +2261,16 @@ fun document_output_reports name {markdown, body} transform_attr meta_args text
fun markup xml =
let val m = if body then Markup.latex_body else Markup.latex_heading
in [XML.Elem (m (Latex.output_name name), xml)] end;
in document_output {markdown = markdown, markup = markup} transform_attr meta_args text ctxt end;
in document_output {markdown = markdown, markup = markup} sem_attrs transform_attr meta_args text ctxt end;
(* document output commands *)
fun document_command (name, pos) descr mark cmd transform_attr =
fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
Outer_Syntax.command (name, pos) descr
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
Toplevel.theory' (fn _ => cmd meta_args)
(Toplevel.presentation_context #> document_output_reports name mark transform_attr meta_args text #> SOME)));
(Toplevel.presentation_context #> document_output_reports name mark sem_attrs transform_attr meta_args text #> SOME)));
(* Core Command Definitions *)
@ -2274,14 +2296,14 @@ val _ =
val _ =
document_command \<^command_keyword>\<open>text*\<close> "formal comment (primary style)"
{markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) (K(K I));
{markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) [] I;
(* This is just a stub at present *)
val _ =
document_command \<^command_keyword>\<open>text-macro*\<close> "formal comment macro"
{markdown = true, body = true}
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I) (K(K I));
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I) [] I;
val (declare_reference_default_class, declare_reference_default_class_setup)
@ -2829,7 +2851,7 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src
|(true,true) => XML.enclose("{\\isaDofmacroDef[type={"^cid_decl^"}]{")"}}"
|(false,true) => XML.enclose("{\\isaDofmacroExp[type={"^cid_decl^"}]{")"}}"
)
(Latex.text (str, pos))
(Latex.text (DOF_core.output_name str, pos))
end

2
Isabelle_DOF/thys/manual/M_04_RefMan.thy
View File

@ -453,9 +453,7 @@ term*\<open>@{B--test- \<open>b\<close>}\<close>
declare_reference*["text-elements-expls"::technical]
(*>*)
ML\<open>
\<close>
subsection*["subsec:onto-term-ctxt"::technical]\<open>Ontological Term-Contexts and their Management\<close>
text\<open>
\<^item> \<open>annotated_term_element\<close>