support for user-defined Isabelle/Scala command-line tools;
misc tuning and clarification;
--- a/NEWS Sat Nov 10 07:57:20 2018 +0000
+++ b/NEWS Sat Nov 10 14:08:02 2018 +0100
@@ -26,9 +26,9 @@
OpenJDK 11.
* Support for user-defined file-formats via class isabelle.File_Format
-in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format). It is
-configured via the shell function "isabelle_file_format" in
-etc/settings, e.g. of an Isabelle component.
+in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
+the shell function "isabelle_file_format" in etc/settings (e.g. of an
+Isabelle component).
*** Isar ***
@@ -117,6 +117,11 @@
*** System ***
+* Support for Isabelle command-line tools defined in Isabelle/Scala.
+Instances of class Isabelle_Scala_Tools may be configured via the shell
+function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
+component).
+
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
source modules for Isabelle tools implemented in Haskell, notably for
Isabelle/PIDE.
--- a/etc/settings Sat Nov 10 07:57:20 2018 +0000
+++ b/etc/settings Sat Nov 10 14:08:02 2018 +0100
@@ -20,6 +20,9 @@
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
+isabelle_scala_tools 'isabelle.Regular_Tools'
+[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools 'isabelle.Admin_Tools'
+
isabelle_file_format 'isabelle.Bibtex$File_Format'
#paranoia settings -- avoid intrusion of alien options
--- a/lib/scripts/getfunctions Sat Nov 10 07:57:20 2018 +0000
+++ b/lib/scripts/getfunctions Sat Nov 10 14:08:02 2018 +0100
@@ -109,19 +109,35 @@
}
export -f classpath
+#Isabelle/Scala tools
+function isabelle_scala_tools ()
+{
+ local X=""
+ for X in "$@"
+ do
+ if [ -z "$ISABELLE_SCALA_TOOLS" ]; then
+ ISABELLE_SCALA_TOOLS="$X"
+ else
+ ISABELLE_SCALA_TOOLS="$ISABELLE_SCALA_TOOLS:$X"
+ fi
+ done
+ export ISABELLE_SCALA_TOOLS
+}
+export -f isabelle_scala_tools
+
#file formats
function isabelle_file_format ()
{
local X=""
for X in "$@"
do
- if [ -z "$ISABELLE_CLASSES_FILE_FORMAT" ]; then
- ISABELLE_CLASSES_FILE_FORMAT="$X"
+ if [ -z "$ISABELLE_FILE_FORMATS" ]; then
+ ISABELLE_FILE_FORMATS="$X"
else
- ISABELLE_CLASSES_FILE_FORMAT="$ISABELLE_CLASSES_FILE_FORMAT:$X"
+ ISABELLE_FILE_FORMATS="$ISABELLE_FILE_FORMATS:$X"
fi
done
- export ISABELLE_CLASSES_FILE_FORMAT
+ export ISABELLE_FILE_FORMATS
}
export -f isabelle_file_format
--- a/src/Pure/Admin/build_cygwin.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_cygwin.scala Sat Nov 10 14:08:02 2018 +0100
@@ -87,5 +87,5 @@
if (more_args.nonEmpty) getopts.usage()
build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages)
- }, admin = true)
+ })
}
--- a/src/Pure/Admin/build_doc.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_doc.scala Sat Nov 10 14:08:02 2018 +0100
@@ -105,5 +105,5 @@
build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
}
sys.exit(rc)
- }, admin = true)
+ })
}
--- a/src/Pure/Admin/build_jdk.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_jdk.scala Sat Nov 10 14:08:02 2018 +0100
@@ -237,5 +237,5 @@
val progress = new Console_Progress()
build_jdk(archives = archives, progress = progress, target_dir = target_dir)
- }, admin = true)
+ })
}
--- a/src/Pure/Admin/build_polyml.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_polyml.scala Sat Nov 10 14:08:02 2018 +0100
@@ -272,7 +272,7 @@
build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
arch_64 = arch_64, options = options, msys_root = msys_root)
}
- }, admin = true)
+ })
val isabelle_tool2 =
Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args =>
@@ -298,5 +298,5 @@
}
build_polyml_component(component, sha1_root = sha1_root)
}
- }, admin = true)
+ })
}
--- a/src/Pure/Admin/build_status.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/build_status.scala Sat Nov 10 14:08:02 2018 +0100
@@ -591,6 +591,5 @@
build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
-
- }, admin = true)
+ })
}
--- a/src/Pure/Admin/check_sources.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/check_sources.scala Sat Nov 10 14:08:02 2018 +0100
@@ -70,5 +70,5 @@
if (specs.isEmpty) getopts.usage()
for (root <- specs) check_hg(Path.explode(root))
- }, admin = true)
+ })
}
--- a/src/Pure/Admin/remote_dmg.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Admin/remote_dmg.scala Sat Nov 10 14:08:02 2018 +0100
@@ -60,5 +60,5 @@
using(SSH.open_session(options, host = host, user = user, port = port))(
remote_dmg(_, tar_gz_file, dmg_file, volume_name))
}
- }, admin = true)
+ })
}
--- a/src/Pure/System/isabelle_system.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/System/isabelle_system.scala Sat Nov 10 14:08:02 2018 +0100
@@ -347,6 +347,24 @@
Path.split(getenv_strict("ISABELLE_COMPONENTS"))
+ /* classes */
+
+ def init_classes[A](variable: String): List[A] =
+ {
+ for (name <- space_explode(':', Isabelle_System.getenv_strict(variable)))
+ yield {
+ def err(msg: String): Nothing =
+ error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
+
+ try { Class.forName(name).asInstanceOf[Class[A]].newInstance() }
+ catch {
+ case _: ClassNotFoundException => err("Class not found")
+ case exn: Throwable => err(Exn.message(exn))
+ }
+ }
+ }
+
+
/* fonts */
def fonts(html: Boolean = false, get: String => String = getenv_strict(_)): List[Path] =
--- a/src/Pure/System/isabelle_tool.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/System/isabelle_tool.scala Sat Nov 10 14:08:02 2018 +0100
@@ -97,44 +97,17 @@
/* internal tools */
- private val internal_tools: List[Isabelle_Tool] =
- List(
- Build.isabelle_tool,
- Build_Cygwin.isabelle_tool,
- Build_Doc.isabelle_tool,
- Build_Docker.isabelle_tool,
- Build_JDK.isabelle_tool,
- Build_PolyML.isabelle_tool1,
- Build_PolyML.isabelle_tool2,
- Build_Status.isabelle_tool,
- Check_Sources.isabelle_tool,
- Doc.isabelle_tool,
- Dump.isabelle_tool,
- Export.isabelle_tool,
- Imports.isabelle_tool,
- Mkroot.isabelle_tool,
- ML_Process.isabelle_tool,
- Options.isabelle_tool,
- Present.isabelle_tool,
- Profiling_Report.isabelle_tool,
- Remote_DMG.isabelle_tool,
- Server.isabelle_tool,
- Update_Cartouches.isabelle_tool,
- Update_Comments.isabelle_tool,
- Update_Header.isabelle_tool,
- Update_Then.isabelle_tool,
- Update_Theorems.isabelle_tool,
- isabelle.vscode.Build_VSCode.isabelle_tool,
- isabelle.vscode.Grammar.isabelle_tool,
- isabelle.vscode.Server.isabelle_tool)
+ private lazy val internal_tools: List[Isabelle_Tool] =
+ Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS")
+ .flatMap(_.tools.toList)
private def list_internal(): List[(String, String)] =
- for (tool <- internal_tools.toList if tool.accessible)
+ for (tool <- internal_tools.toList)
yield (tool.name, tool.description)
private def find_internal(name: String): Option[List[String] => Unit] =
internal_tools.collectFirst({
- case tool if tool.name == name && tool.accessible =>
+ case tool if tool.name == name =>
args => Command_Line.tool0 { tool.body(args) }
})
@@ -165,8 +138,38 @@
}
}
-sealed case class Isabelle_Tool(
- name: String, description: String, body: List[String] => Unit, admin: Boolean = false)
-{
- def accessible: Boolean = !admin || Isabelle_System.admin()
-}
+sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
+
+class Isabelle_Scala_Tools(val tools: Isabelle_Tool*)
+
+class Regular_Tools extends Isabelle_Scala_Tools(
+ Build.isabelle_tool,
+ Build_Docker.isabelle_tool,
+ Doc.isabelle_tool,
+ Dump.isabelle_tool,
+ Export.isabelle_tool,
+ Imports.isabelle_tool,
+ ML_Process.isabelle_tool,
+ Mkroot.isabelle_tool,
+ Options.isabelle_tool,
+ Present.isabelle_tool,
+ Profiling_Report.isabelle_tool,
+ Server.isabelle_tool,
+ Update_Cartouches.isabelle_tool,
+ Update_Comments.isabelle_tool,
+ Update_Header.isabelle_tool,
+ Update_Then.isabelle_tool,
+ Update_Theorems.isabelle_tool,
+ isabelle.vscode.Grammar.isabelle_tool,
+ isabelle.vscode.Server.isabelle_tool)
+
+class Admin_Tools extends Isabelle_Scala_Tools(
+ Build_Cygwin.isabelle_tool,
+ Build_Doc.isabelle_tool,
+ Build_JDK.isabelle_tool,
+ Build_PolyML.isabelle_tool1,
+ Build_PolyML.isabelle_tool2,
+ Build_Status.isabelle_tool,
+ Check_Sources.isabelle_tool,
+ Remote_DMG.isabelle_tool,
+ isabelle.vscode.Build_VSCode.isabelle_tool)
--- a/src/Pure/Thy/file_format.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Pure/Thy/file_format.scala Sat Nov 10 14:08:02 2018 +0100
@@ -10,21 +10,7 @@
object File_Format
{
def environment(): Environment =
- {
- val file_formats =
- for (name <- space_explode(':', Isabelle_System.getenv_strict("ISABELLE_CLASSES_FILE_FORMAT")))
- yield {
- def err(msg: String): Nothing =
- error("Bad entry " + quote(name) + " in ISABELLE_CLASSES_FILE_FORMAT\n" + msg)
-
- try { Class.forName(name).asInstanceOf[Class[File_Format]].newInstance() }
- catch {
- case _: ClassNotFoundException => err("Class not found")
- case exn: Throwable => err(Exn.message(exn))
- }
- }
- new Environment(file_formats)
- }
+ new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS"))
final class Environment private [File_Format](file_formats: List[File_Format])
{
--- a/src/Tools/VSCode/src/build_vscode.scala Sat Nov 10 07:57:20 2018 +0000
+++ b/src/Tools/VSCode/src/build_vscode.scala Sat Nov 10 14:08:02 2018 +0100
@@ -70,5 +70,5 @@
build_grammar(options, progress)
build_extension(progress, publish = publish)
- }, admin = true)
+ })
}