From 2265dfad7543f0abce7e50751c650f8e5fb92683 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 29 Dec 2013 10:44:06 +0100 Subject: nanoPG: compete rewriting with more Emacs/PG like features It is not possible to add shortcuts with arbitrary modifiers and to save into a state some data, like the line offset for C-n and the killed text for C-k and C-y. If you see that your favorite Emacs/PG shortcut is missing, please tell me! Currently supported shortcuts: C-_ Undo C-g Esc C-s Search C-e Move to end of line M-e Move to end of sentence M-a Move to beginning of sentence C-n Move to next line C-p Move to previous line C-f Forward char C-b Backward char M-f Forward word M-b Backward word C-k Kill untill the end of line M-d Kill next word M-k Kill until sentence end M-DELBACK Kill word before cursor C-d Delete next character C-y Yank killed text back C-c C-RET Go to C-c C-n Advance 1 sentence C-c C-u Retract 1 sentence C-c C-b Advance C-c C-r Restart C-c C-c Stop C-c C-a C-p Print C-c C-a C-c Check C-c C-a C-b About C-c C-a C-a Search About C-c C-a C-o Search Pattern C-c C-a C-l Locate C-c C-a C-RET match template C-x C-s Save C-x C-c Quit C-x C-f Open --- ide/nanoPG.ml | 311 ++++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 218 insertions(+), 93 deletions(-) (limited to 'ide/nanoPG.ml') diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index fe9e815c9..a12ab7bd2 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -9,6 +9,10 @@ open Ideutils open Session open Preferences +open GdkKeysyms + +let eprintf x = + if !Flags.debug then Printf.eprintf x else Printf.ifprintf stderr x type gui = { notebook : session Wg_Notebook.typed_notebook; @@ -16,111 +20,232 @@ type gui = { } let actiong gui name = List.find (fun ag -> ag#name = name) gui.action_groups +let ct gui = gui.notebook#current_term -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 || 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")); - ] +type status = [ `Empty | `CnCu of int | `Kill of string * bool ] + +let pr_status = function + | `Empty -> "empty" + | `CnCu n -> Printf.sprintf "^n^u %d" n + | `Kill (s,b) -> Printf.sprintf "kill(%b) %S" b s + +type action = + | Action of string * string + | Callback of (gui -> unit) + | Edit of (status -> GSourceView2.source_buffer -> GText.iter -> status) + | Motion of (status -> GText.iter -> GText.iter * status) + +type 'c entry = { + mods : Gdk.Tags.modifier list; + key : Gdk.keysym; + keyname : string; + doc : string; + contents : 'c +} + +let mC = [`CONTROL] +let mM = [`MOD1] + +let mod_of t x = List.for_all (fun m -> List.mem m (GdkEvent.Key.state t)) x + +let pr_keymod l = + if l = mC then "C-" + else if l = mM then "M-" + else "" + +let mkE ?(mods=mC) key keyname doc contents = + { mods; key; keyname; doc; contents } + +type keypaths = Step of action entry list * keypaths entry list + +let print_keypaths kps = + let rec aux prefix (Step (l, konts)) = + String.concat "\n" ( + (List.map (fun x -> + prefix ^ pr_keymod x.mods ^ x.keyname ^ " " ^ x.doc ) l) @ + (List.map (fun x -> + aux (prefix^pr_keymod x.mods^x.keyname^" ") x.contents) konts)) in + aux " " kps + +let empty = Step([],[]) -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 +let frontier (Step(l1,l2)) = + List.map (fun x -> pr_keymod x.mods ^ x.keyname) l1 @ + List.map (fun x -> pr_keymod x.mods ^ x.keyname) l2 + +let insert kps name enter_syms bindings = + let rec aux kps enter_syms = + match enter_syms, kps with + | [], Step (el, konts) -> Step (bindings @ el, konts) + | (mods, key, keyname)::gs, Step (el, konts) -> + if List.exists (fun { key = k; mods = m } -> key = k && mods = m) konts + then + let konts = + List.map + (fun ({ key = k; contents } as x) -> + if key <> k then x else { x with contents = aux contents gs }) + konts in + Step(el,konts) + else + let kont = + { mods; key; keyname; doc = name; contents = aux empty gs } in + Step(el, kont::konts) in + aux kps enter_syms + +let run gui action status = + match action with + | Callback f -> f gui; status + | Action(group, name) -> + ((actiong gui group)#get_action name)#activate (); status + | Edit f -> + let b = (ct gui).script#source_buffer in + let i = b#get_iter_at_mark `INSERT in + f status b i + | Motion f -> + let b = (ct gui).script#source_buffer in + let i = b#get_iter_at_mark `INSERT in + let where, status = f status i in + b#place_cursor ~where; + status + +let emacs = empty + +let emacs = insert emacs "Emacs" [] [ + mkE _underscore "_" "Undo" (Action("Edit", "Undo")); + mkE _g "g" "Esc" (Callback(fun gui -> (ct gui).finder#hide ())); + mkE _s "s" "Search" (Callback(fun gui -> + if (ct gui).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)); + mkE _s "r" "Search backward" (Callback(fun gui -> + if (ct gui).finder#coerce#misc#visible then + ((actiong gui "Edit")#get_action "Find Previous")#activate () + else ((actiong gui "Edit")#get_action "Find")#activate ())); + mkE _e "e" "Move to end of line" (Motion(fun s i -> + (if not i#ends_line then i#forward_to_line_end else i), s)); + mkE _a "a" "Move to beginning of line" (Motion(fun s i -> + (i#set_line_offset 0), s)); + mkE ~mods:mM _e "e" "Move to end of sentence" (Motion(fun s i -> + i#forward_sentence_end, s)); + mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i -> + i#backward_sentence_start, s)); + mkE _n "n" "Move to next line" (Motion(fun s i -> + let orig_off = match s with `CnCu n -> n | _ -> i#line_offset in + let i = i#forward_line in + let new_off = min (i#chars_in_line - 1) orig_off in + (if new_off > 0 then i#set_line_offset new_off else i), `CnCu orig_off)); + mkE _p "p" "Move to previous line" (Motion(fun s i -> + let orig_off = match s with `CnCu n -> n | _ -> i#line_offset in + let i = i#backward_line in + let new_off = min (i#chars_in_line - 1) orig_off in + (if new_off > 0 then i#set_line_offset new_off else i), `CnCu orig_off)); + mkE _f "f" "Forward char" (Motion(fun s i -> i#forward_char, s)); + mkE _b "b" "Backward char" (Motion(fun s i -> i#backward_char, s)); + mkE ~mods:mM _f "f" "Forward word" (Motion(fun s i -> i#forward_word_end, s)); + mkE ~mods:mM _b "b" "Backward word" (Motion(fun s i -> + i#backward_word_start, s)); + mkE _k "k" "Kill untill the end of line" (Edit(fun s b i -> + let already_killed = match s with `Kill (k,true) -> k | _ -> "" in + let k = + if i#ends_line then begin + b#delete ~start:i ~stop:i#forward_char; "\n" + end else begin + let k = b#get_text ~start:i ~stop:i#forward_to_line_end () in + b#delete ~start:i ~stop:i#forward_to_line_end; k + end in + `Kill (already_killed ^ k,true))); + mkE ~mods:mM _d "d" "Kill next word" (Edit(fun s b i -> + let already_killed = match s with `Kill (k,true) -> k | _ -> "" in + let k = + let k = b#get_text ~start:i ~stop:i#forward_word_end () in + b#delete ~start:i ~stop:i#forward_word_end; k in + `Kill (already_killed ^ k,true))); + mkE ~mods:mM _k "k" "Kill until sentence end" (Edit(fun s b i -> + let already_killed = match s with `Kill (k,true) -> k | _ -> "" in + let k = + let k = b#get_text ~start:i ~stop:i#forward_sentence_end () in + b#delete ~start:i ~stop:i#forward_sentence_end; k in + `Kill (already_killed ^ k,true))); + mkE ~mods:mM _BackSpace "DELBACK" "Kill word before cursor" (Edit(fun s b i -> + let already_killed = match s with `Kill (k,true) -> k | _ -> "" in + let k = + let k = b#get_text ~start:i ~stop:i#backward_word_start () in + b#delete ~start:i ~stop:i#backward_word_start; k in + `Kill (already_killed ^ k,true))); + mkE _d "d" "Delete next character" (Edit(fun s b i -> + b#delete ~start:i ~stop:i#forward_char; s)); + mkE _y "y" "Yank killed text back " (Edit(fun s b i -> + let k, s = match s with `Kill (k,_) -> k, `Kill(k,false) | _ -> "", s in + b#insert ~iter:i k; + s)); ] -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 emacs = insert emacs "Emacs" [mC,_x,"x"] [ + mkE _s "s" "Save" (Action("File", "Save")); + mkE _c "c" "Quit" (Action("File", "Quit")); + mkE _f "f" "Open" (Action("File", "Open")); ] -let is_ctrl t = List.mem `CONTROL (GdkEvent.Key.state t) +let pg = insert emacs "Proof General" [mC,_c,"c"] [ + mkE _Return "RET" "Go to" (Action("Navigation", "Go to")); + mkE _n "n" "Advance 1 sentence" (Action("Navigation", "Forward")); + mkE _u "u" "Retract 1 sentence" (Action("Navigation", "Backward")); + mkE _b "b" "Advance" (Action("Navigation", "End")); + mkE _r "r" "Restart" (Action("Navigation", "Start")); + mkE _c "c" "Stop" (Action("Navigation", "Interrupt")); + ] -let documentation = ref "" +let command gui c = + let command = (ct gui).command in + let script = (ct gui).script in + let term = + let i, j = script#source_buffer#selection_bounds in + if i#equal j then None + else Some (script#buffer#get_text ~start:i ~stop:j ()) in + command#show; + command#new_query ~command:c ?term () + +let pg = insert pg "Proof General" [mC,_c,"c"; mC,_a,"a"] [ + mkE _p "p" "Print" (Callback (fun gui -> command gui "Print")); + mkE _c "c" "Check" (Callback (fun gui -> command gui "Check")); + mkE _b "b" "About" (Callback (fun gui -> command gui "About")); + mkE _a "a" "Search About" (Callback (fun gui -> command gui "SearchAbout")); + mkE _o "o" "Search Pattern" (Callback (fun gui->command gui "SearchPattern")); + mkE _l "l" "Locate" (Callback (fun gui -> command gui "Locate")); + mkE _Return "RET" "match template" (Action("Templates","match")); + ] + +let find gui (Step(here,konts)) t = + (* hack: ^c does copy in clipboard *) + let sel_nonempty () = + let i, j = (ct gui).script#source_buffer#selection_bounds in + not (i#equal j) in + let k = GdkEvent.Key.keyval t in + if k = _c && mod_of t mC && sel_nonempty () then + ignore(run gui (Action("Edit","Copy")) `Empty); + let cmp { key; mods } = key = k && mod_of t mods in + try `Do (List.find cmp here) with Not_found -> + try `Cont (List.find cmp konts).contents with Not_found -> `NotFound 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) - )); + let cur = ref pg in + let status = ref `Empty in + let reset () = cur := pg in 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 + if current.nanoPG then begin + match find gui !cur t with + | `Do e -> + eprintf "run (%s) %s on %s\n%!" e.keyname e.doc (pr_status !status); + status := run gui e.contents !status; reset (); true + | `Cont c -> + flash_info ("Waiting one of " ^ String.concat " " (frontier c)); + cur := c; true + | `NotFound -> reset (); false + end else false )); - documentation := doc + ignore(w#event#connect#button_press ~callback:(fun t -> reset (); false)) + + -let get_documentation () = !documentation +let get_documentation () = print_keypaths pg -- cgit v1.2.3