equal
deleted
inserted
replaced
1127 handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) |
1127 handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) |
1128 | Option => raise (Load_cplexResult "Option") |
1128 | Option => raise (Load_cplexResult "Option") |
1129 |
1129 |
1130 exception Execute of string; |
1130 exception Execute of string; |
1131 |
1131 |
1132 fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s]))); |
1132 fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s))); |
1133 fun wrap s = "\""^s^"\""; |
1133 fun wrap s = "\""^s^"\""; |
1134 |
1134 |
1135 fun solve_glpk prog = |
1135 fun solve_glpk prog = |
1136 let |
1136 let |
1137 val name = string_of_int (Time.toMicroseconds (Time.now ())) |
1137 val name = string_of_int (Time.toMicroseconds (Time.now ())) |