src/HOL/Library/code_test.ML
changeset 65901 e896db33d4ce
parent 65900 d82d1a2e8a4b
child 65904 8411f1a2272c
equal deleted inserted replaced
65900:d82d1a2e8a4b 65901:e896db33d4ce
   419       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   419       "    val _ = print \"" ^ end_markerN ^ "\";\n" ^
   420       "  in\n" ^
   420       "  in\n" ^
   421       "    0\n" ^
   421       "    0\n" ^
   422       "  end;\n" ^
   422       "  end;\n" ^
   423       "end;"
   423       "end;"
   424     val cmd =
   424     val ml_source =
   425       "echo \"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
   425       "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
   426       "use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ Path.implode driver_path ^ "\\\";" ^
   426       "use " ^ ML_Syntax.print_string (Path.implode (Path.expand code_path)) ^
   427       "Test.main ();\" | " ^ Path.implode (Path.variable ISABELLE_SMLNJ)
   427       "; use " ^ ML_Syntax.print_string (Path.implode (Path.expand driver_path)) ^
       
   428       "; Test.main ();"
       
   429     val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\""
   428   in
   430   in
   429     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   431     {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   430   end
   432   end
   431 
   433 
   432 fun evaluate_in_smlnj ctxt =
   434 fun evaluate_in_smlnj ctxt =
   459       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
   461       "  print_string \"" ^ end_markerN ^ "\";;\n" ^
   460       "main ();;"
   462       "main ();;"
   461 
   463 
   462     val compiled_path = Path.append path (Path.basic "test")
   464     val compiled_path = Path.append path (Path.basic "test")
   463     val compile_cmd =
   465     val compile_cmd =
   464       Path.implode (Path.variable ISABELLE_OCAMLC) ^ " -w pu -o " ^ Path.implode compiled_path ^
   466       "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
   465       " -I " ^ Path.implode path ^
   467       " -I " ^ File.bash_path path ^
   466       " nums.cma " ^ Path.implode code_path ^ " " ^ Path.implode driver_path
   468       " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path
   467 
   469 
   468     val run_cmd = File.bash_path compiled_path
   470     val run_cmd = File.bash_path compiled_path
   469   in
   471   in
   470     {files = [(driver_path, driver)],
   472     {files = [(driver_path, driver)],
   471      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   473      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   505       "  }\n" ^
   507       "  }\n" ^
   506       "}\n"
   508       "}\n"
   507 
   509 
   508     val compiled_path = Path.append path (Path.basic "test")
   510     val compiled_path = Path.append path (Path.basic "test")
   509     val compile_cmd =
   511     val compile_cmd =
   510       Path.implode (Path.variable ISABELLE_GHC) ^ " " ^ Code_Haskell.language_params ^ " " ^
   512       "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
   511       Config.get ctxt ghc_options ^ " -o " ^ Path.implode compiled_path ^ " " ^
   513       Config.get ctxt ghc_options ^ " -o " ^ File.bash_path compiled_path ^ " " ^
   512       Path.implode driver_path ^ " -i" ^ Path.implode path
   514       File.bash_path driver_path ^ " -i" ^ File.bash_path path
   513 
   515 
   514     val run_cmd = File.bash_path compiled_path
   516     val run_cmd = File.bash_path compiled_path
   515   in
   517   in
   516     {files = [(driver_path, driver)],
   518     {files = [(driver_path, driver)],
   517      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}
   519      compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file}