# 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; \ - 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