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

Update documentation and some refactoring

This commit is contained in:
Nicolas Méric 2023-05-15 10:48:40 +02:00
parent 7e698a9e69
commit ba7c0711a8
2 changed files with 35 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
Isabelle_DOF/thys/Isa_COL.thy
View File

@ -395,24 +395,42 @@ fun float_command (name, pos) descr cid =
{is_monitor = false} {is_monitor = false}
{is_inline = true} {is_inline = true}
{define = true} oid pos (set_default_class cid_pos) doc_attrs {define = true} oid pos (set_default_class cid_pos) doc_attrs
fun parse_and_tex (margs, text) ctxt = (convert_src_from_margs ctxt margs) fun generate_fig_ltx_ctxt ctxt cap_src oid body =
|> pair (upd_caption Input.empty #> convert_meta_args ctxt margs) Latex.macro0 "centering"
|> fig_content ctxt @ body
|> (fn X => (Latex.macro0 "centering" @ Latex.macro "caption" (generate_caption ctxt cap_src)
@ X @ Latex.macro "label" (DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt)
@ Latex.macro "caption" (generate_caption ctxt text))) |> DOF_core.output_name
(* TODO: add label *) |> Latex.string)
|> (Latex.environment ("figure") ) fun parse_and_tex (margs as (((oid, _),_), _), cap_src) ctxt =
(convert_src_from_margs ctxt margs)
|> pair (upd_caption Input.empty #> convert_meta_args ctxt margs)
|> fig_content ctxt
|> generate_fig_ltx_ctxt ctxt cap_src oid
|> (Latex.environment ("figure") )
in Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex in Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex
end end
fun listing_command (name, pos) descr cid =
let fun set_default_class NONE = SOME(cid,pos)
|set_default_class (SOME X) = SOME X
fun create_instance ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false}
{is_inline = true}
{define = true} oid pos (set_default_class cid_pos) doc_attrs
fun parse_and_tex (margs as (((_, pos),_), _), _) _ =
ISA_core.err ("Not yet implemented.\n Please use text*[oid::listing]\<open>\<close> instead.") pos
in Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex
end
(* *********************************************************************** *) (* *********************************************************************** *)
(* Ontological Macro Command Support *) (* Ontological Macro Command Support *)
(* *********************************************************************** *) (* *********************************************************************** *)
val _ = float_command \<^command_keyword>\<open>figure*\<close> "figure" "Isa_COL.figure" ; val _ = float_command \<^command_keyword>\<open>figure*\<close> "figure" "Isa_COL.figure" ;
val _ = float_command \<^command_keyword>\<open>listing*\<close> "figure" "Isa_COL.listing" ; (* Hack ! *) val _ = listing_command \<^command_keyword>\<open>listing*\<close> "listing" "Isa_COL.listing" ; (* Hack ! *)
\<close> \<close>

14
Isabelle_DOF/thys/manual/M_04_RefMan.thy
View File

@ -497,12 +497,14 @@ text*[b::B'_test']\<open>\<close>
term*\<open>@{B--test- \<open>b\<close>}\<close>\<close>} term*\<open>@{B--test- \<open>b\<close>}\<close>\<close>}
The major commands providing term-contexts are The major commands providing term-contexts are\<^footnote>\<open>The meta-argument list is optional.\<close>
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>, \<^item> \<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>,
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>, and \<^item> \<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>, and
\<^theory_text>\<open>assert*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close> \<^item> \<^theory_text>\<open>assert*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>
\<^theory_text>\<open>definition*[oid::cid, ...] const_name where \<open> \<dots> HOL-term \<dots> \<close>\<close>, and \<^item> \<^theory_text>\<open>definition*[oid::cid, ...] const_name where \<open> \<dots> HOL-term \<dots> \<close>\<close>, and
\<^theory_text>\<open>lemma*[oid::cid, ...] name :: \<open> \<dots> HOL-term \<dots> \<close>\<close>. \<^item> \<^theory_text>\<open>lemma*[oid::cid, ...] name :: \<open> \<dots> HOL-term \<dots> \<close>\<close>.
Wrt. creation, checking and traceability, these commands are analogous to the ontological text and Wrt. creation, checking and traceability, these commands are analogous to the ontological text and
code-commands. However the argument terms may contain term-antiquotations stemming from an code-commands. However the argument terms may contain term-antiquotations stemming from an
ontology definition. Term-contexts were type-checked and \<^emph>\<open>validated\<close> against ontology definition. Term-contexts were type-checked and \<^emph>\<open>validated\<close> against