Commit 3e91bbc5 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Fix calling Coq from the ide.

Edited proof are always obsolete and valid at exit of the editor so that
they can be replayed.
parent a5c1e25b
......@@ -421,8 +421,12 @@ let query_result_buffer id =
Hashtbl.remove result_buffer id; r
with Not_found -> NoUpdates
(* The editor result is returned as Valid but the editor result is also always
made obsolete. We put Valid here so that it is possible to replay the proof
to get a non obsolete valid proof.
let editor_result ret = {
pr_answer = Unknown ("", None);
pr_answer = Valid;
pr_status = ret;
pr_output = "";
pr_time = 0.0;
......@@ -432,15 +432,18 @@ let timeout_handler () =
let q = Queue.create () in
while not (Queue.is_empty prover_tasks_edited) do
(* call is an EditorCall *)
let (callback,call,ores) as c =
let (callback,call,_ores) as c =
Queue.pop prover_tasks_edited in
let prover_update = Call_provers.query_call call in
match prover_update with
| Call_provers.NoUpdates -> Queue.add c q
| Call_provers.ProverFinished _res ->
(* res is meaningless for edition, we returned the old result *)
(* inform the callback *)
callback (match ores with None -> Undone | Some r -> Done r)
| Call_provers.ProverFinished res ->
(* For editor event, the result is always obsolete and valid which
means that the proof need to be replayed to be completely checked.
Replay only replays valid goals so there would be no way to make an
interactive proof and then check it otherwise.
callback (Done res)
| _ -> assert (false) (* An edition can only return Noupdates or finished *)
Queue.transfer q prover_tasks_edited;
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