Robustness fix : clean restart of coqtop on pipe error + force matching

of coqtop return codes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13245 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 242 insertions, 222 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index c40343a7e..fbad08812 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -104,9 +104,16 @@ object(self)
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
       try
-	Coq.raw_interp coqtop phrase;
-	result#buffer#set_text
-	  ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout coqtop))
+        result#buffer#set_text
+          (match Coq.raw_interp coqtop phrase with
+             | Ide_blob.Fail (l,str) ->
+                 ("Error while interpreting "^phrase^":\n"^str)
+             | Ide_blob.Good () ->
+                 match Coq.read_stdout coqtop with
+                   | Ide_blob.Fail (l,str) ->
+                       ("Error while fetching "^phrase^"results:\n"^str)
+                   | Ide_blob.Good results ->
+                       ("Result for command " ^ phrase ^ ":\n" ^ results))
       with e ->
 	let (s,loc) = Coq.process_exn e in
 	assert (Glib.Utf8.validate s);
diff --git a/ide/coq.ml b/ide/coq.ml
index 72f7e9541..9f1c807b8 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -29,12 +29,14 @@ type coqtop = {
   mutable cout : in_channel ;
   mutable cin : out_channel ;
   sup_args : string ;
+  mutable version : int ;
 }
 
 let dummy_coqtop = {
   cout = stdin ;
   cin = stdout ;
   sup_args = "" ;
+  version = 0 ;
 }
 
 let prerr_endline s = if !debug then prerr_endline s else ()
@@ -81,14 +83,9 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
-exception Coq_failure of (Util.loc option * string)
-
 let eval_call coqtop (c:'a Ide_blob.call) =
   Safe_marshal.send coqtop.cin c;
-  let res = (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout in
-  match res with
-    | Ide_blob.Good v -> v
-    | Ide_blob.Fail err -> raise (Coq_failure err)
+  (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout
 
 let is_in_loadpath coqtop s = eval_call coqtop (Ide_blob.is_in_loadpath s)
  
@@ -112,18 +109,20 @@ let spawn_coqtop sup_args =
     let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave "^sup_args) in
     incr toplvl_ctr;
     Mutex.unlock toplvl_ctr_mtx;
-    { cin = ic; cout = oc ; sup_args = sup_args }
+    { cin = ic; cout = oc ; sup_args = sup_args ; version = 0 }
   with e ->
     Mutex.unlock toplvl_ctr_mtx;
     raise e
 
 let kill_coqtop coqtop =
+  let ic = coqtop.cin in
+  let oc = coqtop.cout in
   ignore (Thread.create
             (fun () ->
                try 
-                 ignore (Unix.close_process (coqtop.cout,coqtop.cin));
-                 Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx;
-               with _ -> ())
+                 ignore (Unix.close_process (oc,ic));
+                 Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
+               with _ -> prerr_endline "Process leak")
             ())
 
 let coqtop_zombies =
@@ -137,7 +136,7 @@ let reset_coqtop coqtop =
   kill_coqtop coqtop;
   let ni = spawn_coqtop coqtop.sup_args in
   coqtop.cin <- ni.cin;
-  coqtop.cout <- ni.cout
+  coqtop.cout <- ni.cout;
 
 module PrintOpt =
 struct
@@ -156,13 +155,21 @@ struct
 
   let set coqtop opt value =
     Hashtbl.replace state_hack opt value;
-    List.iter
-      (fun cmd -> 
+    List.fold_left
+      (fun acc cmd -> 
          let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
-         raw_interp coqtop str)
+         match raw_interp coqtop str with
+           | Ide_blob.Good () -> acc
+           | Ide_blob.Fail (l,errstr) ->  Ide_blob.Fail (l,"Could not eval \""^str^"\": "^errstr)
+      )
+      (Ide_blob.Good ())
       opt
 
-  let enforce_hack coqtop = Hashtbl.iter (set coqtop) state_hack 
+  let enforce_hack coqtop = Hashtbl.fold (fun opt v acc ->
+                                            match set coqtop opt v with
+                                              | Ide_blob.Good () -> Ide_blob.Good ()
+                                              | Ide_blob.Fail str -> Ide_blob.Fail str)
+                              state_hack (Ide_blob.Good ())
 end
 
 let rec is_pervasive_exn = function
@@ -197,14 +204,10 @@ let print_toplevel_error exc =
 
 let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
 
-type tried_tactic =
-  | Interrupted
-  | Success of int (* nb of goals after *)
-  | Failed
-
 let goals coqtop =
-  PrintOpt.enforce_hack coqtop;
-  eval_call coqtop Ide_blob.current_goals
+  match PrintOpt.enforce_hack coqtop with
+    | Ide_blob.Good () -> eval_call coqtop Ide_blob.current_goals
+    | Ide_blob.Fail str -> Ide_blob.Fail str
 
 let make_cases coqtop s = eval_call coqtop (Ide_blob.make_cases s)
 
diff --git a/ide/coq.mli b/ide/coq.mli
index 30ee75d41..4b59b5e75 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -27,7 +27,7 @@ val coqtop_zombies : unit -> int
 
 val reset_coqtop : coqtop -> unit
 
-exception Coq_failure of (Util.loc option * string)
+val process_exn : exn -> string*(Util.loc option)
 
 module PrintOpt :
 sig
@@ -40,32 +40,25 @@ sig
   val existential : t
   val universes : t
 
-  val set : coqtop -> t -> bool -> unit
+  val set : coqtop -> t -> bool -> unit Ide_blob.value
 end
 
-val raw_interp : coqtop -> string -> unit
-
-val interp : coqtop -> bool -> string -> int
+val raw_interp : coqtop -> string -> unit Ide_blob.value
 
-val rewind : coqtop -> int -> int
+val interp : coqtop -> bool -> string -> int Ide_blob.value
 
-val read_stdout : coqtop -> string
-
-val process_exn : exn -> string*(Util.loc option)
+val rewind : coqtop -> int -> int Ide_blob.value
 
-val is_in_loadpath : coqtop -> string -> bool
+val read_stdout : coqtop -> string Ide_blob.value
 
-val make_cases : coqtop -> string -> string list list
+val is_in_loadpath : coqtop -> string -> bool Ide_blob.value
 
-type tried_tactic =
-  | Interrupted
-  | Success of int (* nb of goals after *)
-  | Failed
+val make_cases : coqtop -> string -> string list list Ide_blob.value
 
 (* Message to display in lower status bar. *)
 
-val current_status : coqtop -> string
+val current_status : coqtop -> string Ide_blob.value
 
-val goals : coqtop -> goals
+val goals : coqtop -> goals Ide_blob.value
 
 val msgnl : Pp.std_ppcmds -> string
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 55feea70d..d5450220e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -235,24 +235,29 @@ let do_if_not_computing text f x =
   if Mutex.try_lock coq_computing then
     let threaded_task () =
       prerr_endline "Getting lock";
-      try
-        f x;
-        prerr_endline "Releasing lock";
-        Mutex.unlock coq_computing;
-      with e ->
-        prerr_endline "Releasing lock (on error)";
-        Mutex.unlock coq_computing;
-        raise e
+      List.iter
+        (fun elt -> try f elt with
+           | Sys_error str ->
+               elt.analyzed_view#reset_initial;
+               elt.analyzed_view#set_message
+                 ("unable to communicate with coqtop, restarting coqtop:\n"^str)
+           | e ->
+               Mutex.unlock coq_computing;
+               elt.analyzed_view#set_message
+                 ("Unknown error, please report:\n"^(Printexc.to_string e)))
+        x;
+      prerr_endline "Releasing lock";
+      Mutex.unlock coq_computing;
     in
-      prerr_endline ("Launching thread " ^ text);
-      ignore (Glib.Timeout.add ~ms:300 ~callback:
-                  (fun () -> if Mutex.try_lock coq_computing
-                             then (Mutex.unlock coq_computing; false)
-                             else (pbar#pulse (); true)));
-      ignore (Thread.create threaded_task ())
-  else
-    prerr_endline
-      "Discarded order (computations are ongoing)"
+    prerr_endline ("Launching thread " ^ text);
+    ignore (Glib.Timeout.add ~ms:300 ~callback:
+              (fun () -> if Mutex.try_lock coq_computing
+               then (Mutex.unlock coq_computing; false)
+               else (pbar#pulse (); true)));
+    ignore (Thread.create threaded_task ())
+    else
+      prerr_endline
+        "Discarded order (computations are ongoing)"
 
 let remove_current_view_page () =
   let c = session_notebook#current_page in
@@ -271,7 +276,12 @@ let print_items = [
 ]
 
 let setopts ct opts v =
-  List.iter (fun o -> set ct o v) opts
+  List.fold_left
+    (fun acc o ->
+       match set ct o v with
+         | Ide_blob.Good () -> acc
+         | Ide_blob.Fail lstr -> Ide_blob.Fail lstr
+    ) (Ide_blob.Good ()) opts
 
 (* Reset this to None on page change ! *)
 let (last_completion:(string*int*int*bool) option ref) = ref None
@@ -717,9 +727,13 @@ object(self)
         else
           (fun _ _ -> ()) in
         try
-          Ideproof.display
-            (Ideproof.mode_tactic menu_callback)
-            proof_view (Coq.goals mycoqtop)
+          match Coq.goals mycoqtop with
+            | Ide_blob.Fail (l,str) ->
+                self#set_message ("Error in coqtop :\n"^str)
+            | Ide_blob.Good goals ->
+                Ideproof.display
+                  (Ideproof.mode_tactic menu_callback)
+                  proof_view goals
         with
           | e -> prerr_endline (Printexc.to_string e)
       end
@@ -755,14 +769,18 @@ object(self)
     try
       full_goal_done <- false;
       prerr_endline "Send_to_coq starting now";
-      let r = Coq.interp mycoqtop verbosely phrase in
-      let is_complete = true in
-      let msg = Coq.read_stdout mycoqtop in
-      sync display_output msg;
-      Some (is_complete,r)
+      match Coq.interp mycoqtop verbosely phrase with
+        | Ide_blob.Fail (l,str) -> sync display_error (str,l); None
+        | Ide_blob.Good r ->
+            match Coq.read_stdout mycoqtop with
+              | Ide_blob.Fail (_,str) ->
+                  self#set_message
+                    ("interp successful but unable to fetch goal, please report bug:\n"^str);
+                  None
+              | Ide_blob.Good msg ->
+                  sync display_output msg;
+                  Some (true,r)
     with
-      | Coq_failure (l,s) ->
-          sync display_error (s,l); None
       | e ->
           sync display_error (Coq.process_exn e); None
 
@@ -971,29 +989,31 @@ object(self)
     in
     begin
       try
-        prerr_endline (string_of_int (Coq.rewind mycoqtop (n_step 0)));
-        prerr_endline (string_of_int (Stack.length cmd_stack));
-        sync (fun _ ->
-                let start =
-                  if Stack.is_empty cmd_stack then input_buffer#start_iter
-                  else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
-                prerr_endline "Removing (long) processed tag...";
-                input_buffer#remove_tag
-                  Tags.Script.processed
-                  ~start
-                  ~stop:self#get_start_of_input;
-                input_buffer#remove_tag
-                  Tags.Script.unjustified
-                  ~start
-                  ~stop:self#get_start_of_input;
-                prerr_endline "Moving (long) start_of_input...";
-                input_buffer#move_mark ~where:start (`NAME "start_of_input");
-                self#show_goals;
-                self#clear_message)
-          ();
+        match Coq.rewind mycoqtop (n_step 0) with
+          | Ide_blob.Fail (l,str) ->
+              sync self#set_message
+                ("Problem while backtracking, CoqIDE and coqtop may be out of sync, you may want to restart :\n"^str)
+          | Ide_blob.Good _ ->
+              sync (fun _ ->
+                      let start =
+                        if Stack.is_empty cmd_stack then input_buffer#start_iter
+                        else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
+                      prerr_endline "Removing (long) processed tag...";
+                      input_buffer#remove_tag
+                        Tags.Script.processed
+                        ~start
+                        ~stop:self#get_start_of_input;
+                      input_buffer#remove_tag
+                        Tags.Script.unjustified
+                        ~start
+                        ~stop:self#get_start_of_input;
+                      prerr_endline "Moving (long) start_of_input...";
+                      input_buffer#move_mark ~where:start (`NAME "start_of_input");
+                      self#show_goals;
+                      self#clear_message)
+                ();
       with _ ->
-        push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
-                                                                 Please restart and report NOW.";
+        push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. Please restart and report NOW.";
     end
 
   method backtrack_to i =
@@ -1109,11 +1129,18 @@ object(self)
     with
       | None -> ()
       | Some f -> let dir = Filename.dirname f in
-          if not (is_in_loadpath mycoqtop dir) then
-            begin
-              ignore (Coq.interp mycoqtop false
-                        (Printf.sprintf "Add LoadPath \"%s\". "  dir))
-            end
+        match Coq.is_in_loadpath mycoqtop dir with
+          | Ide_blob.Fail (_,str) ->
+              self#set_message
+                ("Could not determine lodpath, this might lead to problems:\n"^str)
+          | Ide_blob.Good true -> ()
+          | Ide_blob.Good false ->
+              match Coq.interp mycoqtop false
+                        (Printf.sprintf "Add LoadPath \"%s\". "  dir) with
+                | Ide_blob.Fail (l,str) ->
+                    self#set_message
+                      ("Couln't add loadpath:\n"^str)
+                | Ide_blob.Good _ -> ()
   end
 
   method electric_handler =
@@ -1692,10 +1719,7 @@ let main files =
     (* XXX *)
     (* File/Revert Menu *)
     let revert_m = file_factory#add_item "_Revert all buffers" in
-    let revert_f () =
-      List.iter
-        (function
-             {analyzed_view = av} ->
+    let revert_f {analyzed_view = av} =
                (try
                   match av#filename,av#stats with
                     | Some f,Some stats ->
@@ -1705,9 +1729,8 @@ let main files =
                     | Some _, None -> av#revert
                     | _ -> ()
                 with _ -> av#revert)
-        ) session_notebook#pages
     in
-    ignore (revert_m#connect#activate revert_f);
+    ignore (revert_m#connect#activate (fun () -> List.iter revert_f session_notebook#pages));
 
     (* File/Close Menu *)
     let close_m =
@@ -1823,46 +1846,46 @@ let main files =
       in
       ignore (w#event#connect#delete (fun _ -> quit_f (); true));
 
-		      (* Edit Menu *)
-		      let edit_menu = factory#add_submenu "_Edit" in
-		      let edit_f = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Edit/" edit_menu ~accel_group in
-			ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
-				 (do_if_not_computing "undo"
-				    (fun () ->
-				       ignore (session_notebook#current_term.analyzed_view#
-						 without_auto_complete
-						 (fun () -> session_notebook#current_term.script#undo) ()))));
-			ignore(edit_f#add_item "_Clear Undo Stack"
-				 (* ~key:GdkKeysyms._exclam *)
-				 ~callback:
-				 (fun () ->
-				    ignore session_notebook#current_term.script#clear_undo));
-			ignore(edit_f#add_separator ());
-                        let get_active_view_for_cp () =
-                          let has_sel (i0,i1) = i0#compare i1 <> 0 in
-                          let current = session_notebook#current_term in
-                            if has_sel current.script#buffer#selection_bounds
-                            then current.script#as_view
-                            else if has_sel current.proof_view#buffer#selection_bounds
-                            then current.proof_view#as_view
-                            else current.message_view#as_view
-                        in
-			ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
-				 (fun () -> GtkSignal.emit_unit
-				    (get_active_view_for_cp ())
-				    GtkText.View.S.cut_clipboard
-                                 ));
-			ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
-				 (fun () -> GtkSignal.emit_unit
-				    (get_active_view_for_cp ())
-				    GtkText.View.S.copy_clipboard));
-			ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
-				 (fun () ->
-				    try GtkSignal.emit_unit
-				      session_notebook#current_term.script#as_view
-				      GtkText.View.S.paste_clipboard
-				    with _ -> prerr_endline "EMIT PASTE FAILED"));
-			ignore (edit_f#add_separator ());
+      (* Edit Menu *)
+      let edit_menu = factory#add_submenu "_Edit" in
+      let edit_f = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Edit/" edit_menu ~accel_group in
+      ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
+               (fun () -> do_if_not_computing "undo"
+                            (fun sess ->
+                               ignore (sess.analyzed_view#without_auto_complete
+                                         (fun () -> session_notebook#current_term.script#undo) ()))
+               [session_notebook#current_term]));
+      ignore(edit_f#add_item "_Clear Undo Stack"
+               (* ~key:GdkKeysyms._exclam *)
+               ~callback:
+               (fun () ->
+                  ignore session_notebook#current_term.script#clear_undo));
+      ignore(edit_f#add_separator ());
+      let get_active_view_for_cp () =
+        let has_sel (i0,i1) = i0#compare i1 <> 0 in
+        let current = session_notebook#current_term in
+        if has_sel current.script#buffer#selection_bounds
+        then current.script#as_view
+        else if has_sel current.proof_view#buffer#selection_bounds
+        then current.proof_view#as_view
+        else current.message_view#as_view
+      in
+      ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
+               (fun () -> GtkSignal.emit_unit
+                            (get_active_view_for_cp ())
+                            GtkText.View.S.cut_clipboard
+               ));
+      ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
+               (fun () -> GtkSignal.emit_unit
+                            (get_active_view_for_cp ())
+                            GtkText.View.S.copy_clipboard));
+      ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
+               (fun () ->
+                  try GtkSignal.emit_unit
+                        session_notebook#current_term.script#as_view
+                        GtkText.View.S.paste_clipboard
+                  with _ -> prerr_endline "EMIT PASTE FAILED"));
+      ignore (edit_f#add_separator ());
 
 
 			(*
@@ -2136,19 +2159,14 @@ let main files =
 				  (GMain.Timeout.add ~ms:!current.global_auto_revert_delay
 				     ~callback:
 				     (fun () ->
-					do_if_not_computing "revert" (sync revert_f) ();
+					do_if_not_computing "revert" (sync revert_f) session_notebook#pages;
 					true))
 			    in reset_revert_timer (); (* to enable statup preferences timer *)
                               (* XXX *)
-			      let auto_save_f () =
-				List.iter
-				  (function
-				       {script = view ; analyzed_view = av} ->
-					 (try
-					      av#auto_save
-					  with _ -> ())
-				  )
-				  session_notebook#pages
+			      let auto_save_f {analyzed_view = av} =
+                                (try
+                                   av#auto_save
+                                 with _ -> ())
 			      in
 
 			      let reset_auto_save_timer () =
@@ -2158,7 +2176,7 @@ let main files =
 				    (GMain.Timeout.add ~ms:!current.auto_save_delay
 				       ~callback:
 				       (fun () ->
-					  do_if_not_computing "autosave" (sync auto_save_f) ();
+					  do_if_not_computing "autosave" (sync auto_save_f) session_notebook#pages;
 					  true))
 			      in reset_auto_save_timer (); (* to enable statup preferences timer *)
 
@@ -2181,15 +2199,19 @@ let main files =
 				    ~accel_group
 				    ~accel_modi:!current.modifier_for_navigation
 				in
-                                let do_or_activate f =
+                                let do_or_activate f () =
                                   do_if_not_computing "do_or_activate"
-                                    (fun () ->
-                                       let current = session_notebook#current_term in
+                                    (fun current ->
                                        let av = current.analyzed_view in
                                        ignore (f av);
                                        pop_info ();
-                                       push_info (Coq.current_status current.toplvl)
-                                    )
+                                       push_info
+                                         (match Coq.current_status current.toplvl with
+                                            | Ide_blob.Fail (l,str) ->
+                                                "Oops, problem while fetching coq status."
+                                            | Ide_blob.Good str -> str)
+                                       )
+                                    [session_notebook#current_term]
                                 in
 				let add_to_menu_toolbar text ~tooltip ?key ~callback icon =
 				  begin
@@ -2265,13 +2287,10 @@ let main files =
 				      ~accel_group
 				      ~accel_modi:!current.modifier_for_tactics
 				  in
-				  let do_if_active_raw f () =
-				    let current = session_notebook#current_term in
-				    let analyzed_view = current.analyzed_view in
-				      if analyzed_view#is_active then ignore (f analyzed_view)
-				  in
-				  let do_if_active f =
-				    do_if_not_computing "do_if_active" (do_if_active_raw f) in
+				  let do_if_active f () =
+                                    do_if_not_computing "do_if_active"
+                                      (fun sess -> ignore (f sess.analyzed_view))
+                                      [session_notebook#current_term] in
 
 				    ignore (tactics_factory#add_item "_auto"
 					      ~key:GdkKeysyms._a
@@ -2417,32 +2436,33 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					  let w = get_current_word () in
 let cur_ct = session_notebook#current_term.toplvl in
 					    try
-					      let cases = Coq.make_cases cur_ct w
-					      in
-					      let print c = function
-						| [x] -> Format.fprintf c "  | %s => _@\n" x
-						| x::l -> Format.fprintf c "  | (%s%a) => _@\n" x
-						    (print_list (fun c s -> Format.fprintf c " %s" s)) l
-						| [] -> assert false
-					      in
-					      let b = Buffer.create 1024 in
-					      let fmt = Format.formatter_of_buffer b in
-						Format.fprintf fmt "@[match var with@\n%aend@]@."
-						  (print_list print) cases;
-						let s = Buffer.contents b in
-						  prerr_endline s;
-						  let {script = view } = session_notebook#current_term in
-						    ignore (view#buffer#delete_selection ());
-						    let m = view#buffer#create_mark
-						      (view#buffer#get_iter `INSERT)
-						    in
-						      if view#buffer#insert_interactive s then
-							let i = view#buffer#get_iter (`MARK m) in
-							let _ = i#nocopy#forward_chars 9 in
-							  view#buffer#place_cursor i;
-							  view#buffer#move_mark ~where:(i#backward_chars 3)
-							    `SEL_BOUND
-					    with Not_found -> flash_info "Not an inductive type"
+                                              match Coq.make_cases cur_ct w with
+                                                | Ide_blob.Fail _ -> raise Not_found
+                                                | Ide_blob.Good cases ->
+                                                    let print c = function
+                                                      | [x] -> Format.fprintf c "  | %s => _@\n" x
+                                                      | x::l -> Format.fprintf c "  | (%s%a) => _@\n" x
+                                                                  (print_list (fun c s -> Format.fprintf c " %s" s)) l
+                                                      | [] -> assert false
+                                                    in
+                                                    let b = Buffer.create 1024 in
+                                                    let fmt = Format.formatter_of_buffer b in
+                                                    Format.fprintf fmt "@[match var with@\n%aend@]@."
+                                                      (print_list print) cases;
+                                                    let s = Buffer.contents b in
+                                                    prerr_endline s;
+                                                    let {script = view } = session_notebook#current_term in
+                                                    ignore (view#buffer#delete_selection ());
+                                                    let m = view#buffer#create_mark
+                                                              (view#buffer#get_iter `INSERT)
+                                                    in
+                                                    if view#buffer#insert_interactive s then
+                                                      let i = view#buffer#get_iter (`MARK m) in
+                                                      let _ = i#nocopy#forward_chars 9 in
+                                                      view#buffer#place_cursor i;
+                                                      view#buffer#move_mark ~where:(i#backward_chars 3)
+                                                        `SEL_BOUND
+                                            with Not_found -> flash_info "Not an inductive type"
 					in
 					  ignore (templates_factory#add_item "match ..."
 						    ~key:GdkKeysyms._C
@@ -2571,7 +2591,7 @@ let cur_ct = session_notebook#current_term.toplvl in
                        (fun (opts,text,key,dflt) -> 
                           view_factory#add_check_item ~key ~active:dflt text
                             ~callback:(fun v -> do_or_activate (fun a ->
-                                                                  setopts session_notebook#current_term.toplvl opts v;
+                                                                  ignore (setopts session_notebook#current_term.toplvl opts v);
                                                                   a#show_goals) ()))
                        print_items
              in
@@ -2722,35 +2742,32 @@ let cur_ct = session_notebook#current_term.toplvl in
 					    configuration_factory#add_item
 					      "Detach _View"
 					      ~callback:
-					      (do_if_not_computing "detach view"
-						 (fun () ->
-						    match session_notebook#current_term with
-						      | {script=v;analyzed_view=av} ->
-							  let w = GWindow.window ~show:true
-							    ~width:(!current.window_width*2/3)
-							    ~height:(!current.window_height*2/3)
-							    ~position:`CENTER
-							    ~title:(match av#filename with
-								      | None -> "*Unnamed*"
-								      | Some f -> f)
-							    ()
-							  in
-							  let sb = GBin.scrolled_window
-							    ~packing:w#add ()
-							  in
-							  let nv = GText.view
-							    ~buffer:v#buffer
-							    ~packing:sb#add
-							    ()
-							  in
-							    nv#misc#modify_font
-							      !current.text_font;
-							    ignore (w#connect#destroy
-								      ~callback:
-								      (fun () -> av#remove_detached_view w));
-							    av#add_detached_view w
-
-						 ))
+					      (fun () -> do_if_not_computing "detach view"
+						 (function {script=v;analyzed_view=av} ->
+                                                   let w = GWindow.window ~show:true
+                                                             ~width:(!current.window_width*2/3)
+                                                             ~height:(!current.window_height*2/3)
+                                                             ~position:`CENTER
+                                                             ~title:(match av#filename with
+                                                                       | None -> "*Unnamed*"
+                                                                       | Some f -> f)
+                                                             ()
+                                                   in
+                                                   let sb = GBin.scrolled_window
+                                                              ~packing:w#add ()
+                                                   in
+                                                   let nv = GText.view
+                                                              ~buffer:v#buffer
+                                                              ~packing:sb#add
+                                                              ()
+                                                   in
+                                                   nv#misc#modify_font
+                                                     !current.text_font;
+                                                   ignore (w#connect#destroy
+                                                             ~callback:
+                                                             (fun () -> av#remove_detached_view w));
+                                                   av#add_detached_view w)
+                                              [session_notebook#current_term])
 					  in
 					    (* Help Menu *)