From 8328626fa44b3cf9b13b4acac35fb396a5cbe200 Mon Sep 17 00:00:00 2001 From: bu Date: Thu, 23 Apr 2020 16:08:05 +0200 Subject: [PATCH] Restructuring library prep. --- .../Isabelle_DOF-Manual/04_RefMan.thy | 1 - src/DOF/Isa_COL.thy | 2 +- src/DOF/Isa_DOF.thy | 33 ++++++++--------- src/DOF/latex/DOF-COL.sty | 1 + .../scholarly_paper/DOF-scholarly_paper.sty | 15 ++++---- .../scholarly_paper/scholarly_paper.thy | 35 +++++++++++-------- .../technical_report/technical_report.thy | 2 +- 7 files changed, 50 insertions(+), 39 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 3c65c6d..b027546 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -538,7 +538,6 @@ text\ | @@{command "text*"} | @@{command "figure*"} | @@{command "side_by_side_figure*"} | @@{command "open_monitor*"} | @@{command "close_monitor*"} | @@{command "Definition*"} | @@{command "Lemma*"} - | @@{command "Theorem*"} | @@{command "Conjecture*"} ) \ '[' meta_args ']' '\' text '\' diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 1b9bece..8b48e81 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -65,7 +65,7 @@ print_doc_classes doc_class figure = relative_width :: "int" (* percent of textwidth *) src :: "string" - placement :: placement <= "pl_h" + placement :: placement spawn_columns :: bool <= True diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 91a83ed..f61e8a2 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1251,6 +1251,23 @@ fun enriched_formal_statement_command (cat:string,tag:string) = in gen_enriched_document_command transform end; +fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), + prop) = + let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy)) + fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") + ::doc_attrs + fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy) + fun mks thy = case DOF_core.get_object_global_opt oid thy of + SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) + | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) + | NONE => (create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy) + val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global + in + (* Toplevel.keep (check o Toplevel.context_of) *) + Toplevel.theory (fn thy => (check thy; mks thy)) + end + + fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) = let fun o_m_c oid pos cid_pos doc_attrs thy = create_and_check_docitem true oid pos cid_pos doc_attrs thy @@ -1412,22 +1429,6 @@ val _ = (attributes_upd >> (Toplevel.theory o update_instance_command)); -fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), - prop) = - let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy)) - fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") - ::doc_attrs - fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy) - fun mks thy = case DOF_core.get_object_global_opt oid thy of - SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) - | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) - | NONE => (create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy) - val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global - in - (* Toplevel.keep (check o Toplevel.context_of) *) - Toplevel.theory (fn thy => (check thy; mks thy)) - end - val _ = Outer_Syntax.command @{command_keyword "assert*"} "evaluate and print term" diff --git a/src/DOF/latex/DOF-COL.sty b/src/DOF/latex/DOF-COL.sty index 73851af..57d8155 100644 --- a/src/DOF/latex/DOF-COL.sty +++ b/src/DOF/latex/DOF-COL.sty @@ -55,6 +55,7 @@ \newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}% [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=% diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty index a4f59bf..2b2602a 100644 --- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty +++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty @@ -412,23 +412,26 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \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 =% + , scholarly_paper.example.status =% + , scholarly_paper.example.short_name =% ] [1] {% \begin{isamarkuptext}% - \ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{ - \ifthenelse{\equal{\commandkey{scholarly_paper.example.tag}} {} } + \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.tag}] \label{\commandkey{label}} #1 \end{example}} - }{% + {\begin{example} [\commandkey{scholarly_paper.example.short_name}] % + \label{\commandkey{label}} #1 % + \end{example}} % + }% + {% #1% }% \end{isamarkuptext}% diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index d01ade9..e2d95e9 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -116,6 +116,19 @@ doc_class technical = text_section + type_synonym tc = technical (* technical content *) +text \This a \doc_class\ of \<^verbatim>\examples\ in the broadest possible sense : they are \emph{not} +necessarily considered as technical content, but may occur in an article. +Note that there are \doc_class\es of \<^verbatim>\math_example\s and \<^verbatim>\tech_example\s which +follow a more specific regime of mathematical or engineering content. +\ +(* An example for the need of multiple inheritance on classes ? *) + +doc_class example = text_section + + referentiable :: bool <= True + status :: status <= "description" + short_name :: string <= "''''" + + subsection\Mathematical Content\ text\We follow in our enumeration referentiable mathematical content class the AMS style and its @@ -169,12 +182,6 @@ doc_class math_explanation = tc + referentiable :: bool <= False type_synonym math_exp = math_explanation -doc_class math_example = tc + - referentiable :: bool <= False - short_name :: string <= "''''" - invariant s3 :: "\ \::math_example. \referentiable \ \ short_name \ = ''''" -type_synonym math_ex = math_example - text\The intended use for the \doc_class\ \<^verbatim>\math_semiformal_statement\ (or \<^verbatim>\math_sfs\ for short) are semi-formal mathematical content (definition, lemma, etc.). They are referentiable entities. @@ -208,10 +215,10 @@ doc_class "corollary" = math_content + mcc :: "math_content_class" <= "cor" invariant d4 :: "\ \::corollary. mcc \ = thm" -doc_class "example" = math_content + +doc_class "math_example" = math_content + referentiable :: bool <= "True" mcc :: "math_content_class" <= "expl" - invariant d5 :: "\ \::example. mcc \ = expl" + invariant d5 :: "\ \::math_example. mcc \ = expl" subsection\Example Statements\ @@ -255,18 +262,18 @@ doc_class "LATEX" = code + subsection\Content in Engineering/Tech Papers \ -doc_class engineering_statement = tc + +doc_class engineering_content = tc + short_name :: string <= "''''" status :: status -type_synonym eng_stmt = engineering_statement +type_synonym eng_c = engineering_content -doc_class "experiment" = eng_stmt + +doc_class "experiment" = eng_c + tag :: "string" <= "''''" -doc_class "evaluation" = eng_stmt + +doc_class "evaluation" = eng_c + tag :: "string" <= "''''" -doc_class "data" = eng_stmt + +doc_class "data" = eng_c + tag :: "string" <= "''''" @@ -307,7 +314,7 @@ doc_class article = \author\\<^sup>+ ~~ abstract ~~ \introduction\\<^sup>+ ~~ - \technical\\<^sup>+ ~~ + \technical || example \\<^sup>+ ~~ \conclusion\\<^sup>+ ~~ bibliography ~~ \annex\\<^sup>* )" diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index 8d818e9..4af8900 100644 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -40,7 +40,7 @@ doc_class report = abstract ~~ \table_of_contents\ ~~ \introduction\\<^sup>+ ~~ - \technical || example\\<^sup>+ ~~ + \technical || figure || side_by_side_figure\\<^sup>+ ~~ \conclusion\\<^sup>+ ~~ \index\\<^sup>* ~~ bibliography)"