# HG changeset patch
# User Andreas Lochbihler
# Date 1500305434 -7200
# Node ID 378895354604643f2f5d430aa36934871d3026b6
# Parent  e5ba49a72ab9c8725aa42c266e9527de8e59363a
new derived targets for evaluating Haskell and Scala programs

diff -r e5ba49a72ab9 -r 378895354604 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Sun Jul 16 23:47:21 2017 +0200
+++ b/src/HOL/Library/code_test.ML	Mon Jul 17 17:30:34 2017 +0200
@@ -32,6 +32,8 @@
   val ghc_options: string Config.T
   val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string
+  val target_Scala: string
+  val target_Haskell: string
 end
 
 structure Code_Test: CODE_TEST =
@@ -576,14 +578,21 @@
       (Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
         >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of)))
 
+val target_Scala = "Scala_eval"
+val target_Haskell = "Haskell_eval"
+
+val _ = Theory.setup 
+   (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)])
+    #> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)]))
+
 val _ =
   Theory.setup (fold add_driver
     [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
      (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
      (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
      (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
-     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
-     (scalaN, (evaluate_in_scala, Code_Scala.target))]
+     (ghcN, (evaluate_in_ghc, target_Haskell)),
+     (scalaN, (evaluate_in_scala, target_Scala))]
   #> fold (fn target => Value_Command.add_evaluator (target, eval_term target))
       [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])