Isabelle/Scala build.props with some pro-forma services

(unusual package name prevents problems with Maven/IntelliJ).

etc/build.props

@@ -0,0 +1,12 @@
+title = Isabelle/DOF
+module = $ISABELLE_HOME_USER/DOF/isabelle_dof.jar
+no_build = false
+requirements = \
+  env:ISABELLE_SCALA_JAR
+sources = \
+  src/scala/dof_document_build.scala \
+  src/scala/dof_mkroot.scala \
+  src/scala/dof_tools.scala
+services = \
+  isabelle_dof.DOF_Tools \
+  isabelle_dof.DOF_Document_Build$Engine

examples/CENELEC_50128/mini_odo/ROOT

@@ -1,5 +1,5 @@
 session "mini_odo" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = "build"]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     "mini_odo"
   document_files

examples/math_exam/MathExam/ROOT

@@ -1,5 +1,5 @@
 session "MathExam" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = "build"]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     MathExam
   document_files

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT

@@ -1,5 +1,5 @@
 session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" + 
-  options  [document = pdf, document_output = "output", document_build = "build",
+  options  [document = pdf, document_output = "output", document_build = dof,
     quick_and_dirty = true]
   theories
     IsaDofApplications

examples/scholarly_paper/2020-iFM-CSP/ROOT

@@ -1,5 +1,5 @@
 session "2020-iFM-csp" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = "build"]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     "paper"
   document_files

examples/scholarly_paper/2021-ITP-PMTI/ROOT

@@ -1,5 +1,5 @@
 session "2021-ITP-PMTI" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = "build"]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     "paper"
   document_files

examples/technical_report/Isabelle_DOF-Manual/ROOT

@@ -1,5 +1,5 @@
 session "Isabelle_DOF-Manual" = "Isabelle_DOF" + 
-  options  [document = pdf, document_output = "output", document_build = "build",
+  options  [document = pdf, document_output = "output", document_build = dof,
     quick_and_dirty = true]
   theories
     "Isabelle_DOF-Manual"

examples/technical_report/TR_my_commented_isabelle/ROOT

@@ -1,5 +1,5 @@
 session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = "build",
+  options [document = pdf, document_output = "output", document_build = dof,
     quick_and_dirty = true]
   theories
     "TR_MyCommentedIsabelle"

src/ROOT

@@ -1,5 +1,5 @@
 session "Isabelle_DOF" = "Functional-Automata" + 
-  options [document = pdf, document_output = "output", document_build = "build"]
+  options [document = pdf, document_output = "output", document_build = dof]
   sessions
     "Regular-Sets"
   directories 

src/scala/dof_document_build.scala

@@ -0,0 +1,17 @@
+/*  Author:     Makarius
+
+Build theory document (PDF) from session database.
+*/
+
+package isabelle_dof
+
+import isabelle._
+
+
+object DOF_Document_Build
+{
+  class Engine extends Document_Build.Bash_Engine("dof")
+  {
+    override def use_build_script: Boolean = true
+  }
+}

src/scala/dof_mkroot.scala

@@ -0,0 +1,69 @@
+/*  Author:     Makarius
+
+Prepare session root directory for Isabelle/DOF.
+*/
+
+package isabelle_dof
+
+import isabelle._
+
+
+object DOF_Mkroot
+{
+  /** mkroot **/
+
+  def mkroot(
+    session_name: String = "",
+    session_dir: Path = Path.current,
+    session_parent: String = "",
+    init_repos: Boolean = false,
+    title: String = "",
+    author: String = "",
+    progress: Progress = new Progress): Unit =
+  {
+    Mkroot.mkroot(session_name = session_name, session_dir = session_dir,
+      session_parent = session_parent, init_repos = init_repos,
+      title = title, author = author, progress = progress)
+  }
+
+
+
+  /** Isabelle tool wrapper **/
+
+  val isabelle_tool = Isabelle_Tool("dof_mkroot", "prepare session root directory for Isabelle/DOF",
+    Scala_Project.here, args =>
+  {
+    var author = ""
+    var init_repos = false
+    var title = ""
+    var session_name = ""
+
+    val getopts = Getopts("""
+Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
+
+  Options are:
+    -A LATEX     provide author in LaTeX notation (default: user name)
+    -I           init Mercurial repository and add generated files
+    -T LATEX     provide title in LaTeX notation (default: session name)
+    -n NAME      alternative session name (default: directory base name)
+
+  Prepare session root directory (default: current directory).
+""",
+      "A:" -> (arg => author = arg),
+      "I" -> (arg => init_repos = true),
+      "T:" -> (arg => title = arg),
+      "n:" -> (arg => session_name = 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()
+      }
+
+    mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
+      author = author, title = title, progress = new Console_Progress)
+  })
+}

src/scala/dof_tools.scala

@@ -0,0 +1,13 @@
+/*  Author:     Makarius
+
+Isabelle/DOF command-line tools.
+*/
+
+package isabelle_dof
+
+import isabelle._
+
+
+class DOF_Tools extends Isabelle_Scala_Tools(
+  DOF_Mkroot.isabelle_tool
+)