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.

(cherry picked from commit d911384)

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

ide/ide.mllib

@@ -30,5 +30,5 @@ CoqOps
 Wg_Command
 Session
 Coqide_ui
-NanoPG
+MicroPG
 Coqide

ide/nanoPG.ml → ide/microPG.ml

@@ -325,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);

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

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