502 #expr_assigns p1 = #expr_assigns p2 andalso |
502 #expr_assigns p1 = #expr_assigns p2 andalso |
503 #tuple_assigns p1 = #tuple_assigns p2 andalso |
503 #tuple_assigns p1 = #tuple_assigns p2 andalso |
504 #int_bounds p1 = #int_bounds p2 andalso |
504 #int_bounds p1 = #int_bounds p2 andalso |
505 filter (is_relevant_setting o fst) (#settings p1) |
505 filter (is_relevant_setting o fst) (#settings p1) |
506 = filter (is_relevant_setting o fst) (#settings p2) |
506 = filter (is_relevant_setting o fst) (#settings p2) |
|
507 |
|
508 val created_temp_dir = Unsynchronized.ref false |
|
509 |
|
510 (* bool -> string * string *) |
|
511 fun serial_string_and_temporary_dir_for_overlord overlord = |
|
512 if overlord then |
|
513 ("", getenv "ISABELLE_HOME_USER") |
|
514 else |
|
515 let |
|
516 val dir = getenv "ISABELLE_TMP" |
|
517 val _ = if !created_temp_dir then () |
|
518 else (created_temp_dir := true; File.mkdir (Path.explode dir)) |
|
519 in (serial_string (), dir) end |
507 |
520 |
508 (* int -> string *) |
521 (* int -> string *) |
509 fun base_name j = |
522 fun base_name j = |
510 if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j |
523 if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j |
511 |
524 |
1010 in |
1023 in |
1011 if null indexed_problems then |
1024 if null indexed_problems then |
1012 Normal ([], triv_js) |
1025 Normal ([], triv_js) |
1013 else |
1026 else |
1014 let |
1027 let |
1015 val (serial_str, tmp_path) = |
1028 val (serial_str, temp_dir) = |
1016 if overlord then |
1029 serial_string_and_temporary_dir_for_overlord overlord |
1017 ("", Path.append (Path.variable "ISABELLE_HOME_USER") o Path.base) |
1030 (* string -> Path.T *) |
1018 else |
1031 fun path_for suf = |
1019 (serial_string (), File.tmp_path) |
1032 Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf) |
1020 (* string -> string -> Path.T *) |
1033 val in_path = path_for "kki" |
1021 fun path_for base suf = |
|
1022 tmp_path (Path.explode (base ^ serial_str ^ "." ^ suf)) |
|
1023 val in_path = path_for "isabelle" "kki" |
|
1024 val in_buf = Unsynchronized.ref Buffer.empty |
1034 val in_buf = Unsynchronized.ref Buffer.empty |
1025 (* string -> unit *) |
1035 (* string -> unit *) |
1026 fun out s = Unsynchronized.change in_buf (Buffer.add s) |
1036 fun out s = Unsynchronized.change in_buf (Buffer.add s) |
1027 val out_path = path_for "kodkodi" "out" |
1037 val out_path = path_for "out" |
1028 val err_path = path_for "kodkodi" "err" |
1038 val err_path = path_for "err" |
1029 val _ = write_problem_file out (map snd indexed_problems) |
1039 val _ = write_problem_file out (map snd indexed_problems) |
1030 val _ = File.write_buffer in_path (!in_buf) |
1040 val _ = File.write_buffer in_path (!in_buf) |
1031 (* unit -> unit *) |
1041 (* unit -> unit *) |
1032 fun remove_temporary_files () = |
1042 fun remove_temporary_files () = |
1033 if overlord then () |
1043 if overlord then () |
1041 Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) |
1051 Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) |
1042 - fudge_ms) |
1052 - fudge_ms) |
1043 val outcome = |
1053 val outcome = |
1044 let |
1054 let |
1045 val code = |
1055 val code = |
1046 system ("env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \ |
1056 system ("cd " ^ temp_dir ^ ";\n" ^ |
|
1057 "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \ |
1047 \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ |
1058 \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ |
1048 \$JAVA_LIBRARY_PATH\" \ |
1059 \$JAVA_LIBRARY_PATH\" \ |
1049 \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ |
1060 \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ |
1050 \$LD_LIBRARY_PATH\" \ |
1061 \$LD_LIBRARY_PATH\" \ |
1051 \\"$KODKODI\"/bin/kodkodi" ^ |
1062 \\"$KODKODI\"/bin/kodkodi" ^ |