From 85f115196b7df3fe2d73f4b9ff8bae1c044f3c2d Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 22 Feb 2023 22:46:25 +0000 Subject: [PATCH] Changed theory dependencies, allowing retirement of use_ontology_unchecked (fixes #25). --- .../CC_v3_1_R5/CC_terminology.thy | 1 - .../CENELEC_50128/CENELEC_50128.thy | 2 +- .../Conceptual/Conceptual.thy | 1 - Isabelle_DOF-Ontologies/document_setup.thy | 6 +++--- .../small_math/small_math.thy | 1 - Isabelle_DOF/thys/Isa_DOF.thy | 16 +++++----------- 6 files changed, 9 insertions(+), 18 deletions(-) diff --git a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy index 7d77b0d..4cf8c70 100644 --- a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy +++ b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy @@ -17,7 +17,6 @@ section\Terminology\ theory CC_terminology imports -"document_setup" "Isabelle_DOF.technical_report" begin diff --git a/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy b/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy index d31b271..97d54ac 100644 --- a/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy @@ -27,7 +27,7 @@ identifies: theory CENELEC_50128 imports - "document_setup" + "Isabelle_DOF.technical_report" begin define_ontology "DOF-CENELEC_50128.sty" diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index b3b359d..bc2b81a 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -16,7 +16,6 @@ chapter\A conceptual introduction into DOF and its features:\ theory Conceptual imports -"document_setup" "Isabelle_DOF.Isa_DOF" "Isabelle_DOF.Isa_COL" begin diff --git a/Isabelle_DOF-Ontologies/document_setup.thy b/Isabelle_DOF-Ontologies/document_setup.thy index 2d2191d..701ea9b 100644 --- a/Isabelle_DOF-Ontologies/document_setup.thy +++ b/Isabelle_DOF-Ontologies/document_setup.thy @@ -1,12 +1,12 @@ (*<*) theory "document_setup" imports - "Isabelle_DOF.technical_report" + "Isabelle_DOF.technical_report" + "Isabelle_DOF-Ontologies.CENELEC_50128" begin use_template "scrreprt-modern" -(* use_ontology "technical_report" *) -use_ontology_unchecked "Isabelle_DOF.technical_report" and "Isabelle_DOF-Ontologies.CENELEC_50128" +use_ontology "Isabelle_DOF.technical_report" and "Isabelle_DOF-Ontologies.CENELEC_50128" (*>*) diff --git a/Isabelle_DOF-Ontologies/small_math/small_math.thy b/Isabelle_DOF-Ontologies/small_math/small_math.thy index 334aa4c..0a68c7d 100644 --- a/Isabelle_DOF-Ontologies/small_math/small_math.thy +++ b/Isabelle_DOF-Ontologies/small_math/small_math.thy @@ -15,7 +15,6 @@ chapter\An example ontology for a math paper\ theory small_math imports -"document_setup" "Isabelle_DOF.Isa_COL" begin diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 097e3fb..13f570a 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -43,7 +43,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) and "text*" "text-macro*" :: document_body and "term*" "value*" "assert*" :: document_body - and "use_template" "use_ontology" "use_ontology_unchecked" :: thy_decl + and "use_template" "use_ontology" :: thy_decl and "define_template" "define_ontology" :: thy_load and "print_doc_classes" "print_doc_items" "print_doc_class_template" "check_doc_global" :: diag @@ -3038,7 +3038,7 @@ sig val define_template: binding * string -> theory -> string * theory val define_ontology: binding * string -> theory -> string * theory val use_template: Context.generic -> xstring * Position.T -> unit - val use_ontology: bool -> Context.generic -> (xstring * Position.T) list -> unit + val use_ontology: Context.generic -> (xstring * Position.T) list -> unit end; structure Document_Context: DOCUMENT_CONTEXT = @@ -3106,10 +3106,10 @@ fun use_template context arg = let val xml = arg |> check_template context |> snd |> XML.string in Export.export (Context.theory_of context) \<^path_binding>\dof/use_template\ xml end; -fun use_ontology check context args = +fun use_ontology context args = let val xml = args - |> map (if check then check_ontology context #> fst else fst) + |> map (check_ontology context #> fst) |> cat_lines |> XML.string; in Export.export (Context.theory_of context) \<^path_binding>\dof/use_ontology\ xml end; @@ -3131,13 +3131,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\use_ontology\ "use DOF document ontologies (as defined within theory context)" (Parse.and_list1 (Parse.position Parse.name) >> (fn args => - Toplevel.theory (fn thy => (use_ontology true (Context.Theory thy) args; thy)))); - -val _ = - Outer_Syntax.command \<^command_keyword>\use_ontology_unchecked\ - "use DOF document ontologies (as defined within theory context). Unchecked version for internal use. All Isabelle/DOF documents shoul duse\"use_ontolog\"" - (Parse.and_list1 (Parse.position Parse.name) >> (fn args => - Toplevel.theory (fn thy => (use_ontology false (Context.Theory thy) args; thy)))); + Toplevel.theory (fn thy => (use_ontology (Context.Theory thy) args; thy)))); val _ = Outer_Syntax.command \<^command_keyword>\define_template\