diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml
index 36a49f226c036a9b549dbbf9b8a8f2802e8271d7..04e299b61bd86642a7dc303f36c9873f28153dcc 100644
--- a/src/ide/why3ide.ml
+++ b/src/ide/why3ide.ml
@@ -561,18 +561,18 @@ let run_strategy_on_task s =
 
 let clear_command_entry () = command_entry#set_text ""
 
-let current_id id =
-  match id with
-  | IproofNode id -> id
-  | _ -> assert (false) (* TODO *)
-
 let interp cmd =
-  let id = current_id !current_selected_index in
+  let id =
+    match !current_selected_index with
+    | IproofNode id -> Some id
+    | _ -> None
+  in
   match interp cont.controller_env id cont.controller_session cmd with
     | Transform(s,_t,args) ->
        clear_command_entry ();
        apply_transform cont.controller_session s args
     | Query s ->
+       clear_command_entry ();
        message_zone#buffer#set_text s
     | Other(s,args) ->
       begin
@@ -582,22 +582,29 @@ let interp cmd =
           test_schedule_proof_attempt cont.controller_session prover_config limit
         | None ->
           match s with
-       | "auto" ->
-           let s =
-             match args with
+          | "auto" ->
+             let s =
+               match args with
                | "2"::_ -> "2"
                | _ -> "1"
-           in
-           clear_command_entry ();
-           run_strategy_on_task s
-       | _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
+             in
+             clear_command_entry ();
+             run_strategy_on_task s
+          | "help" ->
+             clear_command_entry ();
+             let text = Pp.sprintf
+                          "Please type a command among the following (automatic completion available)@\n\
+                           @\n\
+                           @ <transformation name> [arguments]@\n\
+                           @ <prover name> [<time limit> [<mem limit>]]@\n\
+                           @ <query> [arguments]@\n\
+                           @ auto [auto level]@\n\
+                           @\n\
+                           Available queries are:@\n@[%a@]" help_on_queries ()
+             in
+             message_zone#buffer#set_text text
+          | _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
       end
-(*
-       match s with
-       | "c" -> clear_command_entry ();
-                test_schedule_proof_attempt cont.controller_session
-       | _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
- *)
 
 let (_ : GtkSignal.id) =
   command_entry#connect#activate
diff --git a/src/session/session_user_interface.ml b/src/session/session_user_interface.ml
index 5db0e9abd2f0e88bcf1c6be03c064ac55e816eec..d169cefa6fb9e50e6326c72ec2bd52abc02b851d 100644
--- a/src/session/session_user_interface.ml
+++ b/src/session/session_user_interface.ml
@@ -246,6 +246,12 @@ let commands =
  *)
   ]
 
+let help_on_queries fmt () =
+  let l = List.rev_map (fun (c,h,_) -> (c,h)) commands in
+  let l = List.sort sort_pair l in
+  let p fmt (c,help) = fprintf fmt "%20s : %s" c help in
+  Format.fprintf fmt "%a" (Pp.print_list Pp.newline p) l
+
 let commands_table = Stdlib.Hstr.create 17
 let () =
   List.iter
@@ -285,17 +291,20 @@ type command =
   | Other of string * string list
 
 let interp env id ses s =
-  let task = Session_itp.get_task ses id in
   let cmd,args = split_args s in
   try
     let f = Stdlib.Hstr.find commands_table cmd in
-    Query (f task args)
+    match id with
+    | None -> Query "please select a goal first"
+    | Some id ->
+       let task = Session_itp.get_task ses id in
+       Query (f task args)
   with Not_found ->
-       try
-         let t = Trans.lookup_trans env cmd in
-         Transform (cmd,t,args)
-       with Trans.UnknownTrans _ ->
-            Other(cmd,args)
+    try
+      let t = Trans.lookup_trans env cmd in
+      Transform (cmd,t,args)
+    with Trans.UnknownTrans _ ->
+      Other(cmd,args)
 
 
 (********* Callbacks tools *******)