diff options
| -rw-r--r-- | ide/coqide.ml | 8 | ||||
| -rw-r--r-- | ide/ide.mllib | 2 | ||||
| -rw-r--r-- | ide/microPG.ml (renamed from ide/nanoPG.ml) | 2 | ||||
| -rw-r--r-- | ide/microPG.mli (renamed from ide/nanoPG.mli) | 0 | ||||
| -rw-r--r-- | ide/preferences.ml | 5 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 |
6 files changed, 10 insertions, 9 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/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 5e6c0b8462..25cab4638c 100644 --- a/ide/nanoPG.ml +++ b/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); 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 |