diff --git a/Isabelle_DOF-Example-I/IsaDofApplications.thy b/Isabelle_DOF-Example-I/IsaDofApplications.thy index 6b0ac56..b9009cc 100644 --- a/Isabelle_DOF-Example-I/IsaDofApplications.thy +++ b/Isabelle_DOF-Example-I/IsaDofApplications.thy @@ -328,13 +328,36 @@ doc_class abstract = keyword_list :: "string list" <= None doc_class text_section = - main_author :: "author option" <= None - todo_list :: "string list" <= "[]" + main_author :: "author option" <= None + todo_list :: "string list" <= "[]" \} \caption{The core of the ontology definition for writing scholarly papers.} \label{fig:paper-onto-core} -\end{figure}\ -text\ The first part of the ontology \<^theory_text>\scholarly_paper\ (see \autoref{fig:paper-onto-core}) +\end{figure}\ + +text*["paper_onto_core"::figure2, + caption="''The core of the ontology definition for writing scholarly papers.''"] +\@{boxed_theory_text [display]\ +doc_class title = + short_title :: "string option" <= None + +doc_class subtitle = + abbrev :: "string option" <= None + +doc_class author = + affiliation :: "string" + +doc_class abstract = + keyword_list :: "string list" <= None + +doc_class text_section = + main_author :: "author option" <= None + todo_list :: "string list" <= "[]" +\}\ + +text\ The first part of the ontology \<^theory_text>\scholarly_paper\ +(see \autoref{fig:paper-onto-core}) +(see @{figure2 "paper_onto_core"}) contains the document class definitions with the usual text-elements of a scientific paper. The attributes \<^theory_text>\short_title\, \<^theory_text>\abbrev\ etc are introduced with their types as well as their default values. diff --git a/Isabelle_DOF/latex/styles/DOF-COL.sty b/Isabelle_DOF/latex/styles/DOF-COL.sty index ee64c69..be1a8be 100644 --- a/Isabelle_DOF/latex/styles/DOF-COL.sty +++ b/Isabelle_DOF/latex/styles/DOF-COL.sty @@ -46,6 +46,25 @@ % end: figure* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: figure2* +\NewEnviron{isamarkupfigureTWO*}[1][]{\isaDof[env={figureTWO},#1]{\BODY}} +\newisadof{figureDOTIsaUNDERSCORECOLDOTfigureTWO}% +[label=,type=% +,IsaUNDERSCORECOLDOTfigureDOTrelativeUNDERSCOREwidth=% +,IsaUNDERSCORECOLDOTfigureDOTplacement=% +,IsaUNDERSCORECOLDOTfigureDOTsrc=% +,IsaUNDERSCORECOLDOTfigureTWODOTcaption=% +,IsaUNDERSCORECOLDOTfigureDOTspawnUNDERSCOREcolumns=enum False True% +][1]{% + \begin{figure}[] + #1 + \caption{XXX\commandkey{IsaUNDERSCORECOLDOTfigureTWODOTcaption}} + \label{\commandkey{label}}% + \end{figure} +} +% end: figure2* +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index cd44ce4..00c2066 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -154,7 +154,7 @@ datatype placement = pl_h | (*here*) pl_hb (*here -> bottom*) ML\ "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context> - |> Name_Space.space_of_table)\ + |> Name_Space.space_of_table)\ print_doc_classes