From caaba2d077362ec7ac6185757ac3304e94e95f37 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Thu, 22 Sep 2011 16:00:00 +0200
Subject: [PATCH] improve robustness of IDE
---
src/ide/gmain.ml | 22 ++++++++++++++++------
src/ide/session.ml | 23 ++++++++++++++++++-----
2 files changed, 34 insertions(+), 11 deletions(-)
diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml
index 991a47c8d4..bc8a7abcfd 100644
--- a/src/ide/gmain.ml
+++ b/src/ide/gmain.ml
@@ -621,11 +621,15 @@ let () =
let prover_on_selected_goals pr =
List.iter
(fun row ->
+ try
let a = get_any_from_row_reference row in
- M.run_prover
- ~context_unproved_goals_only:!context_unproved_goals_only
- ~timelimit:gconfig.time_limit
- pr a)
+ M.run_prover
+ ~context_unproved_goals_only:!context_unproved_goals_only
+ ~timelimit:gconfig.time_limit
+ pr a
+ with e ->
+ eprintf "@[Exception raised while running a prover:@ %a@.@]"
+ Exn_printer.exn_printer e)
(get_selected_row_references ())
(**********************************)
@@ -1506,8 +1510,14 @@ let select_row r =
| M.Proof_attempt a ->
let o =
match a.M.proof_state with
- | Session.Done r -> r.Call_provers.pr_output;
- | _ -> "No information available"
+ | Session.Undone -> "proof not yet scheduled for running"
+ | 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
task_view#source_buffer#set_text o;
scroll_to_source_goal a.M.proof_goal
diff --git a/src/ide/session.ml b/src/ide/session.ml
index 67ef366899..58f968dc6c 100644
--- a/src/ide/session.ml
+++ b/src/ide/session.ml
@@ -483,11 +483,18 @@ let idle_handler () =
if debug then
Format.eprintf "Task for prover: %a@."
(Driver.print_task driver) goal;
- let pre_call =
- Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
- in
- Queue.push (callback,pre_call) proof_attempts_queue;
- run_timeout_handler ()
+ begin
+ try
+ let pre_call =
+ Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
+ 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 ()
end;
true
@@ -497,6 +504,12 @@ let idle_handler () =
eprintf "Info: idle_handler stopped@.";
*)
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 () =
if !idle_handler_activated then () else
--
GitLab