diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/command_windows.ml | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 40 | ||||
| -rw-r--r-- | ide/preferences.ml | 13 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 |
4 files changed, 42 insertions, 15 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index dfd83e695..3f773b79c 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -26,7 +26,7 @@ class command_window () = let window = GWindow.window ~allow_grow:true ~allow_shrink:true ~width:320 ~height:200 - ~title:"CoqIde Commands" ~show:false () + ~title:"CoqIde queries" ~show:false () in let accel_group = GtkData.AccelGroup.create () in let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in diff --git a/ide/coqide.ml b/ide/coqide.ml index bdaa9c757..3b1b6c2e0 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -164,7 +164,9 @@ object('self) method active_keypress_handler : GdkEvent.Key.t -> bool method backtrack_to : GText.iter -> unit method backtrack_to_no_lock : GText.iter -> unit +(* method backtrack_to_insert : unit +*) method clear_message : unit method deactivate : unit -> unit method disconnected_keypress_handler : GdkEvent.Key.t -> bool @@ -173,6 +175,7 @@ object('self) GText.iter -> (GText.iter * GText.iter) option method get_insert : GText.iter method get_start_of_input : GText.iter + method go_to_insert : unit method indent_current_line : unit method insert_command : string -> string -> unit method insert_commands : (string * string) list -> unit @@ -180,7 +183,9 @@ object('self) method insert_this_phrase_on_success : bool -> bool -> bool -> string -> string -> bool method process_next_phrase : bool -> bool -> bool +(* method process_until_insert_or_error : unit +*) method process_until_iter_or_error : GText.iter -> unit method process_until_end_or_error : unit method recenter_insert : unit @@ -1182,9 +1187,11 @@ object(self) method process_until_end_or_error = self#process_until_iter_or_error input_buffer#end_iter +(* method process_until_insert_or_error = let stop = self#get_insert in self#process_until_iter_or_error stop +*) method reset_initial = Stack.iter @@ -1273,9 +1280,16 @@ Please restart and report NOW."; !pop_info ()) else prerr_endline "backtrack_to : discarded (lock is busy)" +(* method backtrack_to_insert = self#backtrack_to self#get_insert +*) + method go_to_insert = + let point = self#get_insert in + if point#compare self#get_start_of_input>=0 + then self#process_until_iter_or_error point + else self#backtrack_to point method undo_last_step = if Mutex.try_lock coq_may_stop then @@ -2146,6 +2160,7 @@ let main files = ~key:GdkKeysyms._Up ~callback:(do_or_activate (fun a -> a#undo_last_step)) `GO_UP; +(* add_to_menu_toolbar "_Forward to" ~tooltip:"Forward to" @@ -2158,6 +2173,13 @@ let main files = ~key:GdkKeysyms._Left ~callback:(do_or_activate (fun a-> a#backtrack_to_insert)) `GOTO_FIRST; +*) + add_to_menu_toolbar + "_Go to" + ~tooltip:"Go to" + ~key:GdkKeysyms._Right + ~callback:(do_or_activate (fun a-> a#go_to_insert)) + `GOTO_LAST; add_to_menu_toolbar "_Start" ~tooltip:"Start" @@ -2370,22 +2392,22 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ) Coq_commands.commands; - (* Commands Menu *) - let commands_menu = factory#add_submenu "_Commands" in - let commands_factory = new GMenu.factory commands_menu ~accel_group - ~accel_path:"<CoqIde MenuBar>/Commands" + (* Queries Menu *) + let queries_menu = factory#add_submenu "_Queries" in + let queries_factory = new GMenu.factory queries_menu ~accel_group + ~accel_path:"<CoqIde MenuBar>/Queries" ~accel_modi:[] in (* Command/Show commands *) - let commands_show_m = commands_factory#add_item - "_Show Window" + let queries_show_m = queries_factory#add_item + "_Show Query Window" ~key:GdkKeysyms._F12 ~callback:(Command_windows.command_window ()) #window#present in let _ = - commands_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2 + queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"SearchAbout" @@ -2393,7 +2415,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ()) in let _ = - commands_factory#add_item "_Check " ~key:GdkKeysyms._F3 + queries_factory#add_item "_Check " ~key:GdkKeysyms._F3 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Check" @@ -2401,7 +2423,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ()) in let _ = - commands_factory#add_item "_Print " ~key:GdkKeysyms._F4 + queries_factory#add_item "_Print " ~key:GdkKeysyms._F4 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Print" diff --git a/ide/preferences.ml b/ide/preferences.ml index 454333141..2bc92eeb5 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -90,8 +90,9 @@ type pref = mutable contextual_menus_on_goal : bool; mutable window_width : int; mutable window_height :int; +(* mutable use_utf8_notation : bool; - +*) mutable auto_complete : bool; } @@ -111,12 +112,12 @@ let (current:pref ref) = auto_save_name = "#","#"; encoding_use_locale = true; - encoding_use_utf8 = true; + encoding_use_utf8 = false; encoding_manual = "ISO_8859-1"; automatic_tactics = ["Progress Trivial.","Trivial."; - "Progress Auto.","Auto."; "Tauto.","Tauto."; + "Progress Auto.","Auto."; "Omega.","Omega."; "Progress Auto with *.","Auto with *."; "Progress Intuition.","Intuition."; @@ -139,8 +140,10 @@ let (current:pref ref) = contextual_menus_on_goal = true; window_width = 800; window_height = 600; - use_utf8_notation = true; - auto_complete = true +(* + use_utf8_notation = false; +*) + auto_complete = false } diff --git a/ide/preferences.mli b/ide/preferences.mli index ba5d693e9..5cf26c90e 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -45,7 +45,9 @@ type pref = mutable contextual_menus_on_goal : bool; mutable window_width : int; mutable window_height : int; +(* mutable use_utf8_notation : bool; +*) mutable auto_complete : bool; } |