--- 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 =