equal
deleted
inserted
replaced
101 (* future_enabled *) |
101 (* future_enabled *) |
102 |
102 |
103 val parallel_proofs = ref 1; |
103 val parallel_proofs = ref 1; |
104 |
104 |
105 fun future_enabled () = |
105 fun future_enabled () = |
106 Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1; |
106 Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1; |
107 |
107 |
108 fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2; |
108 fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2; |
109 |
109 |
110 |
110 |
111 (* future_result *) |
111 (* future_result *) |