From 8498344c49c66aa84cf7484fdbd9c292f9aae5c6 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 29 Jan 2004 13:25:52 +0000 Subject: [PATCH] - added "clear alias" menu item - added "clear" button to the "edit aliases" window --- helm/gTopLevel/gTopLevel.ml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7363abc2c..7eab7b1ef 100644 --- 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 -- 2.39.2