diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml
index adada4b951c16a2c02ea9c31b259737a41b71a89..d0d23f5bd78111543b224192feeca18fb67eaf58 100644
--- a/src/ide/why3ide.ml
+++ b/src/ide/why3ide.ml
@@ -686,7 +686,7 @@ let image_of_pa_status ~obsolete pa =
   match pa with
   | Controller_itp.Unedited -> !image_scheduled (* TODO !image_unedited *)
   | Controller_itp.JustEdited -> !image_scheduled (* TODO !image_edited *)
-  | Controller_itp.Interrupted -> !image_scheduled (* TODO !image_interrrupted *)
+  | Controller_itp.Interrupted -> !image_undone
   | Controller_itp.Scheduled -> !image_scheduled
   | Controller_itp.Running -> !image_running
   | Controller_itp.InternalFailure _e -> !image_failure
diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index db84ad5d1772459b9b3e08e3e505e471b1e6d0cc..0e47a2e25493693d4d5b10820530bf1d6cb5eff0 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -506,6 +506,20 @@ let timeout_handler () =
   !observer scheduled (waiting_or_running - running) running;
   true
 
+let interrupt () =
+  while not (Queue.is_empty prover_tasks_in_progress) do
+    let (_ses,_id,_pr,callback,_started,_call) =
+      Queue.pop prover_tasks_in_progress in
+    (* TODO: apply some Call_provers.interrupt_call call *)
+    callback Interrupted
+  done;
+  number_of_running_provers := 0;
+  while not (Queue.is_empty scheduled_proof_attempts) do
+    let (_c,_id,_pr,_limit,callback) = Queue.pop scheduled_proof_attempts in
+    callback Interrupted
+  done;
+  !observer 0 0 0
+
 let run_timeout_handler () =
   if not !timeout_handler_running then
     begin
@@ -593,7 +607,8 @@ let run_strategy_on_goal
            | Done { Call_provers.pr_answer = Call_provers.Valid } ->
               (* proof succeeded, nothing more to do *)
               callback STShalt
-           | Interrupted | InternalFailure _
+           | Interrupted | InternalFailure _ ->
+              callback STShalt
            | Done _ ->
               (* proof did not succeed, goto to next step *)
               callback (STSgoto (g,pc+1));
diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli
index 475d9f03e0144a0c45b6c1d95bdbfb7deabd3014..4d6b5c324dbaf6a9166da0a22cb1d2fc5c0ae858 100644
--- a/src/session/controller_itp.mli
+++ b/src/session/controller_itp.mli
@@ -159,6 +159,10 @@ val register_observer : (int -> int -> int -> unit) -> unit
     tasks, scheduled tasks, and running taks, each time these numbers
     change *)
 
+val interrupt : unit -> unit
+(** discards all scheduled proof attempts or transformations, including
+    the one already running *)
+
 val schedule_proof_attempt :
   controller ->
   proofNodeID ->
diff --git a/src/session/itp_communication.ml b/src/session/itp_communication.ml
index aa497cdc72c6899d8f25b2b74a9da6e044100895..1abd25f8b5fc5fc5a439113bd7dd943598212488 100644
--- a/src/session/itp_communication.ml
+++ b/src/session/itp_communication.ml
@@ -96,3 +96,4 @@ type ide_request =
   | Reload_req
   | Replay_req
   | Exit_req
+  | Interrupt_req
diff --git a/src/session/itp_communication.mli b/src/session/itp_communication.mli
index 30ee29ffe5028643c3b01673027a06c67c6e9bb4..9736825391c877bc31b1b992124136567db0efce 100644
--- a/src/session/itp_communication.mli
+++ b/src/session/itp_communication.mli
@@ -103,3 +103,4 @@ type ide_request =
   | Reload_req
   | Replay_req
   | Exit_req
+  | Interrupt_req
diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 197bb1c3d257bfee393ed2ff93b7a3a865326e7f..a3737ae0404b0029a6223bedf88ed70a69615e1c 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -294,6 +294,7 @@ let print_request fmt r =
   | Reload_req                      -> fprintf fmt "reload"
   | Replay_req                      -> fprintf fmt "replay"
   | Exit_req                        -> fprintf fmt "exit"
+  | Interrupt_req                   -> fprintf fmt "interrupt"
 
 let print_msg fmt m =
   match m with
@@ -1020,6 +1021,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
         save_file name text;
     | Get_task nid                 -> send_task nid
     | Replay_req                   -> replay_session (); resend_the_tree ()
+    | Interrupt_req                -> C.interrupt ()
     | Command_req (nid, cmd)       ->
       begin
         let snid = get_proof_node_id nid in
@@ -1028,6 +1030,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
         | Query s                 -> P.notify (Message (Query_Info (nid, s)))
         | Prove (p, limit)        -> schedule_proof_attempt nid p limit
         | Strategies st           -> run_strategy_on_task nid st
+        | Interrupt               -> C.interrupt ()
         | Help_message s          -> P.notify (Message (Help s))
         | QError s                -> P.notify (Message (Query_Error (nid, s)))
         | Other (s, _args)        ->
diff --git a/src/session/json_util.ml b/src/session/json_util.ml
index 96ff87e54e34e63d0a9583714955e36b8682c1a1..daaa1ebc9f31da811e58153bb8ede402f72ea84d 100644
--- a/src/session/json_util.ml
+++ b/src/session/json_util.ml
@@ -129,6 +129,7 @@ let convert_request_constructor (r: ide_request) =
   | Reload_req                -> String "Reload_req"
   | Replay_req                -> String "Replay_req"
   | Exit_req                  -> String "Exit_req"
+  | Interrupt_req             -> String "Interrupt_req"
 
 let print_request_to_json (r: ide_request): Json_base.value =
   let cc = convert_request_constructor in
@@ -192,6 +193,8 @@ let print_request_to_json (r: ide_request): Json_base.value =
       Obj ["ide_request", cc r]
   | Exit_req ->
       Obj ["ide_request", cc r]
+  | Interrupt_req ->
+      Obj ["ide_request", cc r]
 
 let convert_constructor_message (m: message_notification) =
   match m with
diff --git a/src/session/server_utils.ml b/src/session/server_utils.ml
index b6d33c57d6a9cf7849e71cc641a6db1891f17680..5bbba47c695967628265d6c2b0bb7f01a61425fe 100644
--- a/src/session/server_utils.ml
+++ b/src/session/server_utils.ml
@@ -232,6 +232,7 @@ type command =
   | Transform    of string * Trans.gentrans * string list
   | Prove        of Whyconf.config_prover * Call_provers.resource_limit
   | Strategies   of string
+  | Interrupt
   | Help_message of string
   | Query        of string
   | QError       of string
@@ -250,6 +251,7 @@ let interp_others commands config cmd args =
             | _ -> "1"
           in
           Strategies s
+      | "interrupt" -> Interrupt
       | "help" ->
           let text = Pp.sprintf
                           "Please type a command among the following (automatic completion available)@\n\
diff --git a/src/session/server_utils.mli b/src/session/server_utils.mli
index 03aa204f0515eb0a77115ba1e07dd16c3a10a89f..373fe128103268b56ca118a8762cef5a9c15a1a3 100644
--- a/src/session/server_utils.mli
+++ b/src/session/server_utils.mli
@@ -43,6 +43,7 @@ type command =
   | Transform    of string * Trans.gentrans * string list
   | Prove        of Whyconf.config_prover * Call_provers.resource_limit
   | Strategies   of string
+  | Interrupt
   | Help_message of string
   | Query        of string
   | QError       of string