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

Implemented support for using full-qualfied names for ontologies, allowing for user-defined ontology styles in custom sessions.

This commit is contained in:
Achim D. Brucker 2023-02-21 21:32:23 +00:00
parent f8399e0fb2
commit cf386892fc
3 changed files with 7 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/mini_odo.thy
View File

@ -20,7 +20,7 @@ imports
"Physical_Quantities.SI" "Physical_Quantities.SI_Pretty"
begin
use_template "scrreprt-modern"
use_ontology technical_report and CENELEC_50128
use_ontology technical_report and "Isabelle_DOF-Ontologies.CENELEC_50128"
declare[[strict_monitor_checking=true]]
define_shortcut* dof \<rightleftharpoons> \<open>\dof\<close>
isadof \<rightleftharpoons> \<open>\isadof{}\<close>

6
Isabelle_DOF/scala/dof_document_build.scala
View File

@ -68,11 +68,11 @@ object DOF_Document_Build
val isabelle_dof_dir = context.session_context.sessions_structure(DOF.session).dir
val ltx_ontologies = split_lines(the_document_entry(context, "dof/use_ontology").text)
val ltx_ontologies = split_lines(the_document_entry(context, "dof/use_ontology").text)
// LaTeX styles from Isabelle/DOF directory
(List(Path.explode("latex/styles"), Path.explode("ontologies")):::(ltx_ontologies.map(name =>
context.session_context.sessions_structure((Long_Name.qualifier(name)).mkString).dir)))
(List(Path.explode("latex/styles"), Path.explode("ontologies")) :::(ltx_ontologies.map(name =>
context.session_context.sessions_structure((Long_Name.base_name(Long_Name.qualifier(name))).mkString).dir)))
.flatMap(dir => File.find_files((isabelle_dof_dir + dir).file, _.getName.endsWith(".sty")))
.foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file))

6
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -3109,8 +3109,8 @@ fun use_template context arg =
fun use_ontology context args =
let
val xml = args
(* |> map (check_ontology context #> fst #> Long_Name.base_name) *)
|> map (check_ontology context #> fst )
(* |> map (check_ontology context #> fst #> Long_Name.base_name) *)
|> 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;
@ -3152,7 +3152,7 @@ val _ =
(fn (get_file, pos) => Toplevel.theory (fn thy =>
let
val (file, thy') = get_file thy;
val binding = Binding.make (strip_ontology (#src_path file, pos), pos);
val binding = Binding.qualify false (Long_Name.qualifier (Context.theory_long_name thy')) (Binding.make (strip_ontology (#src_path file, pos), pos));
val text = cat_lines (#lines file);
in #2 (define_ontology (binding, text) thy') end)));