forked from Isabelle_DOF/Isabelle_DOF
Code Cleanup.
This commit is contained in:
parent
ef3eee03c9
commit
48c6457f63
|
@ -23,30 +23,11 @@ keywords "text-" "text-latex" :: document_body
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
section\<open>Testing Commands (exec-catch-verify - versions of std commands)\<close>
|
||||||
|
|
||||||
|
|
||||||
text\<open>Current status:\<close>
|
|
||||||
print_doc_classes
|
|
||||||
print_doc_items
|
|
||||||
|
|
||||||
(* this corresponds to low-level accesses : *)
|
|
||||||
ML\<open>
|
|
||||||
val docitem_tab = DOF_core.get_instances \<^context>;
|
|
||||||
val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>;
|
|
||||||
val docclass_tab = DOF_core.get_onto_classes \<^context>;
|
|
||||||
|
|
||||||
Name_Space.dest_table docitem_tab;
|
|
||||||
Name_Space.dest_table isa_transformer_tab;
|
|
||||||
Name_Space.dest_table docclass_tab;
|
|
||||||
app;
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
|
|
||||||
ML\<open>
|
ML\<open>
|
||||||
|
|
||||||
val _ = Document_Output.document_output
|
|
||||||
|
|
||||||
fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown
|
fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown
|
||||||
(((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
|
(((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
|
||||||
xstring_opt:(xstring * Position.T) option),
|
xstring_opt:(xstring * Position.T) option),
|
||||||
|
|
Loading…
Reference in New Issue