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

added onto markup support for definitions and examples in scholarly_paper lncs style

This commit is contained in:
Burkhart Wolff 2020-02-17 23:07:34 +01:00
parent fe8a6c5c87
commit c5b5f994ef
3 changed files with 53 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/DOF/Isa_DOF.thy
View File

@ -1861,4 +1861,5 @@ ML\<open>
\<close>
*)
end

52
src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -14,7 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-scholarly_paper}
[<isadofltxversion>%
[2020/01/14 Unreleased/Isabelle2019%
Document-Type Support Framework for Isabelle (LNCS).]
\RequirePackage{DOF-COL}
@ -153,5 +153,55 @@
\end{abstract}%
\end{isamarkuptext}%
}
% end: scholarly_paper.abstract
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newisadof{text.scholarly_paper.definition}%
[label=,type=%
, scholarly_paper.definition.tag =%
, 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.technical.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.definition.tag}} {} }
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
{\begin{definition} [\commandkey{scholarly_paper.definition.tag}] \label{\commandkey{label}} #1 \end{definition}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newisadof{text.scholarly_paper.example}%
[label=,type=%
, scholarly_paper.example.tag =%
, 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.technical.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.example.tag}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.example.tag}] \label{\commandkey{label}} #1 \end{example}}
}{%
#1%
}%
\end{isamarkuptext}%
}

2
src/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -63,7 +63,7 @@ As Security of the system we define etc...
A formal statement can, but must not have a reference to true formal Isabelle/Isar definition.
\<close>
datatype status = formal | description
datatype status = semiformal | description
doc_class technical = text_section +
definition_list :: "string list" <= "[]"