--- a/src/Pure/System/isabelle_tool.scala Thu Mar 04 21:19:05 2021 +0100
+++ b/src/Pure/System/isabelle_tool.scala Thu Mar 04 22:01:53 2021 +0100
@@ -29,11 +29,14 @@
val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
try {
- val symbol = tool_box.parse(source) match {
- case tree: universe.ModuleDef => tool_box.define(tree)
- case _ => err("Source does not describe a module (Scala object)")
- }
- tool_box.compile(universe.Ident(symbol))() match {
+ val tree = tool_box.parse(source)
+ val module =
+ try { tree.asInstanceOf[universe.ModuleDef] }
+ catch {
+ case _: java.lang.ClassCastException =>
+ err("Source does not describe a module (Scala object)")
+ }
+ tool_box.compile(universe.Ident(tool_box.define(module)))() match {
case body: Body => body
case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
}