X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathita%2Fmathita.ml;h=b1cfaddccd9c2e3026b4698a528563126d5dbd07;hb=4adceafdaa4cd82c427ac9de494179c242e7ad28;hp=0d3b622ffc930d372fb344577a2b0c562ae66c0e;hpb=012882cec674d741f69fce307a6822a584fd6a45;p=helm.git

diff --git a/helm/mathita/mathita.ml b/helm/mathita/mathita.ml
index 0d3b622ff..b1cfaddcc 100644
--- a/helm/mathita/mathita.ml
+++ b/helm/mathita/mathita.ml
@@ -23,64 +23,159 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** quit program, possibly asking for confirmation *)
-let quit () =
-  GMain.Main.quit ()
+exception Not_implemented of string
+let not_implemented feature = raise (Not_implemented feature)
 
-  (** given a window and a check menu item it links the two so that the former
-   * is only hidden on delete and the latter toggle show/hide of the former *)
-let toggle_visibility (win: GWindow.window) (check: GMenu.check_menu_item) =
-  ignore (check#connect#toggled (fun _ ->
-    if check#active then win#show () else win#misc#hide ()));
-  ignore (win#event#connect#delete (fun _ ->
-    win#misc#hide ();
-    check#set_active false;
-    true))
+let _ = Helm_registry.load_from "mathita.conf.xml"
+let _ = GMain.Main.init ()
+let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file")
 
-let toggle_win ?check win () =
-  if win#is_active then win#misc#hide () else win#show ();
-  match check with
-  | None -> ()
-  | Some check -> check#set_active (not check#active)
+(*
+let interactive_user_uri_choice
+  ~selection_mode:[`MULTIPLE|`SINGLE] ?(ok="Ok")
+  ?(enable_button_for_non_vars=false) ~title ~msg
+  uris
+=
+  let only_constant_choices =
+    lazy
+      (List.filter
+        (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+        uris)
+  in
+  if selection_mode <> `SINGLE && !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
+    gui#uriChoice#uriChoiceDialog#set_title title;
+    gui#uriChoice#uriChoiceLabel#set_text msg;
+    FINQUI
 
-let add_key_bindings bindings (evbox: GBin.event_box) =
-  List.iter
-    (fun (key, callback) ->
-      ignore (evbox#event#connect#key_press (function
-        | key' when GdkEvent.Key.keyval key' = key ->
-            callback ();
-            false
-        | _ -> false)))
-    bindings
+    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 !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 ;
+          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
+ ;;
+*)
 
-class gui file =
-  object (self)
-    val about = new MathitaGui.aboutWin ~file ()
-    val dialog = new MathitaGui.genericDialog ~file ()
-    val filesel = new MathitaGui.fileSelectionWin ~file ()
-    val main = new MathitaGui.mainWin ~file ()
-    val proof = new MathitaGui.proofWin ~file ()
-    val toolbar = new MathitaGui.toolBarWin ~file ()
-    initializer
-      let c w = (w :> <check_widgets: unit -> unit>) in
-      List.iter (fun w -> w#check_widgets ())
-        [ c about; c dialog; c filesel; c main; c proof; c toolbar ];
-      ignore (main#toplevel#connect#destroy quit);
-      ignore (main#exitMenuItem#connect#activate quit);
-      toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
-      toggle_visibility proof#proofWin main#showProofMenuItem;
-      let key_bindings = [
-        GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin;
-        GdkKeysyms._q, quit;
-      ] in
-      add_key_bindings key_bindings toolbar#toolBarEventBox;
-      add_key_bindings key_bindings proof#proofWinEventBox;
-      ()
+(*
+module DisambiguateCallbacks =
+  struct
+    let interactive_user_uri_choice =
+      assert false  (* TODO *)
+(*       interactive_user_uri_choice *)
+    let interactive_interpretation_choice choices =
+      assert false  (* TODO *)
+    let input_or_locate_uri ~title =
+      assert false  (* TODO *)
   end
+*)
+
+  (** quit program, possibly asking for confirmation *)
+let quit () = GMain.Main.quit ()
+let _ = gui#setQuitCallback quit
 
-let _ =
-  let glade_file = "mathita.glade" in
-  let _ = GMain.Main.init () in
-  let gui = new gui glade_file in
-  GtkThread.main ()
+let _ = GtkThread.main ()