Restructuring library prep.
This commit is contained in:
parent
9496b535b7
commit
8328626fa4
|
|
@ -538,7 +538,6 @@ text\<open>
|
|||
| @@{command "text*"} | @@{command "figure*"} | @@{command "side_by_side_figure*"}
|
||||
| @@{command "open_monitor*"} | @@{command "close_monitor*"}
|
||||
| @@{command "Definition*"} | @@{command "Lemma*"}
|
||||
| @@{command "Theorem*"} | @@{command "Conjecture*"}
|
||||
)
|
||||
\<newline>
|
||||
'[' meta_args ']' '\<open>' text '\<close>'
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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=%
|
||||
|
|
|
|||
|
|
@ -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}%
|
||||
|
|
|
|||
|
|
@ -116,6 +116,19 @@ doc_class technical = text_section +
|
|||
type_synonym tc = technical (* technical content *)
|
||||
|
||||
|
||||
text \<open>This a \<open>doc_class\<close> of \<^verbatim>\<open>examples\<close> in the broadest possible sense : they are \emph{not}
|
||||
necessarily considered as technical content, but may occur in an article.
|
||||
Note that there are \<open>doc_class\<close>es of \<^verbatim>\<open>math_example\<close>s and \<^verbatim>\<open>tech_example\<close>s which
|
||||
follow a more specific regime of mathematical or engineering content.
|
||||
\<close>
|
||||
(* 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\<open>Mathematical Content\<close>
|
||||
|
||||
text\<open>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 :: "\<lambda> \<sigma>::math_example. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
|
||||
type_synonym math_ex = math_example
|
||||
|
||||
|
||||
text\<open>The intended use for the \<open>doc_class\<close> \<^verbatim>\<open>math_semiformal_statement\<close> (or \<^verbatim>\<open>math_sfs\<close> 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 :: "\<lambda> \<sigma>::corollary. mcc \<sigma> = thm"
|
||||
|
||||
doc_class "example" = math_content +
|
||||
doc_class "math_example" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
mcc :: "math_content_class" <= "expl"
|
||||
invariant d5 :: "\<lambda> \<sigma>::example. mcc \<sigma> = expl"
|
||||
invariant d5 :: "\<lambda> \<sigma>::math_example. mcc \<sigma> = expl"
|
||||
|
||||
|
||||
subsection\<open>Example Statements\<close>
|
||||
|
|
@ -255,18 +262,18 @@ doc_class "LATEX" = code +
|
|||
subsection\<open>Content in Engineering/Tech Papers \<close>
|
||||
|
||||
|
||||
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 =
|
|||
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
||||
abstract ~~
|
||||
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>technical\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>technical || example \<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
||||
bibliography ~~
|
||||
\<lbrace>annex\<rbrace>\<^sup>* )"
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ doc_class report =
|
|||
abstract ~~
|
||||
\<lbrakk>table_of_contents\<rbrakk> ~~
|
||||
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>technical || figure || side_by_side_figure\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>index\<rbrace>\<^sup>* ~~
|
||||
bibliography)"
|
||||
|
|
|
|||
Loading…
Reference in New Issue