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

Updated scala parts to Isabelle 2023.

This commit is contained in:
Achim D. Brucker 2024-04-02 12:36:44 +01:00
parent 49faed4faf
commit f61e107515
3 changed files with 14 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Isabelle_DOF/scala/dof.scala
View File

@ -39,15 +39,16 @@ import isabelle._
object DOF {
/** parameters **/
val isabelle_version = "2022"
val isabelle_url = "https://isabelle.in.tum.de/website-Isabelle2022"
val isabelle_version = "2023"
val isabelle_url = "https://isabelle.in.tum.de/website-Isabelle2023"
val afp_version = "afp-2022-10-27"
val afp_version = "afp-2023-09-13"
// Isabelle/DOF version: "Unreleased" for development, semantic version for releases
val version = "Unreleased"
val session = "Isabelle_DOF"
val session_ontologies = "Isabelle_DOF-Ontologies"
val latest_version = "1.3.0"
val latest_isabelle = "Isabelle2021-1"
@ -55,7 +56,7 @@ object DOF {
val generic_doi = "10.5281/zenodo.3370482"
// Isabelle/DOF source repository
val url = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
val url = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/src/branch/Isabelle_dev"
// Isabelle/DOF release artifacts
val artifact_dir = "releases/Isabelle_DOF/Isabelle_DOF"

7
Isabelle_DOF/scala/dof_document_build.scala
View File

@ -42,7 +42,7 @@ object DOF_Document_Build
def the_document_entry(context: Document_Build.Context, name: String): Export.Entry = {
val entries =
for {
node_name <- context.document_theories
node_name <- context.all_document_theories
entry <- context.session_context.get(node_name.theory, name)
} yield entry
@ -60,11 +60,12 @@ object DOF_Document_Build
override def prepare_directory(
context: Document_Build.Context,
dir: Path,
doc: Document_Build.Document_Variant): Document_Build.Directory =
doc: Document_Build.Document_Variant,
verbose: Boolean): Document_Build.Directory =
{
val options = DOF.options(context.options)
val latex_output = new Latex_Output(options)
val directory = context.prepare_directory(dir, doc, latex_output)
val directory = context.prepare_directory(dir, doc, latex_output, verbose)
val isabelle_dof_dir = context.session_context.sessions_structure(DOF.session).dir

8
scala/dof_mkroot.scala
View File

@ -72,7 +72,7 @@ object DOF_Mkroot
progress.echo_if(!quiet, " creating " + root_path)
File.write(root_path,
"session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ +
"session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session_ontologies) + """ +
options [document = pdf, document_output = "output", document_build = dof]
(*theories [document = false]
A
@ -86,8 +86,10 @@ object DOF_Mkroot
val thy = session_dir + Path.explode(name + ".thy")
progress.echo_if(!quiet, " creating " + thy)
File.write(thy,
"theory\n " + name +
"\nimports\n " + ontologies.map("Isabelle_DOF." + _).mkString("\n ") + """
"theory\n \"" + name + "\"" +
"\nimports\n " +
"\"Isabelle_DOF-Ontologies.document_templates\"\n " +
ontologies.map("Isabelle_DOF." + _).mkString("\n ") + """
begin
list_templates