Re-introduced dof_mkroot for main component and moved component setup to main directory (fixes #20).

Isabelle_DOF/etc/build.props

@@ -4,7 +4,6 @@ no_build = false
 requirements = \
   env:ISABELLE_SCALA_JAR
 sources = \
-  scala/dof.scala \
-  scala/dof_document_build.scala
+  scala/dof_document_build.scala 
 services = \
   isabelle.dof.DOF_Document_Build$Engine

Isabelle_DOF/thys/Isa_DOF.thy

@@ -3163,19 +3163,17 @@ define_template "../latex/document-templates/root-scrartcl.tex"
 define_template "../latex/document-templates/root-scrreprt-modern.tex"
 define_template "../latex/document-templates/root-scrreprt.tex"
 
-
 section \<open>Isabelle/Scala module within session context\<close>
 
 external_file "../etc/build.props"
 external_file "../scala/dof_document_build.scala"
-external_file "../scala/dof.scala"
+
 
 scala_build_generated_files
   external_files
     "build.props" (in "../etc")
   and
-    "scala/dof_document_build.scala"
-    "scala/dof.scala" (in "../")
+    "scala/dof_document_build.scala" (in "../")
 
 (*
 ML\<open>

etc/build.props

@@ -0,0 +1,11 @@
+title = Isabelle/DOF
+module = $ISABELLE_HOME_USER/DOF/isabelle_dof.jar
+no_build = false
+requirements = \
+  env:ISABELLE_SCALA_JAR
+sources = \
+  scala/dof.scala \
+  scala/dof_mkroot.scala \
+  scala/dof_tools.scala
+services = \
+  isabelle.dof.DOF_Tools

scala/dof_mkroot.scala

@@ -0,0 +1,199 @@
+/*
+ * Copyright (c)
+ *               2021-2022 The University of Exeter.
+ *               2021-2022 The University of Paris-Saclay.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in
+ *    the documentation and/or other materials provided with the
+ *    distribution.
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+ * FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+ * COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+ * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+ * BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+ * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ * ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+
+/*** create session root directory for Isabelle/DOF ***/
+
+package isabelle.dof
+
+import isabelle._
+
+
+object DOF_Mkroot
+{
+  /** mkroot **/
+
+  val default_ontologies: List[String] = List("technical_report", "scholarly_paper")
+  val default_template = "scrreprt-modern"
+
+  def mkroot(
+    session_name: String = "",
+    session_dir: Path = Path.current,
+    init_repos: Boolean = false,
+    ontologies: List[String] = default_ontologies,
+    template: String = default_template,
+    quiet: Boolean = false,
+    progress: Progress = new Progress): Unit =
+  {
+    Isabelle_System.make_directory(session_dir)
+
+    val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
+
+    val root_path = session_dir + Sessions.ROOT
+    if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
+
+    val document_path = session_dir + Path.explode("document")
+    if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
+
+    progress.echo(
+      (if (quiet) "" else "\n") +
+      "Initializing session " + quote(name) + " in " + session_dir.absolute)
+
+
+    /* ROOT */
+
+    progress.echo_if(!quiet, "  creating " + root_path)
+
+    File.write(root_path,
+      "session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ +
+  options [document = pdf, document_output = "output", document_build = dof]
+(*theories [document = false]
+    A
+    B*)
+  theories
+    """ + Mkroot.root_name(name) + """
+  document_files
+    "preamble.tex"
+""")
+
+    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  ") +  """
+begin
+
+use_template """ + quote(template) + """
+use_ontology """ + ontologies.map(quote).mkString(" and ") + """
+
+end
+""")
+
+
+    /* preamble */
+
+    val preamble_tex = session_dir + Path.explode("document/preamble.tex")
+    progress.echo_if(!quiet, "  creating " + preamble_tex)
+    Isabelle_System.make_directory(preamble_tex.dir)
+    File.write(preamble_tex,"""%% This is a placeholder for user-specific configuration and packages.""")
+
+
+    /* Mercurial repository */
+
+    if (init_repos) {
+      progress.echo(
+        (if (quiet) "" else "\n") + "Initializing Mercurial repository " + session_dir.absolute)
+
+      val hg = Mercurial.init_repository(session_dir)
+
+      val hg_ignore = session_dir + Path.explode(".hgignore")
+      File.write(hg_ignore,
+"""syntax: glob
+
+*~
+*.marks
+*.orig
+*.rej
+.DS_Store
+.swp
+
+syntax: regexp
+
+^output/
+""")
+
+      hg.add(List(root_path, preamble_tex, hg_ignore))
+    }
+
+
+    /* notes */
+
+    {
+      val print_dir = session_dir.implode
+      progress.echo_if(!quiet, """
+Now use the following command line to build the session:
+
+  isabelle build -D """ +
+        (if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
+    }
+  }
+
+
+
+  /** Isabelle tool wrapper **/
+
+  val isabelle_tool = Isabelle_Tool("dof_mkroot", "create session root directory for Isabelle/DOF",
+    Scala_Project.here, args =>
+  {
+    var init_repos = false
+    var help = false
+    var session_name = ""
+    var ontologies = default_ontologies
+    var template = default_template
+    var quiet = false
+
+    val getopts = Getopts("""
+Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
+
+  Options are:
+    -I           init Mercurial repository and add generated files
+    -h           print help
+    -n NAME      alternative session name (default: directory base name)
+    -o NAMES     list of ontologies, separated by blanks
+                 (default: """ + quote(Word.implode(default_ontologies)) + """)
+    -q           quiet mode: less verbosity
+    -t NAME      template (default: """ + quote(default_template) + """)
+
+  Create session root directory for Isabelle/DOF (default: current directory).
+""",
+      "I" -> (_ => init_repos = true),
+      "h" -> (_ => help = true),
+      "n:" -> (arg => session_name = arg),
+      "o:" -> (arg => ontologies = Word.explode(arg)),
+      "q" -> (_ => quiet = true),
+      "t:" -> (arg => template = arg))
+
+    val more_args = getopts(args)
+    val session_dir =
+      more_args match {
+        case Nil => Path.current
+        case List(dir) => Path.explode(dir)
+        case _ => getopts.usage()
+      }
+
+    if (help) getopts.usage()
+
+    val progress = new Console_Progress
+
+    mkroot(session_name = session_name, session_dir = session_dir,
+      init_repos = init_repos, quiet = quiet, progress = progress,
+      ontologies = ontologies, template = template)
+  })
+}

scala/dof_tools.scala

@@ -0,0 +1,42 @@
+/*
+ * Copyright (c) 
+ *               2021-2022 The University of Exeter. 
+ *               2021-2022 The University of Paris-Saclay. 
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in
+ *    the documentation and/or other materials provided with the
+ *    distribution.
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+ * FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+ * COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+ * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+ * BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+ * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ * ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+
+/*** command-line tools for Isabelle/DOF ***/
+ 
+package isabelle.dof
+
+import isabelle._
+
+
+class DOF_Tools extends Isabelle_Scala_Tools(
+  DOF.isabelle_tool,
+  DOF_Mkroot.isabelle_tool,
+)