* 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 ()
projects / helm.git / blobdiff