--- a/NEWS Wed Apr 08 14:48:55 2020 +0200
+++ b/NEWS Wed Apr 08 14:52:54 2020 +0200
@@ -12,8 +12,15 @@
* The command-line tool "isabelle console" now supports interrupts
properly (on Linux and macOS).
-* The Isabelle/Scala "Progress" interface has changed slightly and
-"No_Progress" discontinued. INCOMPATIBILITY, use "new Progress" instead.
+* The Isabelle/Scala "Progress" interface changed slightly and
+"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
+instead.
+
+* General support for Isabelle/Scala system services, configured via the
+shell function "isabelle_scala_service" in etc/settings (e.g. of an
+Isabelle component). For example, see isabelle.Bibtex.File_Format. This
+supersedes former "isabelle_scala_tools" and "isabelle_file_format":
+minor INCOMPATIBILITY.
--- a/etc/settings Wed Apr 08 14:48:55 2020 +0200
+++ b/etc/settings Wed Apr 08 14:52:54 2020 +0200
@@ -20,10 +20,10 @@
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
-isabelle_scala_tools 'isabelle.Tools'
-[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools 'isabelle.Admin_Tools'
+isabelle_scala_service 'isabelle.Tools'
+[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
-isabelle_file_format 'isabelle.Bibtex$File_Format'
+isabelle_scala_service 'isabelle.Bibtex$File_Format'
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
--- a/lib/scripts/getfunctions Wed Apr 08 14:48:55 2020 +0200
+++ b/lib/scripts/getfunctions Wed Apr 08 14:52:54 2020 +0200
@@ -113,22 +113,6 @@
}
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
-
#Isabelle fonts
function isabelle_fonts ()
{
@@ -160,21 +144,21 @@
}
export -f isabelle_fonts_hidden
-#file formats
-function isabelle_file_format ()
+#Isabelle/Scala services
+function isabelle_scala_service ()
{
local X=""
for X in "$@"
do
- if [ -z "$ISABELLE_FILE_FORMATS" ]; then
- ISABELLE_FILE_FORMATS="$X"
+ if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
+ ISABELLE_SCALA_SERVICES="$X"
else
- ISABELLE_FILE_FORMATS="$ISABELLE_FILE_FORMATS:$X"
+ ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X"
fi
done
- export ISABELLE_FILE_FORMATS
+ export ISABELLE_SCALA_SERVICES
}
-export -f isabelle_file_format
+export -f isabelle_scala_service
#administrative build
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
--- a/src/Pure/PIDE/protocol_handlers.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala Wed Apr 08 14:52:54 2020 +0200
@@ -51,7 +51,10 @@
def init(name: String): State =
{
val new_handler =
- try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
+ try {
+ Some(Class.forName(name).getDeclaredConstructor().newInstance()
+ .asInstanceOf[Session.Protocol_Handler])
+ }
catch { case exn: Throwable => bad_handler(exn, name); None }
new_handler match { case Some(handler) => init(handler) case None => this }
}
--- a/src/Pure/PIDE/resources.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/PIDE/resources.scala Wed Apr 08 14:52:54 2020 +0200
@@ -23,19 +23,17 @@
/* file formats */
- val file_formats: File_Format.Environment = File_Format.environment()
-
def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
- file_formats.get(name).flatMap(_.make_theory_name(resources, name))
+ File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name))
def make_theory_content(thy_name: Document.Node.Name): Option[String] =
- file_formats.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
+ File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
- file_formats.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
+ File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
def is_hidden(name: Document.Node.Name): Boolean =
- !name.is_theory || name.theory == Sessions.root_name || file_formats.is_theory(name)
+ !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
def thy_path(path: Path): Path = path.ext("thy")
--- a/src/Pure/PIDE/session.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/PIDE/session.scala Wed Apr 08 14:52:54 2020 +0200
@@ -354,7 +354,7 @@
/* file formats */
lazy val file_formats: File_Format.Session =
- resources.file_formats.start_session(session)
+ File_Format.registry.start_session(session)
/* protocol handlers */
--- a/src/Pure/System/isabelle_system.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Apr 08 14:52:54 2020 +0200
@@ -54,7 +54,7 @@
_settings.get
}
- def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
+ private def init_settings(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
if (_settings.isEmpty) {
val isabelle_root1 =
bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
@@ -127,6 +127,12 @@
}
}
+ def init()
+ {
+ init_settings()
+ services
+ }
+
/* getenv */
@@ -374,7 +380,9 @@
def err(msg: String): Nothing =
error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
- try { Class.forName(name).asInstanceOf[Class[A]].newInstance() }
+ try {
+ Class.forName(name).asInstanceOf[Class[A]].getDeclaredConstructor().newInstance()
+ }
catch {
case _: ClassNotFoundException => err("Class not found")
case exn: Throwable => err(Exn.message(exn))
@@ -383,6 +391,13 @@
}
+ /* user-defined services */
+
+ abstract class Service
+
+ lazy val services: List[Service] = init_classes[Service]("ISABELLE_SCALA_SERVICES")
+
+
/* default logic */
def default_logic(args: String*): String =
--- a/src/Pure/System/isabelle_tool.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/System/isabelle_tool.scala Wed Apr 08 14:52:54 2020 +0200
@@ -98,7 +98,7 @@
/* internal tools */
private lazy val internal_tools: List[Isabelle_Tool] =
- Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS")
+ Isabelle_System.services.collect { case c: Isabelle_Scala_Tools => c }
.flatMap(_.tools.toList)
private def list_internal(): List[(String, String)] =
@@ -140,7 +140,7 @@
sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
-class Isabelle_Scala_Tools(val tools: Isabelle_Tool*)
+class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
class Tools extends Isabelle_Scala_Tools(
Build.isabelle_tool,
--- a/src/Pure/Thy/file_format.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/Thy/file_format.scala Wed Apr 08 14:52:54 2020 +0200
@@ -12,12 +12,12 @@
sealed case class Theory_Context(name: Document.Node.Name, content: String)
- /* environment */
+ /* registry */
- def environment(): Environment =
- new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS"))
+ lazy val registry: Registry =
+ new Registry(Isabelle_System.services.collect { case c: File_Format => c })
- final class Environment private [File_Format](file_formats: List[File_Format])
+ final class Registry private [File_Format](file_formats: List[File_Format])
{
override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
@@ -53,7 +53,7 @@
object No_Agent extends Agent
}
-trait File_Format
+trait File_Format extends Isabelle_System.Service
{
def format_name: String
override def toString: String = format_name
--- a/src/Pure/Tools/spell_checker.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Pure/Tools/spell_checker.scala Wed Apr 08 14:52:54 2020 +0200
@@ -141,9 +141,9 @@
permanent_updates
val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
- val factory_cons = factory_class.getConstructor()
- factory_cons.setAccessible(true)
- val factory = factory_cons.newInstance()
+ val factory_constructor = factory_class.getConstructor()
+ factory_constructor.setAccessible(true)
+ val factory = factory_constructor.newInstance()
val add = Untyped.method(factory_class, "add", classOf[String])
--- a/src/Tools/VSCode/src/document_model.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Tools/VSCode/src/document_model.scala Wed Apr 08 14:52:54 2020 +0200
@@ -60,7 +60,7 @@
def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
Document_Model(session, editor, node_name, Content.empty,
- node_required = session.resources.file_formats.is_theory(node_name))
+ node_required = File_Format.registry.is_theory(node_name))
}
sealed case class Document_Model(
--- a/src/Tools/jEdit/src/document_model.scala Wed Apr 08 14:48:55 2020 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Apr 08 14:52:54 2020 +0200
@@ -389,7 +389,7 @@
file.foreach(PIDE.plugin.file_watcher.register_parent(_))
val content = Document_Model.File_Content(text)
- val node_required1 = node_required || session.resources.file_formats.is_theory(node_name)
+ val node_required1 = node_required || File_Format.registry.is_theory(node_name)
File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
}
}
@@ -454,7 +454,7 @@
def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
if (pending_edits.nonEmpty ||
- !session.resources.file_formats.is_theory(node_name) &&
+ !File_Format.registry.is_theory(node_name) &&
(node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
else {
val text_edits = List(Text.Edit.remove(0, content.text))