Merge branch 'main' into Isabelle_dev
ci/woodpecker/push/build Pipeline failed
Details
ci/woodpecker/push/build Pipeline failed
Details
This commit is contained in:
commit
8b9c65f6ef
|
@ -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>
|
||||
|
|
|
@ -18,6 +18,7 @@ theory
|
|||
CENELEC_50128
|
||||
|
||||
begin
|
||||
|
||||
define_shortcut* dof \<rightleftharpoons> \<open>\dof\<close>
|
||||
isadof \<rightleftharpoons> \<open>\isadof{}\<close>
|
||||
define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
|
||||
|
|
|
@ -5,7 +5,9 @@ theory "document_setup"
|
|||
begin
|
||||
|
||||
use_template "scrreprt-modern"
|
||||
use_ontology "technical_report"
|
||||
(* use_ontology "technical_report" *)
|
||||
use_ontology_unchecked "Isabelle_DOF.technical_report" and "Isabelle_DOF-Ontologies.CENELEC_50128"
|
||||
|
||||
(*>*)
|
||||
|
||||
title*[title::title] \<open>Isabelle/DOF\<close>
|
||||
|
|
|
@ -69,11 +69,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))
|
||||
|
||||
|
|
|
@ -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" :: thy_decl
|
||||
and "use_template" "use_ontology" "use_ontology_unchecked" :: 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: Context.generic -> (xstring * Position.T) list -> unit
|
||||
val use_ontology: bool -> Context.generic -> (xstring * Position.T) list -> unit
|
||||
end;
|
||||
|
||||
structure Document_Context: DOCUMENT_CONTEXT =
|
||||
|
@ -3103,11 +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 context args =
|
||||
fun use_ontology check context args =
|
||||
let
|
||||
val xml = args
|
||||
(* |> map (check_ontology context #> fst #> Long_Name.base_name) *)
|
||||
|> map (check_ontology context #> fst )
|
||||
|> map (if check then check_ontology context #> fst else fst)
|
||||
|> cat_lines |> XML.string;
|
||||
in Export.export (Context.theory_of context) \<^path_binding>\<open>dof/use_ontology\<close> xml end;
|
||||
|
||||
|
@ -3129,7 +3128,13 @@ 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 (Context.Theory thy) args; thy))));
|
||||
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))));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>define_template\<close>
|
||||
|
@ -3149,7 +3154,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)));
|
||||
|
||||
|
|
Loading…
Reference in New Issue