diff options
author | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-24 14:10:14 +0000 |
---|---|---|
committer | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-24 14:10:14 +0000 |
commit | 6e2117c0e8aed0f6921664582c9dc6e99c0f97c6 (patch) | |
tree | 320782d897eed637b116b06119b54420bce982b6 | |
parent | 069e8967b593f43fd75ea678676ae9b958fe5fae (diff) |
ide changes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3694 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile | 6 | ||||
-rw-r--r-- | ide/coqide.ml | 10 | ||||
-rw-r--r-- | ide/preferences.ml | 33 |
3 files changed, 43 insertions, 6 deletions
@@ -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]; + } |