ide changes

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

3 files changed, 43 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index d7aa4c25f..b0be198ef 100644
--- a/Makefile
+++ b/Makefile
@@ -420,11 +420,15 @@ beforedepend:: scripts/tolink.ml
 
 COQIDEBYTE=bin/coqide.byte$(EXE)
 COQIDEOPT=bin/coqide.opt$(EXE)
+COQIDE=bin/coqide.$(BEST)$(EXE)
+
 COQIDECMO=ide/ideutils.cmo ide/find_phrase.cmo ide/highlight.cmo ide/coq.cmo ide/coqide.cmo
 COQIDECMX=$(COQIDECMO:.cmo=.cmx)
 COQIDEFLAGS=-I +lablgtk2
 beforedepend:: ide/find_phrase.ml ide/highlight.ml
 
+ide: $(COQIDE)
+
 $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX)
 	$(COQMKTOP) -ide -opt $(COQIDEFLAGS) lablgtk.cmxa $(OPTFLAGS) -o $@ $(COQIDECMX)
 	$(STRIP) $@
@@ -880,7 +884,7 @@ install-opt:
 
 install-binaries:
 	$(MKDIR) $(FULLBINDIR)
-	cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(COQVO2XML) $(FULLBINDIR)
+	cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(COQVO2XML) $(COQIDE) $(FULLBINDIR)
 
 LIBFILES=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO)
 LIBFILESLIGHT=$(INITVO) $(THEORIESLIGHTVO)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5ef653f88..1614c905a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -208,7 +208,7 @@ let input_channel b ic =
   done
 
 let with_file name ~f =
-  let ic = open_in name in
+  let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
   try f ic; close_in ic with exn -> close_in ic; raise exn
 
 type info =  {start:GText.mark;
@@ -666,7 +666,6 @@ object(self)
 	  ~stop:self#get_start_of_input
 	  "processed";
 	input_buffer#move_mark ~where:start (`NAME "start_of_input");
-	input_buffer#place_cursor start;
 	(try self#show_goals with e -> ());
 	clear_stdout ();
 	self#clear_message
@@ -1035,7 +1034,7 @@ let main () =
     if has_something_to_save () then 
       match (GToolbox.question_box ~title:"Quit"
 	       ~buttons:["Save Named Buffers and Quit";
-			 "Don't Save and Quit";
+			 "Quit without Saving";
 			 "Don't Quit"] 
 	       ~default:0
 	       ~icon:
@@ -1151,7 +1150,10 @@ let main () =
   
   (* Templates Menu *)
   let templates_menu =  factory#add_submenu "Templates" in
-  let templates_factory = new GMenu.factory templates_menu ~accel_group ~accel_modi:[`MOD1] in
+  let templates_factory = new GMenu.factory templates_menu 
+			    ~accel_group 
+			    ~accel_modi:[`MOD1] 
+  in
   let templates_tactics = templates_factory#add_submenu "Tactics" in
   let templates_tactics_factory = new GMenu.factory templates_tactics ~accel_group in
   ignore (templates_tactics_factory#add_item "Auto");
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 624bed0a7..2702854e2 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -3,10 +3,41 @@ type pref =
       mutable cmd_coqc : string;
       mutable cmd_coqmakefile : string;
       mutable cmd_coqdoc : string;
+
       mutable global_auto_revert : bool;
       mutable global_auto_revert_delay : float;
+
       mutable auto_save : bool;
       mutable auto_save_delay : float;
+      mutable auto_save_name : string*string;
+
       mutable automatic_tactics : string * string list;
-      mutable cmd_print : string
+      mutable cmd_print : string;
+
+      mutable modifier_for_navigation : Gdk.Tags.modifier list;
+      mutable modifier_for_templates : Gdk.Tags.modifier list;
+      
+
     }
+
+
+let (current:pref) = 
+  {
+    cmd_coqc = "coqc";
+    cmd_coqmakefile = "coqmakefile";
+    cmd_coqdoc = "coqdoc";
+    cmd_print = "lpr";
+    
+
+    global_auto_revert = false;
+    global_auto_revert_delay = 1.;
+    
+    auto_save = false;
+    auto_save_delay = 1.;
+    auto_save_name = "#","#";
+
+    automatic_tactics = [];
+    
+    modifier_for_navigation = [`CONTROL; `MOD1];
+    modifier_for_templates = [`MOD1];
+  }