forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
1ea897e660
|
@ -41,7 +41,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||||
"define_shortcut*" "define_macro*" :: thy_decl
|
"define_shortcut*" "define_macro*" :: thy_decl
|
||||||
|
|
||||||
and "text*" "text-macro*" :: document_body
|
and "text*" "text-macro*" :: document_body
|
||||||
and "term*" "value*" "assert*" :: diag
|
and "term*" "value*" "assert*" :: document_body
|
||||||
|
|
||||||
and "print_doc_classes" "print_doc_items"
|
and "print_doc_classes" "print_doc_items"
|
||||||
"print_doc_class_template" "check_doc_global" :: diag
|
"print_doc_class_template" "check_doc_global" :: diag
|
||||||
|
@ -1892,9 +1892,8 @@ end
|
||||||
and adds the possibility to check Term Annotation Antiquotations (TA)
|
and adds the possibility to check Term Annotation Antiquotations (TA)
|
||||||
with the help of DOF_core.transduce_term_global function
|
with the help of DOF_core.transduce_term_global function
|
||||||
*)
|
*)
|
||||||
fun string_of_term meta_args_opt s pos ctxt =
|
fun string_of_term s pos ctxt =
|
||||||
let
|
let
|
||||||
val SS = meta_args_exec meta_args_opt
|
|
||||||
val t = Syntax.read_term ctxt s;
|
val t = Syntax.read_term ctxt s;
|
||||||
val T = Term.type_of t;
|
val T = Term.type_of t;
|
||||||
val ctxt' = Proof_Context.augment t ctxt;
|
val ctxt' = Proof_Context.augment t ctxt;
|
||||||
|
@ -1906,21 +1905,46 @@ in
|
||||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
|
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
|
||||||
end;
|
end;
|
||||||
|
|
||||||
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
|
fun print_item string_of (modes, arg) state =
|
||||||
Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
|
Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ();
|
||||||
|
|
||||||
(*
|
(*
|
||||||
We want to have the current position to pass it to transduce_term_global in
|
We want to have the current position to pass it to transduce_term_global in
|
||||||
string_of_term, so we pass the Toplevel.transition
|
string_of_term, so we pass the Toplevel.transition
|
||||||
*)
|
*)
|
||||||
|
(*
|
||||||
fun print_term meta_args_opt (string_list, string) trans =
|
fun print_term meta_args_opt (string_list, string) trans =
|
||||||
let
|
let
|
||||||
val pos = Toplevel.pos_of trans
|
val pos = Toplevel.pos_of trans
|
||||||
in
|
in
|
||||||
print_item (fn state =>
|
Toplevel.keep(fn state =>
|
||||||
fn string => string_of_term meta_args_opt string pos (Toplevel.context_of state) )
|
print_item
|
||||||
(string_list, string) trans
|
(fn state =>
|
||||||
|
fn string =>
|
||||||
|
string_of_term meta_args_opt string pos (Toplevel.context_of state) )
|
||||||
|
(string_list, string)
|
||||||
|
(state)
|
||||||
|
) trans
|
||||||
end
|
end
|
||||||
|
*)
|
||||||
|
|
||||||
|
fun print_term meta_args_opt (string_list, string) trans =
|
||||||
|
let
|
||||||
|
val pos = Toplevel.pos_of trans
|
||||||
|
in
|
||||||
|
Toplevel.theory(fn thy =>
|
||||||
|
(print_item
|
||||||
|
(fn state =>
|
||||||
|
fn string =>
|
||||||
|
string_of_term string pos (Toplevel.context_of state) )
|
||||||
|
(string_list, string)
|
||||||
|
(Toplevel.theory_toplevel thy);
|
||||||
|
thy |> meta_args_exec meta_args_opt )
|
||||||
|
) trans
|
||||||
|
end
|
||||||
|
|
||||||
|
val _ = Toplevel.theory
|
||||||
|
val _ = Toplevel.theory_toplevel
|
||||||
|
|
||||||
val _ =
|
val _ =
|
||||||
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
|
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
|
||||||
|
@ -2061,10 +2085,10 @@ val _ =
|
||||||
(*Toplevel.theory (meta_args_exec meta_args_opt)
|
(*Toplevel.theory (meta_args_exec meta_args_opt)
|
||||||
#>*)
|
#>*)
|
||||||
Toplevel.generic_theory
|
Toplevel.generic_theory
|
||||||
(ML_Context.exec (fn () =>
|
((ML_Context.exec (fn () =>
|
||||||
(ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))
|
(ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))
|
||||||
#> (meta_args_exec meta_args_opt)
|
#> (meta_args_exec meta_args_opt)
|
||||||
#> Local_Theory.propagate_ml_env)));
|
#> Local_Theory.propagate_ml_env))));
|
||||||
|
|
||||||
end
|
end
|
||||||
\<close>
|
\<close>
|
||||||
|
|
|
@ -54,7 +54,9 @@ of the current implementation.
|
||||||
section\<open>Term Annotation evaluation\<close>
|
section\<open>Term Annotation evaluation\<close>
|
||||||
|
|
||||||
text\<open>We can validate a term with TA:\<close>
|
text\<open>We can validate a term with TA:\<close>
|
||||||
term*\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
term*[axx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
||||||
|
|
||||||
|
text\<open>check : @{A [display] "axx"}\<close>
|
||||||
|
|
||||||
text\<open>Now we can evaluate a term with TA:
|
text\<open>Now we can evaluate a term with TA:
|
||||||
the current implementation return the term which references the object referenced by the TA.
|
the current implementation return the term which references the object referenced by the TA.
|
||||||
|
@ -62,11 +64,11 @@ Here the evualuation of the TA will return the HOL.String which references the t
|
||||||
\<close>
|
\<close>
|
||||||
value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
||||||
|
|
||||||
value*[axx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the option *)
|
value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the option *)
|
||||||
|
|
||||||
value*[axx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
value*[axxxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
|
||||||
|
|
||||||
text\<open>check : @{A "ax"}\<close>
|
text\<open>check : @{A [display] "axxx"}\<close>
|
||||||
|
|
||||||
text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
|
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
|
It is a concept which will be used to implement an ontology. It has roughly the same meaning as
|
||||||
|
|
Reference in New Issue