forked from Isabelle_DOF/Isabelle_DOF
Added syntactic constants for classes (for proper
regexp parsing support).
This commit is contained in:
parent
2acc4ea222
commit
6aa563df17
|
@ -49,7 +49,7 @@ term "@{term ''Bound 0''}"
|
||||||
term "@{thm ''refl''}"
|
term "@{thm ''refl''}"
|
||||||
term "@{docitem ''<doc_ref>''}"
|
term "@{docitem ''<doc_ref>''}"
|
||||||
|
|
||||||
|
type_synonym monitor = "int rexp"
|
||||||
|
|
||||||
section{*Primitive Markup Generators*}
|
section{*Primitive Markup Generators*}
|
||||||
ML{*
|
ML{*
|
||||||
|
@ -732,11 +732,14 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef
|
||||||
else error("no overloading allowed.")
|
else error("no overloading allowed.")
|
||||||
val gen_antiquotation = OntoLinkParser.docitem_ref_antiquotation
|
val gen_antiquotation = OntoLinkParser.docitem_ref_antiquotation
|
||||||
val _ = map_filter (check_n_filter thy) fields
|
val _ = map_filter (check_n_filter thy) fields
|
||||||
|
val H = Sign.add_consts_cmd [(binding,"monitor",Mixfix.NoSyn)]
|
||||||
|
|
||||||
in thy |> Record.add_record overloaded (params', binding) parent (tag_attr::fields)
|
in thy |> Record.add_record overloaded (params', binding) parent (tag_attr::fields)
|
||||||
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
|
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
|
||||||
|> (fn thy => gen_antiquotation binding (cid thy) thy)
|
|> (fn thy => gen_antiquotation binding (cid thy) thy)
|
||||||
(* defines the ontology-checked text antiquotation to this document class *)
|
(* defines the ontology-checked text antiquotation to this document class *)
|
||||||
|
|> Sign.add_consts_cmd [(binding,"monitor",Mixfix.NoSyn)]
|
||||||
|
(* defines syntax for monitor regeexpr for this class *)
|
||||||
end;
|
end;
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -312,6 +312,7 @@ Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> st
|
||||||
Thy_Output.output : Proof.context -> Pretty.T list -> string;
|
Thy_Output.output : Proof.context -> Pretty.T list -> string;
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
section {* The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts *}
|
section {* The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts *}
|
||||||
|
|
||||||
ML{*
|
ML{*
|
||||||
|
|
|
@ -27,7 +27,7 @@ doc_class requirement =
|
||||||
|
|
||||||
doc_class requirement_analysis =
|
doc_class requirement_analysis =
|
||||||
no :: "nat"
|
no :: "nat"
|
||||||
where "\<lbrace>requirement_item\<rbrace>\<^sup>+"
|
where "\<lbrace>requirement\<rbrace>\<^sup>+"
|
||||||
|
|
||||||
|
|
||||||
text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions from the
|
text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions from the
|
||||||
|
@ -140,8 +140,8 @@ doc_class test_documentation =
|
||||||
no :: "nat"
|
no :: "nat"
|
||||||
where "test_specification ~~ \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
where "test_specification ~~ \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||||
\<lbrakk>test_requirement\<rbrakk> ~~ test_adm_role"
|
\<lbrakk>test_requirement\<rbrakk> ~~ test_adm_role"
|
||||||
where " test_specification ~~\<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
where " test_specification ~~ \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||||
\<lbrakk> test_requirement \<rbrakk> ~~ test_adm_role"
|
\<lbrakk>test_requirement \<rbrakk> ~~ test_adm_role"
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -19,10 +19,10 @@ doc_class D = B +
|
||||||
|
|
||||||
doc_class F =
|
doc_class F =
|
||||||
r :: "thm list"
|
r :: "thm list"
|
||||||
b :: "(A \<times> C) set" <= "{}"
|
b :: "(A \<times> C) set" <= "{}"
|
||||||
|
|
||||||
doc_class M =
|
doc_class M =
|
||||||
trace :: "(A + C + D + F) list"
|
trace :: "(A + C + D + F) list"
|
||||||
where "A . (C | D)* . [F]"
|
where "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
|
||||||
|
|
||||||
end
|
end
|
|
@ -54,10 +54,10 @@ doc_class figure = text_section +
|
||||||
doc_class example = text_section +
|
doc_class example = text_section +
|
||||||
comment :: "string"
|
comment :: "string"
|
||||||
|
|
||||||
doc_class conclusion = text_section +
|
doc_class "conclusion" = text_section +
|
||||||
main_author :: "author option" <= None
|
main_author :: "author option" <= None
|
||||||
|
|
||||||
doc_class related_work = conclusion +
|
doc_class related_work = "conclusion" +
|
||||||
main_author :: "author option" <= None
|
main_author :: "author option" <= None
|
||||||
|
|
||||||
doc_class bibliography =
|
doc_class bibliography =
|
||||||
|
|
Loading…
Reference in New Issue