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

Merge branch 'main' into Isabelle_dev

This commit is contained in:
Achim D. Brucker 2023-02-22 22:58:47 +00:00
parent 873f5c79ab 85f115196b
commit 829915ae2c
6 changed files with 9 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy
View File

@ -17,7 +17,6 @@ section\<open>Terminology\<close>
theory CC_terminology
imports
"document_setup"
"Isabelle_DOF.technical_report"
begin

2
Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy
View File

@ -27,7 +27,7 @@ identifies:
theory
CENELEC_50128
imports
"document_setup"
"Isabelle_DOF.technical_report"
begin
define_ontology "DOF-CENELEC_50128.sty"

1
Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy
View File

@ -16,7 +16,6 @@ chapter\<open>A conceptual introduction into DOF and its features:\<close>
theory
Conceptual
imports
"document_setup"
"Isabelle_DOF.Isa_DOF"
"Isabelle_DOF.Isa_COL"
begin

6
Isabelle_DOF-Ontologies/document_setup.thy
View File

@ -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"
(*>*)

1
Isabelle_DOF-Ontologies/small_math/small_math.thy
View File

@ -15,7 +15,6 @@ chapter\<open>An example ontology for a math paper\<close>
theory small_math
imports
"document_setup"
"Isabelle_DOF.Isa_COL"
begin

16
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -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
@ -3035,7 +3035,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 =
@ -3103,10 +3103,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>\<open>dof/use_template\<close> 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>\<open>dof/use_ontology\<close> xml end;
@ -3128,13 +3128,7 @@ val _ =
Outer_Syntax.command \<^command_keyword>\<open>use_ontology\<close>
"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>\<open>use_ontology_unchecked\<close>
"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>\<open>define_template\<close>