src/Tools/Code/code_scala.ML
changeset 37822 cf3588177676
parent 37821 3cbb22cec751
child 37881 096c8397c989
     1.1 --- a/src/Tools/Code/code_scala.ML	Wed Jul 14 14:53:44 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Wed Jul 14 15:08:02 2010 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  signature CODE_SCALA =
     1.5  sig
     1.6    val target: string
     1.7 -  val check: theory -> unit
     1.8    val setup: theory -> theory
     1.9  end;
    1.10  
    1.11 @@ -414,14 +413,6 @@
    1.12  } end;
    1.13  
    1.14  
    1.15 -(** formal checking of compiled code **)
    1.16 -
    1.17 -fun check thy = Code_Target.external_check thy target
    1.18 -  "SCALA_HOME" I (fn scala_home => fn p => fn _ =>
    1.19 -    Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala");
    1.20 -
    1.21 -
    1.22 -
    1.23  (** Isar setup **)
    1.24  
    1.25  fun isar_serializer module_name =
    1.26 @@ -430,7 +421,10 @@
    1.27  
    1.28  val setup =
    1.29    Code_Target.add_target
    1.30 -    (target, { serializer = isar_serializer, literals = literals, check = () })
    1.31 +    (target, { serializer = isar_serializer, literals = literals,
    1.32 +      check = { env_var = "SCALA_HOME", make_destination = I,
    1.33 +        make_command = fn scala_home => fn p => fn _ =>
    1.34 +          Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
    1.35    #> Code_Target.add_syntax_tyco target "fun"
    1.36       (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.37          brackify_infix (1, R) fxy (