equal
deleted
inserted
replaced
97 val extra_shyps: thm -> sort list |
97 val extra_shyps: thm -> sort list |
98 val proof_bodies_of: thm list -> proof_body list |
98 val proof_bodies_of: thm list -> proof_body list |
99 val proof_body_of: thm -> proof_body |
99 val proof_body_of: thm -> proof_body |
100 val proof_of: thm -> proof |
100 val proof_of: thm -> proof |
101 val join_proofs: thm list -> unit |
101 val join_proofs: thm list -> unit |
102 val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool} |
102 val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool} |
103 val future: thm future -> cterm -> thm |
103 val future: thm future -> cterm -> thm |
104 val derivation_name: thm -> string |
104 val derivation_name: thm -> string |
105 val name_derivation: string -> thm -> thm |
105 val name_derivation: string -> thm -> thm |
106 val axiom: theory -> string -> thm |
106 val axiom: theory -> string -> thm |
107 val axioms_of: theory -> (string * thm) list |
107 val axioms_of: theory -> (string * thm) list |
534 val join_proofs = ignore o proof_bodies_of; |
534 val join_proofs = ignore o proof_bodies_of; |
535 |
535 |
536 |
536 |
537 (* derivation status *) |
537 (* derivation status *) |
538 |
538 |
539 fun status_of (Thm (Deriv {promises, body}, _)) = |
539 fun peek_status (Thm (Deriv {promises, body}, _)) = |
540 let |
540 let |
541 val ps = map (Future.peek o snd) promises; |
541 val ps = map (Future.peek o snd) promises; |
542 val bodies = body :: |
542 val bodies = body :: |
543 map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps; |
543 map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps; |
544 val {oracle, unfinished, failed} = Proofterm.status_of bodies; |
544 val {oracle, unfinished, failed} = Proofterm.peek_status bodies; |
545 in |
545 in |
546 {oracle = oracle, |
546 {oracle = oracle, |
547 unfinished = unfinished orelse exists is_none ps, |
547 unfinished = unfinished orelse exists is_none ps, |
548 failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps} |
548 failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps} |
549 end; |
549 end; |