From: Stefano Zacchiroli Date: Thu, 29 Jan 2004 14:53:16 +0000 (+0000) Subject: - s/TexTermEditor/TermEditor/ (* former no longer appropriate) X-Git-Tag: V_0_2_3~126 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8dc254e60fb7ee127568bf1b0e5050f49b5167e1;p=helm.git - s/TexTermEditor/TermEditor/ (* former no longer appropriate) - added "auto disambiguation" setting support --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7eab7b1ef..e0e0bfca3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -78,6 +78,8 @@ let environmentfile = let restore_environment_on_boot = true ;; let notify_hbugs_on_goal_change = false ;; +let auto_disambiguation = ref true ;; + (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let check_term = ref (fun _ _ _ -> assert false);; @@ -222,110 +224,131 @@ let interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris = - let choices = ref [] in - let chosen = ref false in - let use_only_constants = ref false in - let window = - GWindow.dialog ~modal:true ~title ~width:600 () in - let lMessage = - GMisc.label ~text:msg - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 - ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in - let clist = - let expected_height = 18 * List.length uris in - let height = if expected_height > 400 then 400 else expected_height in - GList.clist ~columns:1 ~packing:scrolled_window#add - ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in - let _ = List.map (function x -> clist#append [x]) uris in - let hbox2 = - GPack.hbox ~border_width:0 - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let explain_label = - GMisc.label ~text:"None of the above. Try this one:" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let manual_input = - GEdit.entry ~editable:true - ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in - let hbox = - GPack.hbox ~border_width:0 ~packing:window#action_area#add () in - let okb = - GButton.button ~label:ok - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive false in - let nonvarsb = - GButton.button - ~packing: - (function w -> - if enable_button_for_non_vars then - hbox#pack ~expand:false ~fill:false ~padding:5 w) - ~label:"Try constants only" () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox#pack ~padding:5) () in - let _ = checkb#misc#set_sensitive false in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - (* actions *) - let check_callback () = - assert (List.length !choices > 0) ; - check_window (outputhtml ()) !choices + let only_constant_choices = + lazy + (List.filter + (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + uris) in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; - ignore - (nonvarsb#connect#clicked - (function () -> - use_only_constants := true ; - chosen := true ; - window#destroy () - )) ; - ignore (checkb#connect#clicked check_callback) ; - ignore - (clist#connect#select_row - (fun ~row ~column ~event -> - checkb#misc#set_sensitive true ; - okb#misc#set_sensitive true ; - choices := (List.nth uris row)::!choices)) ; - ignore - (clist#connect#unselect_row - (fun ~row ~column ~event -> - choices := - List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; - ignore - (manual_input#connect#changed - (fun _ -> - if manual_input#text = "" then - begin - choices := [] ; - checkb#misc#set_sensitive false ; - okb#misc#set_sensitive false ; - clist#misc#set_sensitive true - end - else - begin - choices := [manual_input#text] ; - clist#unselect_all () ; + if !auto_disambiguation then + Lazy.force only_constant_choices + else begin + let choices = ref [] in + let chosen = ref false in + let use_only_constants = ref false in + let window = + GWindow.dialog ~modal:true ~title ~width:600 () in + let lMessage = + GMisc.label ~text:msg + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + let expected_height = 18 * List.length uris in + let height = if expected_height > 400 then 400 else expected_height in + GList.clist ~columns:1 ~packing:scrolled_window#add + ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in + let _ = List.map (function x -> clist#append [x]) uris in + let hbox2 = + GPack.hbox ~border_width:0 + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let explain_label = + GMisc.label ~text:"None of the above. Try this one:" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let manual_input = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let hbox = + GPack.hbox ~border_width:0 ~packing:window#action_area#add () in + let okb = + GButton.button ~label:ok + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let nonvarsb = + GButton.button + ~packing: + (function w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Try constants only" () in + let autob = + GButton.button + ~packing: + (fun w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Auto" () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox#pack ~padding:5) () in + let _ = checkb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + let check_callback () = + assert (List.length !choices > 0) ; + check_window (outputhtml ()) !choices + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; + ignore + (nonvarsb#connect#clicked + (function () -> + use_only_constants := true ; + chosen := true ; + window#destroy () + )) ; + ignore (autob#connect#clicked (fun () -> + auto_disambiguation := true; + (rendering_window ())#set_auto_disambiguation true; + use_only_constants := true ; + chosen := true; + window#destroy ())); + ignore (checkb#connect#clicked check_callback) ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> checkb#misc#set_sensitive true ; okb#misc#set_sensitive true ; - clist#misc#set_sensitive false - end)); - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - if !chosen then - if !use_only_constants then - List.filter - (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) - uris - else - if List.length !choices > 0 then !choices else raise NoChoice - else - raise NoChoice + choices := (List.nth uris row)::!choices)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + choices := + List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; + ignore + (manual_input#connect#changed + (fun _ -> + if manual_input#text = "" then + begin + choices := [] ; + checkb#misc#set_sensitive false ; + okb#misc#set_sensitive false ; + clist#misc#set_sensitive true + end + else + begin + choices := [manual_input#text] ; + clist#unselect_all () ; + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + clist#misc#set_sensitive false + end)); + window#set_position `CENTER ; + window#show () ; + GtkThread.main (); + if !chosen then + if !use_only_constants then + Lazy.force only_constant_choices + else + if List.length !choices > 0 then !choices else raise NoChoice + else + raise NoChoice + end ;; let interactive_interpretation_choice interpretations = @@ -1070,7 +1093,7 @@ module Callbacks = end ;; -module TexTermEditor' = ChosenTermEditor.Make(Callbacks);; +module TermEditor' = ChosenTermEditor.Make(Callbacks);; (* OTHER FUNCTIONS *) @@ -1216,7 +1239,7 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () @@ -1328,7 +1351,7 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () @@ -1475,7 +1498,7 @@ let new_proof () = ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* moved here to have visibility of the ok button *) let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window#add ~share_environment_with:inputt () @@ -2778,6 +2801,9 @@ class rendering_window output (notebook : notebook) = let _ = factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K ~callback:clear_aliases in + let autoitem = + factory3#add_check_item "Auto disambiguation" + ~callback:(fun checked -> auto_disambiguation := checked) in let _ = factory3#add_separator () in let _ = factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P @@ -2823,7 +2849,7 @@ class rendering_window output (notebook : notebook) = GBin.scrolled_window ~border_width:5 ~packing:frame#add () in let inputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: @@ -2848,6 +2874,7 @@ object method scratch_window = scratch_window method notebook = notebook method show = window#show + method set_auto_disambiguation set = autoitem#set_active set initializer notebook#set_empty_page ; (*export_to_postscript_menu_item#misc#set_sensitive false ;*) @@ -2875,6 +2902,7 @@ let initialize_everything () = let output = TermViewer.proof_viewer ~width:350 ~height:280 () in let notebook = new notebook in let rendering_window' = new rendering_window output notebook in + rendering_window'#set_auto_disambiguation !auto_disambiguation; set_rendering_window rendering_window' ; let print_error_as_html prefix msg = output_html (outputhtml ()) (`Error (`T (prefix ^ msg)))