968 (false, |
968 (false, |
969 read_next_problems (Substring.full (File.read path), [], []) |
969 read_next_problems (Substring.full (File.read path), [], []) |
970 |>> rev ||> rev) |
970 |>> rev ||> rev) |
971 handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], [])) |
971 handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], [])) |
972 |
972 |
|
973 |
973 (** Main Kodkod entry point **) |
974 (** Main Kodkod entry point **) |
974 |
975 |
975 val created_temp_dir = Unsynchronized.ref false |
976 fun serial_string_and_temporary_dir overlord = |
976 |
977 if overlord then ("", getenv "ISABELLE_HOME_USER") |
977 fun serial_string_and_temporary_dir_for_overlord overlord = |
978 else (serial_string (), getenv "ISABELLE_TMP") |
978 if overlord then |
|
979 ("", getenv "ISABELLE_HOME_USER") |
|
980 else |
|
981 let |
|
982 val dir = getenv "ISABELLE_TMP" |
|
983 val _ = if !created_temp_dir then () |
|
984 else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir)) |
|
985 in (serial_string (), dir) end |
|
986 |
979 |
987 (* The fudge term below is to account for Kodkodi's slow start-up time, which |
980 (* The fudge term below is to account for Kodkodi's slow start-up time, which |
988 is partly due to the JVM and partly due to the ML "bash" function. *) |
981 is partly due to the JVM and partly due to the ML "bash" function. *) |
989 val fudge_ms = 250 |
982 val fudge_ms = 250 |
990 |
983 |
1006 in |
999 in |
1007 if null indexed_problems then |
1000 if null indexed_problems then |
1008 Normal ([], triv_js, "") |
1001 Normal ([], triv_js, "") |
1009 else |
1002 else |
1010 let |
1003 let |
1011 val (serial_str, temp_dir) = |
1004 val (serial_str, temp_dir) = serial_string_and_temporary_dir overlord |
1012 serial_string_and_temporary_dir_for_overlord overlord |
|
1013 fun path_for suf = |
1005 fun path_for suf = |
1014 Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf) |
1006 Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf) |
1015 val in_path = path_for "kki" |
1007 val in_path = path_for "kki" |
1016 val in_buf = Unsynchronized.ref Buffer.empty |
1008 val in_buf = Unsynchronized.ref Buffer.empty |
1017 fun out s = Unsynchronized.change in_buf (Buffer.add s) |
1009 fun out s = Unsynchronized.change in_buf (Buffer.add s) |