diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index c9ca1c9..22681f0 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -45,7 +45,7 @@ we follow LaTeX terminology on levels for scholarly paper: invariant level > 0. \ -doc_class text_element = +doc_class text_element = level :: "int option" <= "None" referentiable :: bool <= "False" variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}" diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 6ea0717..2cff442 100755 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -41,7 +41,8 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) 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 *) and "corrollary*" "proposition*" "lemma*" "theorem*" :: thy_decl @@ -641,6 +642,20 @@ fun print_doc_items b ctxt = in map print_item (Symtab.dest x); 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 = let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt; val _ = writeln "====================================="; @@ -676,6 +691,12 @@ val _ = Outer_Syntax.command \<^command_keyword>\print_doc_classes\ "print document classes" (Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_classes b o Toplevel.context_of))); +val _ = + Outer_Syntax.command \<^command_keyword>\print_doc_class_template\ + "print document class latex template" + (Parse.string >> (fn b => Toplevel.keep (print_docclass_template b o Toplevel.context_of))); + + val _ = Outer_Syntax.command \<^command_keyword>\print_doc_items\ "print document items" (Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of))); diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 36fea4a..a80af43 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -287,6 +287,12 @@ doc_class "evaluation" = eng_c + doc_class "data" = eng_c + tag :: "string" <= "''''" +subsection\Some Summary\ + +print_doc_classes + +print_doc_class_template "definition" (* just a sample *) + subsection\Structuring Enforcement in Engineering/Math Papers \ (* todo : could be finer *) @@ -413,6 +419,5 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ; \ - end