equal
deleted
inserted
replaced
40 val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n" |
40 val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n" |
41 (unprefix "module Code where {" code) |
41 (unprefix "module Code where {" code) |
42 val _ = File.write code_file code' |
42 val _ = File.write code_file code' |
43 val _ = File.write narrowing_engine_file narrowing_engine |
43 val _ = File.write narrowing_engine_file narrowing_engine |
44 val _ = File.write main_file main |
44 val _ = File.write main_file main |
45 val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc")) |
45 val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc")) |
46 val cmd = "\"$EXEC_GHC\" -fglasgow-exts " ^ |
46 val cmd = "\"$EXEC_GHC\" -fglasgow-exts " ^ |
47 (space_implode " " (map Path.implode [code_file, narrowing_engine_file, main_file])) ^ |
47 (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^ |
48 " -o " ^ executable ^ " && " ^ executable |
48 " -o " ^ executable ^ " && " ^ executable |
49 in |
49 in |
50 bash_output cmd |
50 bash_output cmd |
51 end |
51 end |
52 val result = Isabelle_System.with_tmp_dir tmp_prefix run |
52 val result = Isabelle_System.with_tmp_dir tmp_prefix run |