src/Pure/goal.ML
changeset 50974 55f8bd61b029
parent 50914 fe4714886d92
child 50987 616789281413
equal deleted inserted replaced
50967:00d87ade2294 50974:55f8bd61b029
   114 
   114 
   115 fun count_forked i =
   115 fun count_forked i =
   116   Synchronized.change forked_proofs (fn (m, groups, tab) =>
   116   Synchronized.change forked_proofs (fn (m, groups, tab) =>
   117     let
   117     let
   118       val n = m + i;
   118       val n = m + i;
   119       val _ =
   119       val _ = Future.forked_proofs := n;
   120         Multithreading.tracing 2 (fn () =>
       
   121           ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
       
   122     in (n, groups, tab) end);
   120     in (n, groups, tab) end);
   123 
   121 
   124 fun register_forked id future =
   122 fun register_forked id future =
   125   Synchronized.change forked_proofs (fn (m, groups, tab) =>
   123   Synchronized.change forked_proofs (fn (m, groups, tab) =>
   126     let
   124     let
   174 fun peek_futures id =
   172 fun peek_futures id =
   175   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
   173   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
   176 
   174 
   177 fun reset_futures () =
   175 fun reset_futures () =
   178   Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
   176   Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
   179     (groups, (0, [], Inttab.empty)));
   177     (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
   180 
   178 
   181 end;
   179 end;
   182 
   180 
   183 
   181 
   184 (* scheduling parameters *)
   182 (* scheduling parameters *)