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

Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF

This commit is contained in:
Burkhart Wolff 2023-03-06 16:54:14 +01:00
parent 224a320165 92e7ee017a
commit f60aebccb3
3 changed files with 12 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy
View File

@ -79,10 +79,10 @@ text-assert-error[c1::C, x = "''gamma''"]
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
... @{C "c1"} or @{C \<open>c1\<close>} or \<^C>\<open>c1\<close>
similar to @{thm "refl"} and \<^thm>"refl"\<close> \<comment> \<open>ontological and built-in
references\<close>
text\<open>Not only text-elements are "ontology-aware", proofs and code can this be too !\<close>
references\<close>
\<comment> \<open>Referencing from and to a ML-code context:\<close>
(*<*)
ML*[c4::C, z = "Some @{A \<open>a1\<close>}"]\<open>
@ -102,11 +102,9 @@ text\<open>This is the answer to the "OutOfOrder Presentation Problem": @{E (unc
definition*[e6::E] facu :: "nat \<Rightarrow> nat" where "facu arg = undefined"
text\<open>As shown in @{E \<open>e5\<close>} following from @{E \<open>e6\<close>}\<close>
text\<open>As shown in @{E [display]\<open>e5\<close>} following from @{E [display]\<open>e6\<close>}\<close>
(* BUG ?: why is option [display] necessary ? *)
text\<open>As shown in @{C [display]\<open>c4\<close>}\<close>
text\<open>As shown in @{C \<open>c4\<close>}\<close>
@ -116,8 +114,7 @@ update_instance*[d::D, a1 := X2]
text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>} ... \<close> \<comment> \<open>untyped or typed referencing \<close>
(* THIS IS A BUG : this weird option is necessary *)
text-assert-error[ae::text_element]\<open>the function @{C [display] "c4"} \<close>\<open>referred text-element is macro!\<close>
text-assert-error[ae::text_element]\<open>the function @{C [display] "c4"} \<close>\<open>referred text-element is no macro!\<close>
text*[c2::C, x = "\<open>delta\<close>"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>

4
Isabelle_DOF-Unit-Tests/Evaluation.thy
View File

@ -59,7 +59,7 @@ section\<open>Term Annotation evaluation\<close>
text\<open>We can validate a term with TA:\<close>
term*[axx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
text\<open>check : @{A [display] "axx"}\<close>
text\<open>check : @{A "axx"}\<close>
text\<open>Now we can evaluate a term with TA:
the current implementation return the term which references the object referenced by the TA.
@ -69,7 +69,7 @@ value*\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>syntax che
value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>defining a reference of class A\<close>
text\<open>check : @{A [display] "axxx"}\<close> \<comment> \<open>using it\<close>
text\<open>check : @{A "axxx"}\<close> \<comment> \<open>using it\<close>
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

10
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -1796,7 +1796,7 @@ fun meta_args_exec (meta_args as (((oid, pos), cid_pos), doc_attrs) : ODL_Meta_A
thy |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args
then (K thy)
else Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false} {define = true}
{is_monitor = false} {is_inline = true} {define = true}
oid pos (I cid_pos) (I doc_attrs))
fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t pos thy =
@ -2300,7 +2300,7 @@ fun meta_args_exec (meta_args as (((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Ar
ctxt |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args
then (K ctxt)
else Context.map_theory (Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false}
{is_monitor = false} {is_inline = true}
{define = true} oid pos (I cid_pos) (I doc_attrs))
)
@ -2668,9 +2668,9 @@ fun check_and_mark ctxt cid_decl ({strict_checking = strict}) {inline=inline_req
then if defined
then ISA_core.warn ("Instance defined, unchecked option useless") pos
else ()
else if defined
then ()
else ISA_core.err ("Instance declared but not defined, try option unchecked") pos
else if defined
then ()
else ISA_core.err ("Instance declared but not defined, try option unchecked") pos
val _ = if not inline_req
then if inline then () else error("referred text-element is macro! (try option display)")
else if not inline then () else error("referred text-element is no macro!")