diff options
| -rw-r--r-- | ide/coqide.ml | 15 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 1 | ||||
| -rw-r--r-- | ide/ide.mllib | 1 | ||||
| -rw-r--r-- | ide/nanoPG.ml | 126 | ||||
| -rw-r--r-- | ide/preferences.ml | 8 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 |
6 files changed, 151 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 15a3d250c..0b6f9aa80 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -500,7 +500,7 @@ let update_status sn = | None -> "" | Some n -> ", proving " ^ n in - display ("Ready" ^ path ^ name); + display ("Ready"^ if current.nanoPG then ", [μPG]" else "" ^ path ^ name); Coq.return () in Coq.bind (Coq.status ~logger:sn.messages#push false) next @@ -955,6 +955,10 @@ let build_ui () = let compile_menu = GAction.action_group ~name:"Compile" () in let windows_menu = GAction.action_group ~name:"Windows" () in let help_menu = GAction.action_group ~name:"Help" () in + let all_menus = [ + file_menu; edit_menu; view_menu; export_menu; navigation_menu; tactics_menu; + templates_menu; tools_menu; queries_menu; compile_menu; windows_menu; + help_menu; ] in menu file_menu [ item "File" ~label:"_File"; @@ -1172,6 +1176,10 @@ let build_ui () = item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP ~callback:(fun _ -> on_current_term (fun sn -> browse_keyword sn.messages#add (get_current_word sn))); + item "Help for μPG mode" ~label:"Help for μPG mode" + ~callback:(fun _ -> on_current_term (fun sn -> + sn.messages#clear; + sn.messages#add (NanoPG.get_documentation ()))); item "About Coq" ~label:"_About" ~stock:`ABOUT ~callback:MiscMenu.about ]; @@ -1204,6 +1212,9 @@ let build_ui () = let toolbar = new GObj.widget tbar in let () = vbox#pack toolbar in + (* Emacs/PG mode *) + NanoPG.init w notebook all_menus; + (* Reset on tab switch *) let _ = notebook#connect#switch_page ~callback:(fun _ -> if prefs.reset_on_tab_switch then Nav.restart ()) @@ -1214,7 +1225,7 @@ let build_ui () = let () = refresh_notebook_pos () in let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in let () = lower_hbox#pack ~expand:true status#coerce in - let () = push_info "Ready" in + let () = push_info ("Ready"^ if current.nanoPG then ", [μPG]" else "") in (* Location display *) let l = GMisc.label diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index fd5bc6c49..ed8027959 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -141,6 +141,7 @@ let init () = <menuitem action='Browse Coq Manual' /> <menuitem action='Browse Coq Library' /> <menuitem action='Help for keyword' /> + <menuitem action='Help for μPG mode' /> <separator /> <menuitem name='Abt' action='About Coq' /> </menu> diff --git a/ide/ide.mllib b/ide/ide.mllib index fde206732..81e36763e 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -31,4 +31,5 @@ FileOps CoqOps Session Coqide_ui +NanoPG Coqide diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml new file mode 100644 index 000000000..dafb0575d --- /dev/null +++ b/ide/nanoPG.ml @@ -0,0 +1,126 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Ideutils +open Session +open Preferences + +type gui = { + notebook : session Wg_Notebook.typed_notebook; + action_groups : GAction.action_group list; +} + +let actiong gui name = List.find (fun ag -> ag#name = name) gui.action_groups + +let make_emacs_mode gui name enter_sym bindings = + let notebook = gui.notebook in + let bound k = List.mem_assoc k bindings in + let is_set, set, unset, mask = match enter_sym with + | None -> (fun () -> true), (fun _ -> false), (fun () -> ()), bound + | Some (k,_) -> let status = ref false in + let is_set () = !status in + let set ~dry_run k' = + if not (is_set ()) && k = k' then begin + if dry_run then true else begin + flash_info ("Waiting " ^name^" command: " ^ + String.concat " " (List.map (fun (_,(d,_,_)) ->"^"^d) bindings)); + status := true; true + end + end else false in + let unset () = status := false in + let mask k' = set ~dry_run:true k' || (is_set () && bound k') in + is_set, set ~dry_run:false, unset, mask in + let doc = + let prefix = + match enter_sym with + | None -> " " + | Some (_,k) -> " ^"^k in + name ^":\n"^ + String.concat "\n" + (List.map (fun (_,(k,doc,_)) -> prefix^"^"^k^" "^doc) bindings) in + let run k = if not (is_set ()) then false else try + let action = match Util.pi3 (List.assoc k bindings) with + | `Callback f -> f + | `Edit f -> (fun () -> + let b = notebook#current_term.script#source_buffer in + let i = b#get_iter_at_mark `INSERT in + f b i) + | `Motion f -> (fun () -> + let b = notebook#current_term.script#source_buffer in + let i = b#get_iter_at_mark `INSERT in + b#place_cursor ~where:(f i)) + | `Action(group,name) -> ((actiong gui group)#get_action name)#activate in + action (); + unset (); + true + with Not_found -> false in + run, set, unset, mask, doc + +let compile_emacs_modes gui l = + List.fold_left (fun (r,s,u,m,d) mode -> + let run, set, unset, mask,doc = mode gui in + (fun k -> r k || run k), (fun k -> s k or set k), + (fun () -> u (); unset ()), (fun k -> m k || mask k), d^"\n"^doc) + ((fun _ -> false),(fun _ -> false),(fun () -> ()),(fun _ -> false),"") l + +let pg_mode gui = make_emacs_mode gui "Proof General" (Some(GdkKeysyms._c,"c"))[ + GdkKeysyms._Return, ("RET", "Go to", `Action("Navigation", "Go to")); + GdkKeysyms._n, ("n", "Advance 1 sentence",`Action("Navigation", "Forward")); + GdkKeysyms._u, ("u", "Retract 1 sentence",`Action("Navigation", "Backward")); + GdkKeysyms._b, ("b", "Advance", `Action("Navigation", "End")); + GdkKeysyms._r, ("r", "Restart", `Action("Navigation", "Start")); + GdkKeysyms._c, ("c", "Stop", `Action("Navigation", "Interrupt")); + ] + +let std_mode gui = make_emacs_mode gui "Emacs" None [ + GdkKeysyms._underscore, ("_", "Undo", `Action("Edit", "Undo")); + GdkKeysyms._g, ("g", "Esc", `Callback(fun () -> + gui.notebook#current_term.finder#hide ())); + GdkKeysyms._s, ("s", "Search", `Callback(fun () -> + if gui.notebook#current_term.finder#coerce#misc#visible then + ((actiong gui "Edit")#get_action "Find Next")#activate () + else ((actiong gui "Edit")#get_action "Find")#activate ())); + GdkKeysyms._e, ("e", "Move to end of line", `Motion(fun i -> + i#forward_to_line_end)); + GdkKeysyms._a, ("a", "More to beginning of line", `Motion(fun i -> + i#backward_sentence_start)); + GdkKeysyms._n, ("n", "Move to next line", `Motion(fun i -> + i#forward_line#set_line_offset i#line_offset)); + GdkKeysyms._p, ("p", "Move to previous line", `Motion(fun i -> + i#backward_line#set_line_offset i#line_offset)); + GdkKeysyms._k, ("k", "Kill untill the end of line", `Edit(fun b i -> + b#delete ~start:i ~stop:i#forward_to_line_end)); + ] + +let std_xmode gui = make_emacs_mode gui "Emacs" (Some (GdkKeysyms._x,"x")) [ + GdkKeysyms._s, ("s", "Save", `Action("File", "Save")); + GdkKeysyms._c, ("c", "Quit", `Action("File", "Quit")); + ] + +let is_ctrl t = List.mem `CONTROL (GdkEvent.Key.state t) + +let documentation = ref "" + +let init w nb ags = + let gui = { notebook = nb; action_groups = ags } in + let emacs_run, emacs_set, emacs_unset, emacs_mask, doc = + compile_emacs_modes gui [std_xmode; pg_mode; std_mode] in + ignore(w#event#connect#key_release ~callback:(fun t -> + current.nanoPG && is_ctrl t && + emacs_mask (GdkEvent.Key.keyval t) + )); + ignore(w#event#connect#key_press ~callback:(fun t -> + if current.nanoPG && is_ctrl t then + let keyval = GdkEvent.Key.keyval t in + if emacs_run keyval then (emacs_unset (); true) + else emacs_set keyval + else false + )); + documentation := doc + +let get_documentation () = !documentation diff --git a/ide/preferences.ml b/ide/preferences.ml index 39eaccb52..b3ef96fd9 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -153,6 +153,8 @@ type pref = mutable tab_length : int; mutable highlight_current_line : bool; + mutable nanoPG : bool; + } let use_default_doc_url = "(automatic)" @@ -228,6 +230,8 @@ let current = { spaces_instead_of_tabs = true; tab_length = 2; highlight_current_line = false; + + nanoPG = false; } let save_pref () = @@ -295,6 +299,7 @@ let save_pref () = add "spaces_instead_of_tabs" [string_of_bool p.spaces_instead_of_tabs] ++ add "tab_length" [string_of_int p.tab_length] ++ add "highlight_current_line" [string_of_bool p.highlight_current_line] ++ + add "nanoPG" [string_of_bool p.nanoPG] ++ Config_lexer.print_file pref_file let load_pref () = @@ -378,6 +383,7 @@ let load_pref () = set_bool "spaces_instead_of_tabs" (fun v -> np.spaces_instead_of_tabs <- v); set_int "tab_length" (fun v -> np.tab_length <- v); set_bool "highlight_current_line" (fun v -> np.highlight_current_line <- v); + set_bool "nanoPG" (fun v -> np.nanoPG <- v); () let configure ?(apply=(fun () -> ())) () = @@ -520,6 +526,7 @@ let configure ?(apply=(fun () -> ())) () = gen_button "Highlight current line" current.highlight_current_line in + let nanoPG = gen_button "Emacs/PG keybindings (μPG mode)" current.nanoPG in (* let lbox = GPack.hbox ~packing:box#pack () in *) (* let _ = GMisc.label ~text:"Tab width" *) (* ~xalign:0. *) @@ -536,6 +543,7 @@ let configure ?(apply=(fun () -> ())) () = current.show_right_margin <- show_right_margin#active; current.spaces_instead_of_tabs <- spaces_instead_of_tabs#active; current.highlight_current_line <- highlight_current_line#active; + current.nanoPG <- nanoPG#active; current.auto_complete <- auto_complete#active; (* current.tab_length <- tab_width#value_as_int; *) !refresh_editor_hook () diff --git a/ide/preferences.mli b/ide/preferences.mli index 10f1ea827..0c5b7f6e1 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -80,6 +80,8 @@ type pref = mutable tab_length : int; mutable highlight_current_line : bool; + mutable nanoPG : bool; + } val save_pref : unit -> unit |