added a little useful template generation command
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit
Details
Isabelle_DOF/Isabelle_DOF/pipeline/head There was a failure building this commit
Details
This commit is contained in:
parent
f5622c2f59
commit
ef93285ec7
|
@ -45,7 +45,7 @@ we follow LaTeX terminology on levels
|
||||||
|
|
||||||
for scholarly paper: invariant level > 0. \<close>
|
for scholarly paper: invariant level > 0. \<close>
|
||||||
|
|
||||||
doc_class text_element =
|
doc_class text_element =
|
||||||
level :: "int option" <= "None"
|
level :: "int option" <= "None"
|
||||||
referentiable :: bool <= "False"
|
referentiable :: bool <= "False"
|
||||||
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
||||||
|
|
|
@ -41,7 +41,8 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||||
|
|
||||||
and "text*" "text-macro*" :: document_body
|
and "text*" "text-macro*" :: document_body
|
||||||
|
|
||||||
and "print_doc_classes" "print_doc_items" "check_doc_global" :: diag
|
and "print_doc_classes" "print_doc_items"
|
||||||
|
"print_doc_class_template" "check_doc_global" :: diag
|
||||||
|
|
||||||
(* experimental *)
|
(* experimental *)
|
||||||
and "corrollary*" "proposition*" "lemma*" "theorem*" :: thy_decl
|
and "corrollary*" "proposition*" "lemma*" "theorem*" :: thy_decl
|
||||||
|
@ -641,6 +642,20 @@ fun print_doc_items b ctxt =
|
||||||
in map print_item (Symtab.dest x);
|
in map print_item (Symtab.dest x);
|
||||||
writeln "=====================================\n\n\n" end;
|
writeln "=====================================\n\n\n" end;
|
||||||
|
|
||||||
|
|
||||||
|
fun print_docclass_template cid ctxt =
|
||||||
|
let val cid_long = read_cid ctxt cid (* assure that given cid is really a long_cid *)
|
||||||
|
val brute_hierarchy = (get_attributes_local cid_long ctxt)
|
||||||
|
val flatten_hrchy = flat o (map(fn(lname, attrS) =>
|
||||||
|
map (fn (s,_,_)=>(lname,(Binding.name_of s))) attrS))
|
||||||
|
fun filter_overrides [] = []
|
||||||
|
|filter_overrides ((ln,s)::S) = (ln,s):: filter_overrides(filter(fn(_,s')=> s<>s')S)
|
||||||
|
val hierarchy = map (fn(ln,s)=>ln^"."^s)(filter_overrides(flatten_hrchy brute_hierarchy))
|
||||||
|
val args = String.concatWith "=%\n , " (" label=,type":: hierarchy);
|
||||||
|
val template = "\\newisadof{"^cid_long^"}%\n["^args^"][1]\n{%\n#1%\n}\n\n";
|
||||||
|
in writeln template end;
|
||||||
|
|
||||||
|
|
||||||
fun print_doc_classes b ctxt =
|
fun print_doc_classes b ctxt =
|
||||||
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt;
|
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt;
|
||||||
val _ = writeln "=====================================";
|
val _ = writeln "=====================================";
|
||||||
|
@ -676,6 +691,12 @@ val _ =
|
||||||
Outer_Syntax.command \<^command_keyword>\<open>print_doc_classes\<close> "print document classes"
|
Outer_Syntax.command \<^command_keyword>\<open>print_doc_classes\<close> "print document classes"
|
||||||
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_classes b o Toplevel.context_of)));
|
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_classes b o Toplevel.context_of)));
|
||||||
|
|
||||||
|
val _ =
|
||||||
|
Outer_Syntax.command \<^command_keyword>\<open>print_doc_class_template\<close>
|
||||||
|
"print document class latex template"
|
||||||
|
(Parse.string >> (fn b => Toplevel.keep (print_docclass_template b o Toplevel.context_of)));
|
||||||
|
|
||||||
|
|
||||||
val _ =
|
val _ =
|
||||||
Outer_Syntax.command \<^command_keyword>\<open>print_doc_items\<close> "print document items"
|
Outer_Syntax.command \<^command_keyword>\<open>print_doc_items\<close> "print document items"
|
||||||
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of)));
|
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of)));
|
||||||
|
|
|
@ -287,6 +287,12 @@ doc_class "evaluation" = eng_c +
|
||||||
doc_class "data" = eng_c +
|
doc_class "data" = eng_c +
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
|
subsection\<open>Some Summary\<close>
|
||||||
|
|
||||||
|
print_doc_classes
|
||||||
|
|
||||||
|
print_doc_class_template "definition" (* just a sample *)
|
||||||
|
|
||||||
|
|
||||||
subsection\<open>Structuring Enforcement in Engineering/Math Papers \<close>
|
subsection\<open>Structuring Enforcement in Engineering/Math Papers \<close>
|
||||||
(* todo : could be finer *)
|
(* todo : could be finer *)
|
||||||
|
@ -413,6 +419,5 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ;
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue