# HG changeset patch
# User wenzelm
# Date 1600961005 -7200
# Node ID 697e5688f37073b9790dd87bbbb4821ef9d0be17
# Parent  e4a317d00489be5bab88d1d889f39e344d35d0aa
evaluate PolyML via running Isabelle/ML;

diff -r e4a317d00489 -r 697e5688f370 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Sep 24 16:43:43 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 17:23:25 2020 +0200
@@ -293,9 +293,9 @@
 
 val polymlN = "PolyML"
 
-fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir =
+fun evaluate_in_polyml ctxt (code_files, value_name) dir =
   let
-    val compiler = polymlN
+    val code = #2 (the_single code_files);
     val code_path = Path.append dir (Path.basic "generated.sml")
     val driver_path = Path.append dir (Path.basic "driver.sml")
     val out_path = Path.append dir (Path.basic "out")
@@ -316,14 +316,19 @@
     val _ = BinIO.closeOut out
   in () end;
 \<close>
-    val cmd =
-      "\"$POLYML_EXE\" --use " ^ File.bash_platform_path code_path ^
-      " --use " ^ File.bash_platform_path driver_path ^
-      " --eval " ^ Bash.string "main ()"
   in
-    List.app (File.write code_path o snd) code_files;
-    File.write driver_path driver;
-    evaluate compiler cmd;
+    if Config.get ctxt debug
+    then (File.write code_path code; File.write driver_path driver)
+    else ();
+
+    ML_Context.eval
+      {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE,
+        writeln = writeln, warning = warning}
+      Position.none
+      (ML_Lex.read_text (code, Path.position code_path) @
+       ML_Lex.read_text (driver, Path.position driver_path) @
+       ML_Lex.read "main ()");
+
     File.read out_path
   end