Clarified export name for the sake of low-level errors
This commit is contained in:
parent
d20e9ccd22
commit
a4e75c8b12
|
@ -2960,14 +2960,14 @@ val define_ontology = define (snd, apsnd);
|
|||
|
||||
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/root.tex\<close> xml end;
|
||||
in Export.export (Context.theory_of context) \<^path_binding>\<open>dof/use_template\<close> xml end;
|
||||
|
||||
fun use_ontology context args =
|
||||
let
|
||||
val xml = args
|
||||
|> map (check_ontology context)
|
||||
|> let open XML.Encode in list (pair string string) end;
|
||||
in Export.export (Context.theory_of context) \<^path_binding>\<open>dof/ontologies\<close> xml end;
|
||||
in Export.export (Context.theory_of context) \<^path_binding>\<open>dof/use_ontology\<close> xml end;
|
||||
|
||||
val strip_template = strip "root-" ".tex";
|
||||
val strip_ontology = strip "DOF-" ".sty";
|
||||
|
|
|
@ -74,7 +74,7 @@ object DOF_Document_Build
|
|||
|
||||
// root.tex from exports
|
||||
File.write(directory.doc_dir + Path.explode("root.tex"),
|
||||
the_document_entry(context, "dof/root.tex", "use_template").text)
|
||||
the_document_entry(context, "dof/use_template", "use_template").text)
|
||||
|
||||
// copy Isabelle/DOF LaTeX styles
|
||||
List(Path.explode("DOF/latex"), Path.explode("ontologies"))
|
||||
|
@ -83,7 +83,7 @@ object DOF_Document_Build
|
|||
|
||||
// ontologies.tex from exports
|
||||
val ontologies = {
|
||||
val xml = the_document_entry(context, "dof/ontologies", "use_ontology").uncompressed_yxml
|
||||
val xml = the_document_entry(context, "dof/use_ontology", "use_ontology").uncompressed_yxml
|
||||
import XML.Decode._
|
||||
list(pair(string, string))(xml)
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue