nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Code cleanup

This commit is contained in:
Burkhart Wolff 2023-03-04 10:12:05 +01:00
parent 280feb8653
commit 853158c916
1 changed files with 11 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -2228,13 +2228,18 @@ val _ =
{markdown = true, body = true}
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>declare_reference*\<close>
val _ =
let fun create_and_check_docitem (((oid, pos),cid_pos),doc_attrs)
= (Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline=true}
{define = false} oid pos (cid_pos) (doc_attrs))
in Outer_Syntax.command \<^command_keyword>\<open>declare_reference*\<close>
"declare document reference"
(ODL_Meta_Args_Parser.attributes >> (fn (((oid, pos),cid_pos),doc_attrs) =>
(Toplevel.theory (Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline=true}
{define = false} oid pos (cid_pos) (doc_attrs)))));
(ODL_Meta_Args_Parser.attributes
>> (Toplevel.theory o create_and_check_docitem))
end;
end (* structure Monitor_Command_Parser *)
\<close>