src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42039 cef738d55348
parent 42028 bd6515e113b2
child 42090 ef566ce50170
equal deleted inserted replaced
42038:626fcf4a803e 42039:cef738d55348
   142           (unprefix "module Code where {" code)
   142           (unprefix "module Code where {" code)
   143         val _ = File.write code_file code'
   143         val _ = File.write code_file code'
   144         val _ = File.write narrowing_engine_file narrowing_engine
   144         val _ = File.write narrowing_engine_file narrowing_engine
   145         val _ = File.write main_file main
   145         val _ = File.write main_file main
   146         val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
   146         val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
   147         val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
   147         val cmd = "( exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
   148           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
   148           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
   149           " -o " ^ executable ^ " && " ^ executable
   149           " -o " ^ executable ^ "; ) && " ^ executable
   150           (* FIXME: should use bash command exec but does not work with && *) 
       
   151       in
   150       in
   152         bash_output cmd
   151         bash_output cmd
   153       end
   152       end
   154     val result = Isabelle_System.with_tmp_dir tmp_prefix run
   153     val result = Isabelle_System.with_tmp_dir tmp_prefix run
   155     val output_value = the_default "NONE"
   154     val output_value = the_default "NONE"