src/Pure/proofterm.ML
changeset 44332 e10f6b873f88
parent 44331 aa9c1e9ef2ce
child 44333 cc53ce50f738
equal deleted inserted replaced
44331:aa9c1e9ef2ce 44332:e10f6b873f88
   174 fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
   174 fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
   175 
   175 
   176 fun check_body_thms (body as PBody {thms, ...}) =
   176 fun check_body_thms (body as PBody {thms, ...}) =
   177   (singleton o Future.cond_forks)
   177   (singleton o Future.cond_forks)
   178     {name = "Proofterm.check_body_thms", group = NONE,
   178     {name = "Proofterm.check_body_thms", group = NONE,
   179       deps = map (Future.task_of o #3 o #2) thms, pri = ~1, interrupts = true}
   179       deps = map (Future.task_of o #3 o #2) thms, pri = 0, interrupts = true}
   180     (fn () => (join_thms thms; body));
   180     (fn () => (join_thms thms; body));
   181 
   181 
   182 fun proof_of (PBody {proof, ...}) = proof;
   182 fun proof_of (PBody {proof, ...}) = proof;
   183 val join_proof = Future.join #> proof_of;
   183 val join_proof = Future.join #> proof_of;
   184 
   184 
  1404 
  1404 
  1405 fun fulfill_proof_future _ [] postproc body = Future.map postproc body
  1405 fun fulfill_proof_future _ [] postproc body = Future.map postproc body
  1406   | fulfill_proof_future thy promises postproc body =
  1406   | fulfill_proof_future thy promises postproc body =
  1407       (singleton o Future.forks)
  1407       (singleton o Future.forks)
  1408         {name = "Proofterm.fulfill_proof_future", group = NONE,
  1408         {name = "Proofterm.fulfill_proof_future", group = NONE,
  1409           deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = ~1,
  1409           deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
  1410           interrupts = true}
  1410           interrupts = true}
  1411         (fn () =>
  1411         (fn () =>
  1412           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
  1412           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
  1413 
  1413 
  1414 
  1414 
  1462     val body0 =
  1462     val body0 =
  1463       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
  1463       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
  1464       else
  1464       else
  1465         (singleton o Future.cond_forks)
  1465         (singleton o Future.cond_forks)
  1466           {name = "Proofterm.prepare_thm_proof", group = NONE,
  1466           {name = "Proofterm.prepare_thm_proof", group = NONE,
  1467             deps = [], pri = ~1, interrupts = true}
  1467             deps = [], pri = 0, interrupts = true}
  1468           (make_body0 o full_proof0);
  1468           (make_body0 o full_proof0);
  1469 
  1469 
  1470     fun new_prf () =
  1470     fun new_prf () =
  1471       let
  1471       let
  1472         val body' = body0
  1472         val body' = body0