diff -r 3daaf23b9ab4 -r 6315b6426200 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jul 08 16:19:24 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Florian Haftmann, TU Muenchen
+(*  Title:      Tools/Code/code_scala.ML
+    Author:     Florian Haftmann, TU Muenchen
 
 Serializer for Scala.
 *)
 
 signature CODE_SCALA =
 sig
+  val target: string
+  val check: theory -> Path.T -> unit
   val setup: theory -> theory
 end;
 
@@ -411,6 +414,14 @@
 } end;
 
 
+(** formal checking of compiled code **)
+
+fun check thy = Code_Target.external_check thy target
+  "SCALA_HOME" I (fn scala_home => fn p => fn _ =>
+    Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala");
+
+
+
 (** Isar setup **)
 
 fun isar_seri_scala module_name =