- 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 7eab7b1ef086f09b68f9223b90f1d68b5650725c..e0e0bfca3385ec92996bd07da6ad0a4c4b8be674 100644 (file)
--- 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)))