From a63ac0351d6feb3f3242649faccf88da6a34d5eb Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 12:15:59 +0200 Subject: Fix a nanoPG bug: was accepting unexpectedly extra modifier keys pressed. For instance, Ctrl-Meta-e was behaving like Ctrl-e. --- ide/nanoPG.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index d85d87142c..de386e4ccf 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -67,7 +67,10 @@ type 'c entry = { 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 mod_of t x = + let y = GdkEvent.Key.state t in + List.for_all (fun m -> List.mem m y) x && + List.for_all (fun m -> List.mem m x) y let pr_keymod l = if l = mC then "C-" -- cgit v1.2.3 From 714d745858b031e58c5d089799d017eb092543c0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 12:43:35 +0200 Subject: NanoPG: expanding the notation C- and M- to Ctrl- and Meta-. Not only will this be clearer but it prepares to describing action on MacOS which shall use Cmd and which cannot be abbreviated w/o introducing a confusion with the abbreviation C- of Control-. --- ide/nanoPG.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index de386e4ccf..89bf07ce23 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -73,8 +73,8 @@ let mod_of t x = List.for_all (fun m -> List.mem m x) y let pr_keymod l = - if l = mC then "C-" - else if l = mM then "M-" + if l = mC then "Ctrl-" + else if l = mM then "Meta-" else "" let mkE ?(mods=mC) key keyname doc ?(alias=[]) contents = -- cgit v1.2.3 From dda4e65e530bd0e4a3ada165fdc752e1a217da8b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 12:18:17 +0200 Subject: CoqIDE: Adding MacOS X support for Meta-based nano-PG keys. In practice, most of Alt modified keys are used on MacOS X keyboards for special characters and many Command modified keys are used for MacOS standard actions. So, we propose to use Ctrl-Command- as a prefix for the Meta-based nano-PG shortcuts. E.g. Ctrl-Command-e would go the end of the sentence. --- ide/nanoPG.ml | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 89bf07ce23..0cb39c8d75 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -65,7 +65,13 @@ type 'c entry = { } let mC = [`CONTROL] -let mM = [`MOD1] +let mM = + if Coq_config.arch = "Darwin" then + (* We add both MOD2 and META because both are + returned when pressing Command on MacOS X *) + [`CONTROL;`MOD2;`META] + else + [`MOD1] let mod_of t x = let y = GdkEvent.Key.state t in @@ -73,9 +79,13 @@ let mod_of t x = List.for_all (fun m -> List.mem m x) y let pr_keymod l = - if l = mC then "Ctrl-" - else if l = mM then "Meta-" - else "" + if l = mC then + "Ctrl-" + else + if l = mM then + if Coq_config.arch = "Darwin" then "Ctrl-Cmd-" else "Meta-" + else + "" let mkE ?(mods=mC) key keyname doc ?(alias=[]) contents = List.map (fun (mods, key, keyname) -> { mods; key; keyname; doc; contents }) -- cgit v1.2.3 From 523fc765d1363767ffb6970781767dfcdca6892c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 12:29:38 +0200 Subject: Cosmetic in nanoPG.ml: fixing a wrong indentation. --- ide/nanoPG.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 0cb39c8d75..70f2a71db2 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -299,9 +299,9 @@ let find gui (Step(here,konts)) t = else if k = _c && mod_of t mC && sel_nonempty () then ignore(run t 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 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 -- cgit v1.2.3 From d42c059d6c7877948fdae76bf0400d4e3b06b90d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 12:29:49 +0200 Subject: NanoPG doc: telling that char, word, sentence, line have their unicode meaning. More precisely, GTK+ uses Pango rules which follows the standard Unicode text segmentation rules (see http://www.unicode.org/reports/tr29/). --- ide/nanoPG.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 70f2a71db2..435076c332 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -333,4 +333,6 @@ let init w nb ags = -let get_documentation () = print_keypaths pg +let get_documentation () = + "Chars, words, lines and sentences below pertain to standard unicode segmentation rules\n" ^ + print_keypaths pg -- cgit v1.2.3 From bae9b53c58d995a0cce404c279c37206e5418d2f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 12:38:05 +0200 Subject: CoqIDE nanoPG: adding keys to go the start/end of file (w/o evaluating). On MacOS X: Ctrl-Cmd-Left and Ctrl-Cmd-Right Elsewhere: Meta-Left and Meta-Right See issue #9899 (moving cursor to beginning and end of file). --- ide/nanoPG.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 435076c332..5e6c0b8462 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -160,6 +160,13 @@ let emacs = insert emacs "Emacs" [] [ 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 with move = None })); + mkE ~mods:mM _Right "->" "Move to end of buffer" (Motion(fun s i -> + i#forward_to_end, + { s with move = None })); + mkE ~mods:mM _Left "<-" "Move to start of buffer" (Motion(fun s i -> + let buffer = new GText.buffer i#buffer in + buffer#start_iter, + { s with move = None })); mkE _a "a" "Move to beginning of line" (Motion(fun s i -> (i#set_line_offset 0), { s with move = None })); mkE ~mods:mM _e "e" "Move to end of sentence" (Motion(fun s i -> -- cgit v1.2.3 From 7d3e6fefd7dab20c433fb7ae1baec5fa3ff2f0d7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 12:56:30 +0200 Subject: CoqIDE: updating documentation of the Preference windows. In particular, we explicitly mention the existence of an Emacs mode. --- doc/sphinx/practical-tools/coqide.rst | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 97d86943fb..d3d75dddd8 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -181,7 +181,14 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second section is devoted to file management: you may configure +The second and third sections are for controlling colors and style. + +The fourth section is for customizing the editor. It includes in +particular the ability to activate an Emacs mode named +micro-Proof-General (use the Help menu to know more about the +available bindings). + +The next section is devoted to file management: you may configure automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a -- cgit v1.2.3 From d911384de18874b98c20bf25e444f1d356af4249 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 27 Apr 2019 13:28:37 +0200 Subject: Renaming nanoPG to microPG. This is to be consistent with what the preference panel displays (namely μpG). We keep the nanoPG name in the preference file by compatibility. --- ide/coqide.ml | 8 +- ide/ide.mllib | 2 +- ide/microPG.ml | 345 ++++++++++++++++++++++++++++++++++++++++++++++++++++ ide/microPG.mli | 13 ++ ide/nanoPG.ml | 345 ---------------------------------------------------- ide/nanoPG.mli | 13 -- ide/preferences.ml | 5 +- ide/preferences.mli | 2 +- 8 files changed, 367 insertions(+), 366 deletions(-) create mode 100644 ide/microPG.ml create mode 100644 ide/microPG.mli delete mode 100644 ide/nanoPG.ml delete mode 100644 ide/nanoPG.mli diff --git a/ide/coqide.ml b/ide/coqide.ml index aa9e150fd5..4f00be27a1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -561,7 +561,7 @@ let update_status sn = | None -> "" | Some n -> ", proving " ^ n in - display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name); + display ("Ready"^ (if microPG#get then ", [μPG]" else "") ^ path ^ name); Coq.return () in Coq.bind (Coq.status false) next @@ -1200,7 +1200,7 @@ let build_ui () = item "Help for μPG mode" ~label:"Help for μPG mode" ~callback:(fun _ -> on_current_term (fun sn -> sn.messages#default_route#clear; - sn.messages#default_route#add_string (NanoPG.get_documentation ()))); + sn.messages#default_route#add_string (MicroPG.get_documentation ()))); item "About Coq" ~label:"_About" ~stock:`ABOUT ~callback:MiscMenu.about ]; @@ -1234,7 +1234,7 @@ let build_ui () = let () = vbox#pack toolbar#coerce in (* Emacs/PG mode *) - NanoPG.init w notebook all_menus; + MicroPG.init w notebook all_menus; (* On tab switch, reset, update location *) let _ = notebook#connect#switch_page ~callback:(fun n -> @@ -1251,7 +1251,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"^ if nanoPG#get then ", [μPG]" else "") in + let () = push_info ("Ready"^ if microPG#get then ", [μPG]" else "") in (* Location display *) let l = GMisc.label diff --git a/ide/ide.mllib b/ide/ide.mllib index ed6520f29f..f8e8ff48d6 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -30,5 +30,5 @@ CoqOps Wg_Command Session Coqide_ui -NanoPG +MicroPG Coqide diff --git a/ide/microPG.ml b/ide/microPG.ml new file mode 100644 index 0000000000..25cab4638c --- /dev/null +++ b/ide/microPG.ml @@ -0,0 +1,345 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* ag#name = name) gui.action_groups +let ct gui = gui.notebook#current_term + +let get_sel b = b#selection_bounds +let sel_nonempty b = let i, j = get_sel b in not (i#equal j) +let get_sel_txt b = let i, j = get_sel b in i#get_text ~stop:j + +type status = { move : int option; kill : (string * bool) option; sel: bool } + +let pr_status { move; kill; sel } = + let move = Option.cata (fun i -> string_of_int i) "" move in + let kill = Option.cata (fun (s,b) -> sprintf "kill(%b) %S" b s) "" kill in + let sel = string_of_bool sel in + Printf.sprintf "{ move: %s; kill: %s; sel: %s }" move kill sel +let pr_key t = + let kv = GdkEvent.Key.keyval t in + let str = GdkEvent.Key.string t in + let str_of_mod = function + | `SHIFT -> "SHIFT" | `LOCK -> "LOCK" | `CONTROL -> "CONTROL" + | `MOD1 -> "MOD1" | `MOD2 -> "MOD2" | `MOD3 -> "MOD3" | `MOD4 -> "MOD4" + | `MOD5 -> "MOD5" | `BUTTON1 -> "BUTTON1" | `BUTTON2 -> "BUTTON2" + | `BUTTON3 -> "BUTTON3" | `BUTTON4 -> "BUTTON4" | `BUTTON5 -> "BUTTON5" + | `SUPER -> "SUPER" | `HYPER -> "HYPER" | `META -> "META" + | `RELEASE -> "RELEASE" in + let mods = String.concat " " (List.map str_of_mod (GdkEvent.Key.state t)) in + Printf.sprintf "'%s' (%d, %s)" str kv mods + +type action = + | Action of string * string + | Callback of (gui -> unit) + | Edit of (status -> GSourceView3.source_buffer -> GText.iter -> + (string -> string -> unit) -> 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 = + if Coq_config.arch = "Darwin" then + (* We add both MOD2 and META because both are + returned when pressing Command on MacOS X *) + [`CONTROL;`MOD2;`META] + else + [`MOD1] + +let mod_of t x = + let y = GdkEvent.Key.state t in + List.for_all (fun m -> List.mem m y) x && + List.for_all (fun m -> List.mem m x) y + +let pr_keymod l = + if l = mC then + "Ctrl-" + else + if l = mM then + if Coq_config.arch = "Darwin" then "Ctrl-Cmd-" else "Meta-" + else + "" + +let mkE ?(mods=mC) key keyname doc ?(alias=[]) contents = + List.map (fun (mods, key, keyname) -> { mods; key; keyname; doc; contents }) + ((mods, key, keyname)::alias) + +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 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 (List.flatten 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_action gui group name = + ((actiong gui group)#get_action name)#activate () + +let run key gui action status = + match action with + | Callback f -> f gui; status + | Action(group, name) -> run_action gui group name; status + | Edit f -> + let b = (ct gui).script#source_buffer in + let i = b#get_iter_at_mark `INSERT in + let status = f status b i (run_action gui) in + if not status.sel then + b#place_cursor ~where:(b#get_iter_at_mark `SEL_BOUND); + status + | Motion f -> + let b, script = (ct gui).script#source_buffer, (ct gui).script in + let sel_mode = status.sel || List.mem `SHIFT (GdkEvent.Key.state key) in + let i = + if sel_mode then b#get_iter_at_mark `SEL_BOUND + else b#get_iter_at_mark `INSERT in + let where, status = f status i in + let sel_mode = status.sel || List.mem `SHIFT (GdkEvent.Key.state key) in + if sel_mode then (b#move_mark `SEL_BOUND ~where; script#scroll_mark_onscreen `SEL_BOUND) + else (b#place_cursor ~where; script#scroll_mark_onscreen `INSERT); + status + +let emacs = empty + +let emacs = insert emacs "Emacs" [] [ + (* motion *) + 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 with move = None })); + mkE ~mods:mM _Right "->" "Move to end of buffer" (Motion(fun s i -> + i#forward_to_end, + { s with move = None })); + mkE ~mods:mM _Left "<-" "Move to start of buffer" (Motion(fun s i -> + let buffer = new GText.buffer i#buffer in + buffer#start_iter, + { s with move = None })); + mkE _a "a" "Move to beginning of line" (Motion(fun s i -> + (i#set_line_offset 0), { s with move = None })); + mkE ~mods:mM _e "e" "Move to end of sentence" (Motion(fun s i -> + i#forward_sentence_end, { s with move = None })); + mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i -> + i#backward_sentence_start, { s with move = None })); + mkE _n "n" "Move to next line" (Motion(fun s i -> + let orig_off = Option.default i#line_offset s.move 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), + { s with move = Some orig_off })); + mkE _p "p" "Move to previous line" (Motion(fun s i -> + let orig_off = Option.default i#line_offset s.move 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), + { s with move = Some orig_off })); + mkE _f "f" "Forward char" ~alias:[[],_Right,"RIGHT"] + (Motion(fun s i -> i#forward_char, { s with move = None })); + mkE _b "b" "Backward char" ~alias:[[],_Left,"LEFT"] + (Motion(fun s i -> i#backward_char, { s with move = None })); + mkE ~mods:mM _f "f" "Forward word" ~alias:[mC,_Right,"RIGHT"] + (Motion(fun s i -> i#forward_word_end, { s with move = None })); + mkE ~mods:mM _b "b" "Backward word" ~alias:[mC,_Left,"LEFT"] + (Motion(fun s i -> i#backward_word_start, { s with move = None })); + mkE _space "SPC" "Set mark" ~alias:[mC,_at,"@"] (Motion(fun s i -> + if s.sel = false then i, { s with sel = true } + else i, { s with sel = false } )); + (* edits *) + mkE ~mods:mM _w "w" "Copy selected region" (Edit(fun s b i run -> + if sel_nonempty b then + let txt = get_sel_txt b in + run "Edit" "Copy"; + { s with kill = Some(txt,false); sel = false } + else s)); + mkE _w "w" "Kill selected region" (Edit(fun s b i run -> + if sel_nonempty b then + let txt = get_sel_txt b in + run "Edit" "Cut"; + { s with kill = Some(txt,false); sel = false } + else s)); + mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ -> + let already_killed = match s.kill with Some (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 + { s with kill = Some (already_killed ^ k,true) })); + mkE ~mods:mM _d "d" "Kill next word" (Edit(fun s b i _ -> + let already_killed = match s.kill with Some (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 + { s with kill = Some (already_killed ^ k,true) })); + mkE ~mods:mM _k "k" "Kill until sentence end" (Edit(fun s b i _ -> + let already_killed = match s.kill with Some (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 + { s with kill = Some (already_killed ^ k,true) })); + mkE ~mods:mM _BackSpace "DELBACK" "Kill word before cursor" + (Edit(fun s b i _ -> + let already_killed = match s.kill with Some (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 + { s with kill = Some (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.kill with + | Some (k,_) -> k, { s with kill = Some (k,false) } + | _ -> "", s in + b#insert ~iter:i k; + s)); + (* misc *) + 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 run_action gui "Edit" "Find Next" + else run_action gui "Edit" "Find")); + mkE _s "r" "Search backward" (Callback(fun gui -> + if (ct gui).finder#coerce#misc#visible + then run_action gui "Edit" "Find Previous" + else run_action gui "Edit" "Find")); + ] + +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")); + mkE ~mods:[] _u "u" "Undo" (Action("Edit", "Undo")); + ] + +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 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 empty = { sel = false; kill = None; move = None } + +let find gui (Step(here,konts)) t = + (* hack: ^c does copy in clipboard *) + let sel_nonempty () = sel_nonempty (ct gui).script#source_buffer in + let k = GdkEvent.Key.keyval t in + if k = _x && mod_of t mC && sel_nonempty () then + ignore(run t gui (Action("Edit","Cut")) empty) + else + if k = _c && mod_of t mC && sel_nonempty () then + ignore(run t 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 cur = ref pg in + let status = ref empty in + let reset () = eprintf "reset\n%!"; cur := pg in + ignore(w#event#connect#key_press ~callback:(fun t -> + let on_current_term f = + let term = try Some nb#current_term with Invalid_argument _ -> None in + match term with None -> false | Some t -> f t + in + on_current_term (fun x -> + if x.script#misc#get_property "has-focus" <> `BOOL true + then false + else begin + eprintf "got key %s\n%!" (pr_key t); + if microPG#get 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 t 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 + end))); + ignore(w#event#connect#button_press ~callback:(fun t -> reset (); false)) + + + +let get_documentation () = + "Chars, words, lines and sentences below pertain to standard unicode segmentation rules\n" ^ + print_keypaths pg diff --git a/ide/microPG.mli b/ide/microPG.mli new file mode 100644 index 0000000000..bc9b39d823 --- /dev/null +++ b/ide/microPG.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* string +val init : GWindow.window -> Session.session Wg_Notebook.typed_notebook -> + GAction.action_group list -> unit diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml deleted file mode 100644 index 5e6c0b8462..0000000000 --- a/ide/nanoPG.ml +++ /dev/null @@ -1,345 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* ag#name = name) gui.action_groups -let ct gui = gui.notebook#current_term - -let get_sel b = b#selection_bounds -let sel_nonempty b = let i, j = get_sel b in not (i#equal j) -let get_sel_txt b = let i, j = get_sel b in i#get_text ~stop:j - -type status = { move : int option; kill : (string * bool) option; sel: bool } - -let pr_status { move; kill; sel } = - let move = Option.cata (fun i -> string_of_int i) "" move in - let kill = Option.cata (fun (s,b) -> sprintf "kill(%b) %S" b s) "" kill in - let sel = string_of_bool sel in - Printf.sprintf "{ move: %s; kill: %s; sel: %s }" move kill sel -let pr_key t = - let kv = GdkEvent.Key.keyval t in - let str = GdkEvent.Key.string t in - let str_of_mod = function - | `SHIFT -> "SHIFT" | `LOCK -> "LOCK" | `CONTROL -> "CONTROL" - | `MOD1 -> "MOD1" | `MOD2 -> "MOD2" | `MOD3 -> "MOD3" | `MOD4 -> "MOD4" - | `MOD5 -> "MOD5" | `BUTTON1 -> "BUTTON1" | `BUTTON2 -> "BUTTON2" - | `BUTTON3 -> "BUTTON3" | `BUTTON4 -> "BUTTON4" | `BUTTON5 -> "BUTTON5" - | `SUPER -> "SUPER" | `HYPER -> "HYPER" | `META -> "META" - | `RELEASE -> "RELEASE" in - let mods = String.concat " " (List.map str_of_mod (GdkEvent.Key.state t)) in - Printf.sprintf "'%s' (%d, %s)" str kv mods - -type action = - | Action of string * string - | Callback of (gui -> unit) - | Edit of (status -> GSourceView3.source_buffer -> GText.iter -> - (string -> string -> unit) -> 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 = - if Coq_config.arch = "Darwin" then - (* We add both MOD2 and META because both are - returned when pressing Command on MacOS X *) - [`CONTROL;`MOD2;`META] - else - [`MOD1] - -let mod_of t x = - let y = GdkEvent.Key.state t in - List.for_all (fun m -> List.mem m y) x && - List.for_all (fun m -> List.mem m x) y - -let pr_keymod l = - if l = mC then - "Ctrl-" - else - if l = mM then - if Coq_config.arch = "Darwin" then "Ctrl-Cmd-" else "Meta-" - else - "" - -let mkE ?(mods=mC) key keyname doc ?(alias=[]) contents = - List.map (fun (mods, key, keyname) -> { mods; key; keyname; doc; contents }) - ((mods, key, keyname)::alias) - -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 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 (List.flatten 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_action gui group name = - ((actiong gui group)#get_action name)#activate () - -let run key gui action status = - match action with - | Callback f -> f gui; status - | Action(group, name) -> run_action gui group name; status - | Edit f -> - let b = (ct gui).script#source_buffer in - let i = b#get_iter_at_mark `INSERT in - let status = f status b i (run_action gui) in - if not status.sel then - b#place_cursor ~where:(b#get_iter_at_mark `SEL_BOUND); - status - | Motion f -> - let b, script = (ct gui).script#source_buffer, (ct gui).script in - let sel_mode = status.sel || List.mem `SHIFT (GdkEvent.Key.state key) in - let i = - if sel_mode then b#get_iter_at_mark `SEL_BOUND - else b#get_iter_at_mark `INSERT in - let where, status = f status i in - let sel_mode = status.sel || List.mem `SHIFT (GdkEvent.Key.state key) in - if sel_mode then (b#move_mark `SEL_BOUND ~where; script#scroll_mark_onscreen `SEL_BOUND) - else (b#place_cursor ~where; script#scroll_mark_onscreen `INSERT); - status - -let emacs = empty - -let emacs = insert emacs "Emacs" [] [ - (* motion *) - 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 with move = None })); - mkE ~mods:mM _Right "->" "Move to end of buffer" (Motion(fun s i -> - i#forward_to_end, - { s with move = None })); - mkE ~mods:mM _Left "<-" "Move to start of buffer" (Motion(fun s i -> - let buffer = new GText.buffer i#buffer in - buffer#start_iter, - { s with move = None })); - mkE _a "a" "Move to beginning of line" (Motion(fun s i -> - (i#set_line_offset 0), { s with move = None })); - mkE ~mods:mM _e "e" "Move to end of sentence" (Motion(fun s i -> - i#forward_sentence_end, { s with move = None })); - mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i -> - i#backward_sentence_start, { s with move = None })); - mkE _n "n" "Move to next line" (Motion(fun s i -> - let orig_off = Option.default i#line_offset s.move 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), - { s with move = Some orig_off })); - mkE _p "p" "Move to previous line" (Motion(fun s i -> - let orig_off = Option.default i#line_offset s.move 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), - { s with move = Some orig_off })); - mkE _f "f" "Forward char" ~alias:[[],_Right,"RIGHT"] - (Motion(fun s i -> i#forward_char, { s with move = None })); - mkE _b "b" "Backward char" ~alias:[[],_Left,"LEFT"] - (Motion(fun s i -> i#backward_char, { s with move = None })); - mkE ~mods:mM _f "f" "Forward word" ~alias:[mC,_Right,"RIGHT"] - (Motion(fun s i -> i#forward_word_end, { s with move = None })); - mkE ~mods:mM _b "b" "Backward word" ~alias:[mC,_Left,"LEFT"] - (Motion(fun s i -> i#backward_word_start, { s with move = None })); - mkE _space "SPC" "Set mark" ~alias:[mC,_at,"@"] (Motion(fun s i -> - if s.sel = false then i, { s with sel = true } - else i, { s with sel = false } )); - (* edits *) - mkE ~mods:mM _w "w" "Copy selected region" (Edit(fun s b i run -> - if sel_nonempty b then - let txt = get_sel_txt b in - run "Edit" "Copy"; - { s with kill = Some(txt,false); sel = false } - else s)); - mkE _w "w" "Kill selected region" (Edit(fun s b i run -> - if sel_nonempty b then - let txt = get_sel_txt b in - run "Edit" "Cut"; - { s with kill = Some(txt,false); sel = false } - else s)); - mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ -> - let already_killed = match s.kill with Some (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 - { s with kill = Some (already_killed ^ k,true) })); - mkE ~mods:mM _d "d" "Kill next word" (Edit(fun s b i _ -> - let already_killed = match s.kill with Some (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 - { s with kill = Some (already_killed ^ k,true) })); - mkE ~mods:mM _k "k" "Kill until sentence end" (Edit(fun s b i _ -> - let already_killed = match s.kill with Some (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 - { s with kill = Some (already_killed ^ k,true) })); - mkE ~mods:mM _BackSpace "DELBACK" "Kill word before cursor" - (Edit(fun s b i _ -> - let already_killed = match s.kill with Some (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 - { s with kill = Some (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.kill with - | Some (k,_) -> k, { s with kill = Some (k,false) } - | _ -> "", s in - b#insert ~iter:i k; - s)); - (* misc *) - 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 run_action gui "Edit" "Find Next" - else run_action gui "Edit" "Find")); - mkE _s "r" "Search backward" (Callback(fun gui -> - if (ct gui).finder#coerce#misc#visible - then run_action gui "Edit" "Find Previous" - else run_action gui "Edit" "Find")); - ] - -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")); - mkE ~mods:[] _u "u" "Undo" (Action("Edit", "Undo")); - ] - -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 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 empty = { sel = false; kill = None; move = None } - -let find gui (Step(here,konts)) t = - (* hack: ^c does copy in clipboard *) - let sel_nonempty () = sel_nonempty (ct gui).script#source_buffer in - let k = GdkEvent.Key.keyval t in - if k = _x && mod_of t mC && sel_nonempty () then - ignore(run t gui (Action("Edit","Cut")) empty) - else - if k = _c && mod_of t mC && sel_nonempty () then - ignore(run t 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 cur = ref pg in - let status = ref empty in - let reset () = eprintf "reset\n%!"; cur := pg in - ignore(w#event#connect#key_press ~callback:(fun t -> - let on_current_term f = - let term = try Some nb#current_term with Invalid_argument _ -> None in - match term with None -> false | Some t -> f t - in - on_current_term (fun x -> - if x.script#misc#get_property "has-focus" <> `BOOL true - then false - else begin - eprintf "got key %s\n%!" (pr_key t); - if nanoPG#get 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 t 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 - end))); - ignore(w#event#connect#button_press ~callback:(fun t -> reset (); false)) - - - -let get_documentation () = - "Chars, words, lines and sentences below pertain to standard unicode segmentation rules\n" ^ - print_keypaths pg diff --git a/ide/nanoPG.mli b/ide/nanoPG.mli deleted file mode 100644 index bc9b39d823..0000000000 --- a/ide/nanoPG.mli +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* string -val init : GWindow.window -> Session.session Wg_Notebook.typed_notebook -> - GAction.action_group list -> unit diff --git a/ide/preferences.ml b/ide/preferences.ml index 3893d023bd..4e2e3f31e6 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -561,7 +561,8 @@ let tab_length = let highlight_current_line = new preference ~name:["highlight_current_line"] ~init:false ~repr:Repr.(bool) -let nanoPG = +let microPG = + (* Legacy name in preference is "nanoPG" *) new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool) let user_queries = @@ -799,7 +800,7 @@ let configure ?(apply=(fun () -> ())) parent = let () = button "Show progress bar" show_progress_bar in let () = button "Insert spaces instead of tabs" spaces_instead_of_tabs in let () = button "Highlight current line" highlight_current_line in - let () = button "Emacs/PG keybindings (μPG mode)" nanoPG in + let () = button "Emacs/PG keybindings (μPG mode)" microPG in let callback () = () in custom ~label box callback true in diff --git a/ide/preferences.mli b/ide/preferences.mli index 785c191b46..b01c4598d8 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -102,7 +102,7 @@ val show_progress_bar : bool preference val spaces_instead_of_tabs : bool preference val tab_length : int preference val highlight_current_line : bool preference -val nanoPG : bool preference +val microPG : bool preference val user_queries : (string * string) list preference val diffs : string preference -- cgit v1.2.3