Commit 1940906d authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp/gui] fix proof script feedback

parent ee021c67
......@@ -369,16 +369,18 @@ let pending = function
| Tactic(n,_,_) -> n
| Error _ -> 1
let rec status = function
let rec pending_any = function
| [] -> 1
| [a] -> pending a
| a::s ->
let n = pending a in
if n = 0 then 0 else min n (status s)
if n = 0 then 0 else min n (pending_any s)
let rec subgoals n = function
| [] -> n
| (_,a)::s -> subgoals (n + status a) s
| (_,js)::s -> subgoals (n + pending_any js) s
let has_proof = List.exists is_tactic
let a_prover p r = Prover(p,r)
let a_tactic tac children = Tactic(subgoals 0 children,tac,children)
......
......@@ -43,7 +43,8 @@ val a_prover : VCS.prover -> VCS.result -> alternative
val a_tactic : jtactic -> (string * jscript) list -> alternative
val pending : alternative -> int (** pending goals *)
val status : jscript -> int (** minimum of pending goals *)
val pending_any : jscript -> int (** minimum of pending goals *)
val has_proof : jscript -> bool (** Has a tactical alternative *)
val decode : Json.t -> jscript
val encode : jscript -> Json.t
......
......@@ -463,6 +463,7 @@ let search
(* -------------------------------------------------------------------------- *)
let proofs = Hashtbl.create 32
let has_proof wpo =
let wid = wpo.Wpo.po_gid in
try Hashtbl.find proofs wid
......@@ -471,7 +472,7 @@ let has_proof wpo =
let ok =
try
let script = ProofScript.decode (ProofSession.load wpo) in
ProofScript.status script = 0
ProofScript.has_proof script
with _ -> false in
(Hashtbl.add proofs wid ok ; ok)
else false
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment