equal
deleted
inserted
replaced
72 def err(msg: String): Nothing = |
72 def err(msg: String): Nothing = |
73 error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg) |
73 error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg) |
74 try { Class.forName(name, true, class_loader).asInstanceOf[Classpath.Service_Class] } |
74 try { Class.forName(name, true, class_loader).asInstanceOf[Classpath.Service_Class] } |
75 catch { |
75 catch { |
76 case _: ClassNotFoundException => err("Class not found") |
76 case _: ClassNotFoundException => err("Class not found") |
77 case exn: Throwable => err(Exn.message(exn)) |
77 case exn: Throwable => err(Exn.print(exn)) |
78 } |
78 } |
79 } |
79 } |
80 } |
80 } |
81 |
81 |
82 val services: List[Classpath.Service_Class] = |
82 val services: List[Classpath.Service_Class] = |