Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

added value* metaargs option.

This commit is contained in:
Burkhart Wolff 2022-02-24 14:37:58 +01:00
parent 01c196086b
commit 6863995671
2 changed files with 19 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/DOF/Isa_DOF.thy
View File

@ -1846,12 +1846,26 @@ val opt_evaluator =
We want to have the current position to pass it to transduce_term_global in
value_cmd, so we pass the Toplevel.transition
*)
val opt_attributes = Scan.option ODL_Command_Parser.attributes
fun meta_args_exec NONE thy = thy
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy =
thy |> (ODL_Command_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false}
oid pos (I cid_pos) (I doc_attrs))
fun pass_trans_to_value_cmd ((name, modes), t) trans =
Toplevel.keep (fn state => value_cmd name modes t state trans) trans
val _ =
Outer_Syntax.command \<^command_keyword>\<open>value*\<close> "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term >> pass_trans_to_value_cmd);
(opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
>> (fn (meta_args_opt, eval_args ) =>
Toplevel.theory (meta_args_exec meta_args_opt)
#>
pass_trans_to_value_cmd eval_args));
val _ = Theory.setup
(Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value*\<close>
@ -1881,10 +1895,11 @@ fun meta_args_exec NONE thy = thy
{is_monitor = false} {is_inline = false}
oid pos (I cid_pos) (I doc_attrs))
val attributes_opt = Scan.option ODL_Command_Parser.attributes
val _ =
Outer_Syntax.command ("ML*", \<^here>) "ODL annotated ML text within theory or local theory"
(((Scan.option ODL_Command_Parser.attributes) -- Parse.ML_source)
((attributes_opt -- Parse.ML_source)
>> (fn (meta_args_opt, source) =>
Toplevel.theory (meta_args_exec meta_args_opt)
#>

2
src/tests/Evaluation.thy
View File

@ -57,6 +57,8 @@ Here the evualuation of the TA will return the HOL.String which references the t
\<close>
value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
value*[a::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the opption *)
text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
It is a concept which will be used to implement an ontology. It has roughly the same meaning as
an individual in an OWL ontology.