Merge remote-tracking branch 'origin/master' into stm+doc_hook

8 files changed, 54 insertions, 27 deletions

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/gtk_parsing.ml b/ide/gtk_parsing.ml
index d554bebdd3..82a5e9cdf6 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -10,11 +10,11 @@
 
 let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
 let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0)
-
+let dot = Glib.Utf8.to_unichar "." ~pos:(ref 0)
 
 (* TODO: avoid num and prime at the head of a word *)
 let is_word_char c =
-  Glib.Unichar.isalnum c || c = underscore || c = prime
+  Glib.Unichar.isalnum c || c = underscore || c = prime || c = dot
 
 
 let starts_word (it:GText.iter) =
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/idetop.ml b/ide/idetop.ml
index 38839f3488..970d7cf650 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -64,7 +64,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with
 
 (** Check whether a command is forbidden in the IDE *)
 
-let ide_cmd_checks ~last_valid {CAst.loc;v=ast} =
+let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) =
   let user_error s =
     try CErrors.user_err ?loc ~hdr:"IDE" (str s)
     with e ->
@@ -72,14 +72,14 @@ let ide_cmd_checks ~last_valid {CAst.loc;v=ast} =
       let info = Stateid.add info ~valid:last_valid Stateid.dummy in
       Exninfo.raise ~info e
   in
-  if is_debug ast then
+  if is_debug cmd then
     user_error "Debug mode not available in the IDE"
 
-let ide_cmd_warns ~id {CAst.loc;v=ast} =
+let ide_cmd_warns ~id ({ CAst.loc; _ } as cmd) =
   let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
-  if is_known_option ast then
+  if is_known_option cmd then
     warn "Set this option from the IDE menu instead";
-  if is_navigation_vernac ast || is_undo ast then
+  if is_navigation_vernac cmd || is_undo cmd then
     warn "Use IDE navigation instead"
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
@@ -137,7 +137,7 @@ let annotate phrase =
   | None -> Richpp.richpp_of_pp 78 (Pp.mt ())
   | Some ast ->
     (* XXX: Width should be a parameter of annotate... *)
-    Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast.CAst.v)
+    Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
 
 (** Goal display *)
 
@@ -537,7 +537,11 @@ let rec parse = function
         Xmlprotocol.document Xml_printer.to_string_fmt; exit 0
   | "--xml_format=Ppcmds" :: rest ->
         msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest
-  | x :: rest -> x :: parse rest
+  | x :: rest ->
+     if String.length x > 0 && x.[0] = '-' then
+       (prerr_endline ("Unknown option " ^ x); exit 1)
+     else
+       x :: parse rest
   | [] -> []
 
 let () = Usage.add_to_usage "coqidetop"
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