- added "clear alias" menu item

- added "clear" button to the "edit aliases" window

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 7363abc2c02295d809fa86d54f6cf5d2e6af3b48..7eab7b1ef086f09b68f9223b90f1d68b5650725c 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -721,6 +721,13 @@ let load_unfinished_proof () =
        (`Error (`T (Printexc.to_string e)))
 ;;
 
+let clear_aliases () =
+  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
+  inputt#environment :=
+    DisambiguatingParser.EnvironmentP3.of_string
+      DisambiguatingParser.EnvironmentP3.empty
+;;
+
 let edit_aliases () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
  let disambiguation_env = inputt#environment in
@@ -741,14 +748,18 @@ let edit_aliases () =
  let okb =
   GButton.button ~label:"Ok"
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearb =
+  GButton.button ~label:"Clear"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  let cancelb =
   GButton.button ~label:"Cancel"
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  ignore (window#connect#destroy GMain.Main.quit) ;
  ignore (cancelb#connect#clicked window#destroy) ;
+ ignore (clearb#connect#clicked (fun () ->
+  input#buffer#set_text DisambiguatingParser.EnvironmentP3.empty)) ;
  ignore (okb#connect#clicked (fun () ->
-    chosen_aliases := Some (input#buffer#get_text
-      ~start:input#buffer#start_iter ~stop:input#buffer#end_iter ());
+    chosen_aliases := Some (input#buffer#get_text ());
     window#destroy ()));
   ignore
    (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
@@ -2764,6 +2775,9 @@ class rendering_window output (notebook : notebook) =
  let _ =
   factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A
    ~callback:edit_aliases in
+ let _ =
+  factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K
+   ~callback:clear_aliases in
  let _ = factory3#add_separator () in
  let _ =
   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P