coqide: .coqidepref en bin. Preferences en plus

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

3 files changed, 193 insertions, 87 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index f1ef1b4501..368ef6d9fc 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -80,6 +80,12 @@ let get_tab_label i =
 
 let get_current_tab_label () = get_tab_label (notebook())#current_page
 
+let get_current_page () = 
+  let i = (notebook())#current_page in
+  (notebook())#get_nth_page i
+
+				      
+
 let reset_tab_label i = set_tab_label i (get_tab_label i)
 
 let to_do_on_page_switch = ref []
@@ -135,7 +141,8 @@ object('self)
     method set_filename : string option -> unit
     method update_stats : unit
     method revert : unit
-    method save : string -> unit
+    method save : string -> bool
+    method save_as : string -> bool
     method read_only : bool
     method set_read_only : bool -> unit
     method is_active : bool
@@ -185,8 +192,9 @@ let crash_save i =
 	 | Some f -> f^".crashcoqide"
        in
        try 
-	 try_export filename (view#buffer#get_text ());
-	 Pervasives.prerr_endline ("Saved "^filename)
+	 if try_export filename (view#buffer#get_text ()) then
+	   Pervasives.prerr_endline ("Saved "^filename)
+	 else Pervasives.prerr_endline ("Could not save "^filename)
        with _ -> Pervasives.prerr_endline ("Could not save "^filename))
        | _ -> Pervasives.prerr_endline "Unanalyzed view found. Please report."
     )
@@ -440,21 +448,41 @@ object(self)
 		     "Some unsaved buffers changed on disk"
 		  )
 	    with 1 -> do_revert ()
-	      | 2 -> self#save f
+	      | 2 -> if self#save f then !flash_info "Overwritten" else
+		  !flash_info "Could not overwrite file"
 	      | _ -> 
 		  prerr_endline "Auto revert set to false";
-		  current.global_auto_revert <- false;
+		  !current.global_auto_revert <- false;
 		  disconnect_revert_timer ()
 	  else do_revert () 
 	end
       | None -> ()
 	  
   method save f = 
-    filename <- Some f;
-    try_export f (input_buffer#get_text ());
-    input_buffer#set_modified false;
-    stats <- my_stat f;
-
+    if try_export f (input_buffer#get_text ()) then begin
+      filename <- Some f;
+      input_buffer#set_modified false;
+      stats <- my_stat f;
+      true
+    end
+    else false
+    
+
+  method save_as f =
+    if Sys.file_exists f then 
+      match (GToolbox.question_box ~title:"File exists on disk"
+	       ~buttons:["Overwrite";
+			 "Cancel";] 
+	       ~default:1
+	       ~icon:
+	       (let img = GMisc.image () in
+		img#set_stock "gtk-dialog-warning" ~size:6;
+		img#coerce)
+	       ("File "^f^"already exists")
+	    )
+      with 1 -> self#save f
+	| _ -> false
+    else self#save f
 
   method set_read_only b = read_only<-b
   method read_only = read_only
@@ -1034,7 +1062,8 @@ let create_input_tab filename =
   let image = GMisc.image ~packing:v_box#pack () in
   let label = GMisc.label ~text:filename ~packing:v_box#pack () in
   let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
-	      ~packing:((notebook ())#append_page ~tab_label:v_box#coerce) () 
+	      ~packing:((notebook ())#append_page
+			  ~tab_label:v_box#coerce) () 
   in 
   let sw1 = GBin.scrolled_window
 	      ~vpolicy:`AUTOMATIC 
@@ -1097,7 +1126,7 @@ let main files =
 	    ~width:window_width ~height:window_height 
 	    ~title:"CoqIde" ()
   in
-  let accel_group = GtkData.AccelGroup.create () in
+(*  let accel_group = GtkData.AccelGroup.create () in *)
   let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
   let menubar = GMenu.menu_bar ~packing:vbox#pack () in
   let factory = new GMenu.factory menubar in
@@ -1167,13 +1196,16 @@ let main files =
 	     with
 	       | None -> ()
 	       | Some f -> 
-		   (out_some current.analyzed_view)#save f;
-		   set_current_tab_label (Filename.basename f);
-		   !flash_info "Saved"
+		   if (out_some current.analyzed_view)#save_as f then begin
+		     set_current_tab_label (Filename.basename f);
+		     !flash_info "Saved"
+		   end
+		   else !flash_info "Save Failed"
 	     end
 	 | Some f -> 
-	     (out_some current.analyzed_view)#save f;
-	     !flash_info "Saved"
+	     if (out_some current.analyzed_view)#save f then 
+	       !flash_info "Saved"
+	     else !flash_info "Save Failed"
 	       
       )
     with 
@@ -1191,9 +1223,11 @@ let main files =
 	       with
 		 | None -> ()
 		 | Some f -> 
-		     (out_some current.analyzed_view)#save f;
-		     set_current_tab_label (Filename.basename f);
-		     !flash_info "Saved"
+		     if (out_some current.analyzed_view)#save_as f then begin
+		       set_current_tab_label (Filename.basename f);
+		       !flash_info "Saved"
+		     end
+		     else !flash_info "Save Failed"
 	       end
 	   | Some f -> 
 	       begin match GToolbox.select_file 
@@ -1203,11 +1237,12 @@ let main files =
 	       with
 		 | None -> ()
 		 | Some f -> 
-		     (out_some current.analyzed_view)#save f;
-		     set_current_tab_label (Filename.basename f);
-		     !flash_info "Saved"
+		     if (out_some current.analyzed_view)#save_as f then begin
+		       set_current_tab_label (Filename.basename f);
+		       !flash_info "Saved"
+		     end else !flash_info "Save Failed"
 	       end);
-    with e -> !flash_info "Save failed"
+    with e -> !flash_info "Save Failed"
   in   
   ignore (saveas_m#connect#activate saveas_f);
   
@@ -1221,7 +1256,7 @@ let main files =
 	     begin match av#filename with 
 	       | None -> ()
 	       | Some f ->
-		   av#save f;
+		   ignore (av#save f)
 	     end
 	 | _ -> ()
       )  input_views
@@ -1275,8 +1310,8 @@ let main files =
       | Some f ->
 	  let cmd = 
 	    "cd " ^ Filename.dirname f ^ "; " ^
-	    current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^ 
-	    " | " ^ current.cmd_print
+	    !current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^ 
+	    " | " ^ !current.cmd_print
 	  in
 	  let c = Sys.command cmd in
 	  !flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
@@ -1301,7 +1336,7 @@ let main files =
 	  in
 	  let cmd = 
 	    "cd " ^ Filename.dirname f ^ "; " ^
-	    current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
+	    !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
 	  in
 	  let c = Sys.command cmd in
 	  !flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
@@ -1402,7 +1437,7 @@ let main files =
   let navigation_factory = 
     new GMenu.factory navigation_menu 
       ~accel_group 
-      ~accel_modi:current.modifier_for_navigation 
+      ~accel_modi:!current.modifier_for_navigation 
   in
   let do_or_activate f () = 
     let current = get_current_view () in
@@ -1442,7 +1477,7 @@ let main files =
   let tactics_factory = 
     new GMenu.factory tactics_menu 
       ~accel_group 
-      ~accel_modi:current.modifier_for_tactics
+      ~accel_modi:!current.modifier_for_tactics
   in
   let do_if_active f () = 
     let current = get_current_view () in
@@ -1494,21 +1529,15 @@ let main files =
   ignore (tactics_factory#add_item "<Proof _Wizzard>"
 	    ~key:GdkKeysyms._dollar
 	    ~callback:(do_if_active (fun a -> a#insert_commands 
-				       ["Progress Trivial.\n","Trivial.\n";
-					"Progress Auto.\n","Auto.\n";
-					"Tauto.\n","Tauto.\n";
-					"Omega.\n","Omega.\n";
-					"Progress Auto with *.\n","Auto with *.\n";
-					"Progress EAuto with *.\n","EAuto with *.\n";
-					"Progress Intuition.\n","Intuition.\n";
-				       ]))
+				       !current.automatic_tactics
+				    ))
 	 );
   
   (* Templates Menu *)
   let templates_menu =  factory#add_submenu "_Templates" in
   let templates_factory = new GMenu.factory templates_menu 
 			    ~accel_group 
-			    ~accel_modi:current.modifier_for_templates
+			    ~accel_modi:!current.modifier_for_templates
   in
   let add_complex_template (menu_text, text, offset, len, key) =
   (* Templates/Lemma *)
@@ -1598,7 +1627,7 @@ let main files =
       | None -> 
 	  !flash_info "Active buffer has no name"
       | Some f ->
-	  let c = Sys.command (current.cmd_coqc ^ " " ^ f) in
+	  let c = Sys.command (!current.cmd_coqc ^ " " ^ f) in
 	  if c = 0 then
 	    !flash_info (f ^ " successfully compiled")
 	  else begin
@@ -1611,16 +1640,16 @@ let main files =
   (* Command/Make Menu *)
   let make_f () =
     save_f ();
-    let c = Sys.command current.cmd_make in
-    !flash_info (current.cmd_make ^ if c = 0 then " succeeded" else " failed")
+    let c = Sys.command !current.cmd_make in
+    !flash_info (!current.cmd_make ^ if c = 0 then " succeeded" else " failed")
   in
   let make_m = commands_factory#add_item "_Make" ~callback:make_f in
   
   (* Command/CoqMakefile Menu*)
   let coq_makefile_f () =
-    let c = Sys.command current.cmd_coqmakefile in
+    let c = Sys.command !current.cmd_coqmakefile in
     !flash_info 
-      (current.cmd_coqmakefile ^ if c = 0 then " succeeded" else " failed")
+      (!current.cmd_coqmakefile ^ if c = 0 then " succeeded" else " failed")
   in
   let _ = commands_factory#add_item "_Make Makefile" ~callback:coq_makefile_f 
   in
@@ -1628,9 +1657,9 @@ let main files =
   (* Configuration Menu *)
   let reset_revert_timer () =
     disconnect_revert_timer ();
-    if current.global_auto_revert then 
+    if !current.global_auto_revert then 
       revert_timer := Some
-	(GMain.Timeout.add ~ms:current.global_auto_revert_delay 
+	(GMain.Timeout.add ~ms:!current.global_auto_revert_delay 
 	   ~callback:(fun () -> revert_f ();true))
   in reset_revert_timer (); (* to enable statup preferences timer *)
 
@@ -1658,10 +1687,26 @@ let main files =
   font_selector#selection#set_preview_text 
     "Lemma Truth: (p:Prover) `p < Coq`. Proof. Auto with *. Save."; 
   let customize_fonts_m = 
-    configuration_factory#add_item "Customize fonts"
+    configuration_factory#add_item "Customize _fonts"
       ~callback:(fun () -> font_selector#present ())
   in
 
+  let detach_menu = configuration_factory#add_item 
+		      "_Detach Scripting Window"
+		      ~callback:
+		      (fun () -> 
+			 let nb = notebook () in
+			 if nb#misc#toplevel#get_oid = w#coerce#get_oid then 
+			   begin  
+			     let nw = GWindow.window ~show:true () in
+			     let parent = out_some nb#misc#parent in
+			     ignore (nw#connect#destroy 
+				       ~callback:
+				       (fun () -> nb#misc#reparent parent));
+			     nw#add_accel_group accel_group;
+			     nb#misc#reparent nw#coerce
+			   end	      )
+  in
   (* Help Menu *)
 
   let help_menu = factory#add_submenu "_Help" in
@@ -1669,9 +1714,9 @@ let main files =
 		       ~accel_modi:[]
 		       ~accel_group in
   let _ = help_factory#add_item "Browse Coq _Manual" 
-	    ~callback:(fun () -> browse (current.doc_url ^ "main.html")) in
+	    ~callback:(fun () -> browse (!current.doc_url ^ "main.html")) in
   let _ = help_factory#add_item "Browse Coq _Library" 
-	    ~callback:(fun () -> browse current.library_url) in
+	    ~callback:(fun () -> browse !current.library_url) in
   let _ = 
     help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1
       ~callback:(fun () -> 
@@ -1692,7 +1737,9 @@ let main files =
   (* Window layout *)
 
   let hb = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () in
-  _notebook := Some (GPack.notebook ~scrollable:true ~packing:hb#add1 ());
+  _notebook := Some (GPack.notebook ~scrollable:true 
+		       ~packing:hb#add1
+		       ());
   let nb = notebook () in
   let fr2 = GBin.frame ~shadow_type:`ETCHED_OUT ~packing:hb#add2 () in 
   let hb2 = GPack.paned `VERTICAL  ~border_width:3 ~packing:fr2#add () in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 6373e5a344..bca97c7a72 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -58,15 +58,17 @@ let try_export file_name s =
       if (fst (Glib.Convert.get_charset ())) then
 	s 
       else
-	(try Glib.Convert.locale_from_utf8 s with _ -> prerr_endline "Warning: exporting to utf8";s)
+	(try Glib.Convert.locale_from_utf8 s 
+	 with _ -> prerr_endline "Warning: exporting to utf8";s)
     in
     let oc = open_out file_name in
     output_string oc s;
-    close_out oc
-  with e -> prerr_endline (Printexc.to_string e)
+    close_out oc;
+    true
+  with e -> prerr_endline (Printexc.to_string e);false
 
 let browse url =
-  let l,r = current.cmd_browse in
+  let l,r = !current.cmd_browse in
   ignore (Sys.command (l ^ url ^ r))
 
 let url_for_keyword =
@@ -92,7 +94,7 @@ let url_for_keyword =
 
 let browse_keyword text = 
   try 
-    let u = url_for_keyword text in browse (current.doc_url ^ u) 
+    let u = url_for_keyword text in browse (!current.doc_url ^ u) 
   with _ -> ()
 
 let my_stat f = try Some (Unix.stat f) with _ -> None
diff --git a/ide/preferences.ml b/ide/preferences.ml
index bbd1d062b2..51c7a025cc 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -69,6 +69,8 @@ type pref =
 let save_pref p =
   try 
     let fd = open_out pref_file in
+    output_value fd p;
+(*
     let output_string f c = fprintf fd "%s = \"%s\"\n" f c in
     let output_bool f c = fprintf fd "%s = \"%b\"\n" f c in
     let output_int f c = fprintf fd "%s = \"%d\"\n" f c in
@@ -77,8 +79,8 @@ let save_pref p =
 	(fun c -> 
 	   List.iter
 	   (fun x -> fprintf c "%a;" to_string x)) l in
-    let output_modi fd m = fprintf fd "%s" (mod_to_str m) 
-    in 
+    let output_modi fd m = fprintf fd "%s" (mod_to_str m) in
+    let output_tactics fd (m1,m2) = fprintf fd "%s,%s" m1 m2 in
     output_string "cmd_coqc" p.cmd_coqc;
     output_string "cmd_make" p.cmd_make;
     output_string "cmd_coqmakefile" p.cmd_coqmakefile;
@@ -114,12 +116,17 @@ let save_pref p =
       "modifiers_valid" 
       output_modi 
       p.modifiers_valid;
-
+   output_list 
+     "automatic_tactics" 
+     output_tactics
+     p.automatic_tactics;
+*)
     close_out fd
+
   with _ -> prerr_endline "Could not save preferences."
   
-let (current:pref) = 
-  {
+let (current:pref ref) = 
+  ref {
     cmd_coqc = "coqc";
     cmd_make = "make";
     cmd_coqmakefile = "coq_makefile -o Makefile *.v";
@@ -134,7 +141,13 @@ let (current:pref) =
     auto_save_delay = 10000;
     auto_save_name = "#","#";
 
-    automatic_tactics = [];
+    automatic_tactics = ["Progress Trivial.\n","Trivial.\n";
+			 "Progress Auto.\n","Auto.\n";
+			 "Tauto.\n","Tauto.\n";
+			 "Omega.\n","Omega.\n";
+			 "Progress Auto with *.\n","Auto with *.\n";
+			 "Progress Intuition.\n","Intuition.\n";
+			];
     
     modifier_for_navigation = [`CONTROL; `MOD1];
     modifier_for_templates = [`MOD4];
@@ -150,7 +163,7 @@ let (current:pref) =
 
 let load_pref p = 
   try 
-    let l = Config_lexer.get_config pref_file in
+(*    let l = Config_lexer.get_config pref_file in
     List.iter 
       (function k,v -> try match k with
 	 | "cmd_coqc" -> p.cmd_coqc <- v
@@ -190,71 +203,115 @@ let load_pref p =
 	 | "modifiers_valid" ->
 	     p.modifiers_valid <- 
 	     List.rev_map str_to_mod (Config_lexer.split v)
+	 | "automatic_tactics" ->
+	     p.automatic_tactics <- 
+	     List.map (fun x -> Pervasives.prerr_endline x;(x,"")) (Config_lexer.split v)
 	 | _ -> prerr_endline ("Warning: unknown option "^k)
        with _ -> ())
       l
+*)
+    let cin = open_in pref_file in
+    let (new_pref:pref) = input_value cin in
+    close_in cin;
+    current := new_pref
   with _ -> prerr_endline "Could not load preferences."
 
 let configure () = 
   let cmd_coqc = 
-    string ~f:(fun s -> current.cmd_coqc <- s) "coqc"  current.cmd_coqc in
-  let cmd_make = string ~f:(fun s -> current.cmd_make <- s)
-		   "make" current.cmd_make in
-  let cmd_coqmakefile = string ~f:(fun s -> current.cmd_coqmakefile <- s)
-			  "coqmakefile" current.cmd_coqmakefile in
-  let cmd_coqdoc = string ~f:(fun s -> current.cmd_coqdoc <- s)
-		     "coqdoc" current.cmd_coqdoc in
-  let cmd_print = string ~f:(fun s -> current.cmd_print <- s) 
-		    "Print ps" current.cmd_print in
+    string ~f:(fun s -> !current.cmd_coqc <- s) "coqc"  !current.cmd_coqc in
+  let cmd_make = string ~f:(fun s -> !current.cmd_make <- s)
+		   "make" !current.cmd_make in
+  let cmd_coqmakefile = string ~f:(fun s -> !current.cmd_coqmakefile <- s)
+			  "coqmakefile" !current.cmd_coqmakefile in
+  let cmd_coqdoc = string ~f:(fun s -> !current.cmd_coqdoc <- s)
+		     "coqdoc" !current.cmd_coqdoc in
+  let cmd_print = string ~f:(fun s -> !current.cmd_print <- s) 
+		    "Print ps" !current.cmd_print in
 
   let global_auto_revert = 
     bool 
-      ~f:(fun s -> current.global_auto_revert <- s) 
-      "Enable global auto revert" current.global_auto_revert
+      ~f:(fun s -> !current.global_auto_revert <- s) 
+      "Enable global auto revert" !current.global_auto_revert
   in
   let global_auto_revert_delay =
     string
-    ~f:(fun s -> current.global_auto_revert_delay <- 
+    ~f:(fun s -> !current.global_auto_revert_delay <- 
 	  (try int_of_string s with _ -> 10000)) 
       "Global auto revert delay (ms)" 
-      (string_of_int current.global_auto_revert_delay)
+      (string_of_int !current.global_auto_revert_delay)
   in  
 
   let modifier_for_tactics = 
     modifiers
-      ~allow:current.modifiers_valid
-      ~f:(fun l -> current.modifier_for_tactics <- l)
+      ~allow:!current.modifiers_valid
+      ~f:(fun l -> !current.modifier_for_tactics <- l)
       "Modifiers for Tactics Menu"
-      current.modifier_for_tactics
+      !current.modifier_for_tactics
   in
   let modifier_for_templates = 
     modifiers
-      ~allow:current.modifiers_valid
-      ~f:(fun l -> current.modifier_for_templates <- l)
+      ~allow:!current.modifiers_valid
+      ~f:(fun l -> !current.modifier_for_templates <- l)
       "Modifiers for Templates Menu"
-      current.modifier_for_templates
+      !current.modifier_for_templates
   in
   let modifier_for_navigation = 
     modifiers
-      ~allow:current.modifiers_valid
-      ~f:(fun l -> current.modifier_for_navigation <- l)
+      ~allow:!current.modifiers_valid
+      ~f:(fun l -> !current.modifier_for_navigation <- l)
       "Modifiers for Navigation Menu"
-      current.modifier_for_navigation
+      !current.modifier_for_navigation
   in
   let modifiers_valid = 
     modifiers
-      ~f:(fun l -> current.modifiers_valid <- l)
+      ~f:(fun l -> !current.modifiers_valid <- l)
       "Allowed modifiers"
-      current.modifiers_valid
+      !current.modifiers_valid
+  in
+
+  let cmd_browse = 
+    string
+      ~f:(fun s -> 
+	    !current.cmd_browse <- 
+	    try 
+	      let i = String.index s '%' in
+	      let pre = (String.sub s 0 i) in
+	      if String.length s - 1 = i then 
+		pre,""
+	      else
+		let post = String.sub s (i+2) (String.length s - i - 2) in
+		prerr_endline pre;
+		prerr_endline post;
+		pre,post
+	    with Not_found -> s,""
+	    )
+      "Browse command (%s for url)" 
+      ((fst !current.cmd_browse)^"%s"^(snd !current.cmd_browse))
+  in    
+  let doc_url = 
+    string ~f:(fun s -> !current.doc_url <- s) "Documentation URL"  !current.doc_url in
+  let library_url = 
+    string ~f:(fun s -> !current.library_url <- s) "Library URL"  !current.library_url in
+
+  let automatic_tactics = 
+    list 
+      ~titles:["Coq Command to try";"Coq Command to insert in script"]
+      "Wizzard tactics to apply"
+      (fun (c,i) -> [c;i])
+      !current.automatic_tactics
   in
   let cmds =
     [Section("Commands",
 	     [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print]);
      Section("Files",
 	     [global_auto_revert;global_auto_revert_delay]);
+     Section("Browser",
+	     [cmd_browse;doc_url;library_url]);
+     Section("Tactics Wizzard",
+	     [automatic_tactics]);
      Section("Shortcuts(need restart)",
 	     [modifiers_valid; modifier_for_tactics;modifier_for_templates; modifier_for_navigation])]
   in
   match edit "Customizations" cmds
-  with | Return_apply | Return_ok -> save_pref current
+  with | Return_apply | Return_ok -> save_pref !current
     | Return_cancel -> ()