# HG changeset patch
# User wenzelm
# Date 1614891713 -3600
# Node ID ffdb22a155b4b60adc7d42b5cfbf6a488ea618fc
# Parent  894f29abe5fc7dfdf6722a7a8ce3e1d2e60d00f1
tuned --- avoid compiler warnings;

diff -r 894f29abe5fc -r ffdb22a155b4 src/Pure/System/isabelle_tool.scala
--- 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")
       }