Merge PR #10006: NanoPG: a general fix + fixing Meta-based bindings on MacOS + adding a go-to-end binding + improving documentation

Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: ppedrot

7 files changed, 49 insertions, 19 deletions

diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 6cbd00f45d..efb5df720a 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
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/nanoPG.ml b/ide/microPG.ml
index d85d87142c..25cab4638c 100644
--- a/ide/nanoPG.ml
+++ b/ide/microPG.ml
@@ -65,14 +65,27 @@ 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 = 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-"
-  else if l = mM then "M-"
-  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 })
@@ -147,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 ->
@@ -286,9 +306,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
@@ -305,7 +325,7 @@ let init w nb ags =
     then false
     else begin
     eprintf "got key %s\n%!" (pr_key t);
-    if nanoPG#get then begin
+    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);
@@ -320,4 +340,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
diff --git a/ide/nanoPG.mli b/ide/microPG.mli
index bc9b39d823..bc9b39d823 100644
--- a/ide/nanoPG.mli
+++ b/ide/microPG.mli
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