Commit caaba2d0 authored by MARCHE Claude's avatar MARCHE Claude

improve robustness of IDE

parent c6409c9f
...@@ -621,11 +621,15 @@ let () = ...@@ -621,11 +621,15 @@ let () =
let prover_on_selected_goals pr = let prover_on_selected_goals pr =
List.iter List.iter
(fun row -> (fun row ->
try
let a = get_any_from_row_reference row in let a = get_any_from_row_reference row in
M.run_prover M.run_prover
~context_unproved_goals_only:!context_unproved_goals_only ~context_unproved_goals_only:!context_unproved_goals_only
~timelimit:gconfig.time_limit ~timelimit:gconfig.time_limit
pr a) pr a
with e ->
eprintf "@[Exception raised while running a prover:@ %a@.@]"
Exn_printer.exn_printer e)
(get_selected_row_references ()) (get_selected_row_references ())
(**********************************) (**********************************)
...@@ -1506,8 +1510,14 @@ let select_row r = ...@@ -1506,8 +1510,14 @@ let select_row r =
| M.Proof_attempt a -> | M.Proof_attempt a ->
let o = let o =
match a.M.proof_state with match a.M.proof_state with
| Session.Done r -> r.Call_provers.pr_output; | Session.Undone -> "proof not yet scheduled for running"
| _ -> "No information available" | Session.Done r -> r.Call_provers.pr_output
| Session.Scheduled-> "proof scheduled by not running yet"
| Session.Running -> "prover currently running"
| Session.InternalFailure e ->
let b = Buffer.create 37 in
bprintf b "%a" Exn_printer.exn_printer e;
Buffer.contents b
in in
task_view#source_buffer#set_text o; task_view#source_buffer#set_text o;
scroll_to_source_goal a.M.proof_goal scroll_to_source_goal a.M.proof_goal
......
...@@ -483,11 +483,18 @@ let idle_handler () = ...@@ -483,11 +483,18 @@ let idle_handler () =
if debug then if debug then
Format.eprintf "Task for prover: %a@." Format.eprintf "Task for prover: %a@."
(Driver.print_task driver) goal; (Driver.print_task driver) goal;
let pre_call = begin
Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal try
in let pre_call =
Queue.push (callback,pre_call) proof_attempts_queue; Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
run_timeout_handler () in
Queue.push (callback,pre_call) proof_attempts_queue;
run_timeout_handler ()
with e ->
Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
Exn_printer.exn_printer e;
callback (InternalFailure e)
end
| Action_delayed callback -> callback () | Action_delayed callback -> callback ()
end; end;
true true
...@@ -497,6 +504,12 @@ let idle_handler () = ...@@ -497,6 +504,12 @@ let idle_handler () =
eprintf "Info: idle_handler stopped@."; eprintf "Info: idle_handler stopped@.";
*) *)
false false
| e ->
Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
Exn_printer.exn_printer e;
eprintf "Session.idle_handler stopped@.";
false
let run_idle_handler () = let run_idle_handler () =
if !idle_handler_activated then () else if !idle_handler_activated then () else
......
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