mathitaGtkMisc.cmx: mathitaGtkMisc.cmi
mathitaGui.cmo: mathitaGeneratedGui.cmi mathitaGtkMisc.cmi mathitaGui.cmi
mathitaGui.cmx: mathitaGeneratedGui.cmx mathitaGtkMisc.cmx mathitaGui.cmi
-mathita.cmo: mathitaGui.cmi
-mathita.cmx: mathitaGui.cmx
-mathitaGui.cmi: mathitaGeneratedGui.cmi
+mathita.cmo: mathitaGeneratedGui.cmi mathitaGui.cmi
+mathita.cmx: mathitaGeneratedGui.cmx mathitaGui.cmx
+mathitaGui.cmi: mathitaGeneratedGui.cmi mathitaGtkMisc.cmi
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image13">
+ <widget class="GtkImage" id="image40">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image14">
+ <widget class="GtkImage" id="image41">
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image15">
+ <widget class="GtkImage" id="image42">
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image16">
+ <widget class="GtkImage" id="image43">
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image17">
+ <widget class="GtkImage" id="image44">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
</widget>
</child>
+ <child>
+ <widget class="GtkMenuItem" id="DebugMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Debug</property>
+ <property name="use_underline">True</property>
+
+ <child>
+ <widget class="GtkMenu" id="DebugMenu_menu">
+
+ <child>
+ <widget class="GtkMenuItem" id="DebugMenuItem0">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">0</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="DebugMenuItem1">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">1</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="DebugMenuItem2">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">2</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
<child>
<widget class="GtkMenuItem" id="HelpMenu">
<property name="visible">True</property>
<widget class="GtkDialog" id="UriChoiceDialog">
<property name="height_request">280</property>
- <property name="visible">True</property>
<property name="title" translatable="yes">Uri choice</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_CENTER</property>
<child>
<widget class="GtkButton" id="UriChoiceConstantsButton">
<property name="visible">True</property>
+ <property name="sensitive">False</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
<property name="label" translatable="yes">Try Constants</property>
</child>
</widget>
+<widget class="GtkDialog" id="Debug">
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">dialog1</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">True</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox5">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area5">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="cancelbutton2">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="okbutton2">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+</widget>
+
</glade-interface>
exception Not_implemented of string
let not_implemented feature = raise (Not_implemented feature)
+ (** exceptions whose content should be presented to the user *)
+exception Failure of string
+let error s = raise (Failure s)
+
let _ = Helm_registry.load_from "mathita.conf.xml"
let _ = GMain.Main.init ()
let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file")
-(*
let interactive_user_uri_choice
- ~selection_mode:[`MULTIPLE|`SINGLE] ?(ok="Ok")
- ?(enable_button_for_non_vars=false) ~title ~msg
+ ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=false) ~title ~msg
uris
=
let only_constant_choices =
(fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
uris)
in
- if selection_mode <> `SINGLE && !auto_disambiguation then
+ if (selection_mode <> `SINGLE) &&
+ (Helm_registry.get_bool "mathita.auto_disambiguation")
+ then
Lazy.force only_constant_choices
else begin
+ let win = gui#uriChoice in
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 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
+ win#uriChoiceDialog#set_title title;
+ win#uriChoiceLabel#set_text msg;
+ gui#uriChoices#list_store#clear ();
+ List.iter gui#uriChoices#easy_append uris;
+ win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+ let bye = ref (fun () -> ()) in
+ let id1 =
+ win#uriChoiceConstantsButton#connect#clicked (fun _ ->
+ use_only_constants := true;
+ !bye ())
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;
+ let id2 =
+ win#uriChoiceAutoButton#connect#clicked (fun _ ->
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
+ Helm_registry.set_bool "mathita.auto_disambiguation" true;
+ !bye ())
+ in
+ let id3 =
+ win#uriChoiceSelectedButton#connect#clicked (fun _ ->
+ choices := gui#uriChoices#easy_selection ();
+ !bye ())
+ in
+ bye := (fun () ->
+ win#uriChoiceDialog#misc#hide ();
+ win#uriChoiceConstantsButton#misc#disconnect id1;
+ win#uriChoiceAutoButton#misc#disconnect id2;
+ win#uriChoiceSelectedButton#misc#disconnect id3;
+ prerr_endline "quit";
+ GMain.Main.quit ());
+ win#uriChoiceDialog#show ();
+ GtkThread.main ();
+ if !use_only_constants then
+ Lazy.force only_constant_choices
+ else
+ match !choices with
+ | [] -> error "No choice"
+ | choices -> choices
end
- ;;
-*)
(*
module DisambiguateCallbacks =
end
*)
+let debugDialog () =
+ let dialog =
+ new MathitaGeneratedGui.debug
+ ~file:(Helm_registry.get "mathita.glade_file") ()
+ in
+ let retval = ref None in
+ let return v =
+ retval := Some v;
+ dialog#debug#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#debug#event#connect#delete (fun _ -> true));
+ ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1));
+ ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2));
+ dialog#debug#show ();
+ GtkThread.main ();
+ (match !retval with None -> assert false | Some v -> v)
+
+let _ =
+ gui#main#debugMenuItem2#connect#activate (fun _ ->
+ prerr_endline (string_of_int (debugDialog ())))
+
(** quit program, possibly asking for confirmation *)
let quit () = GMain.Main.quit ()
let _ = gui#setQuitCallback quit
+let _ =
+ gui#main#debugMenuItem0#connect#activate (fun _ ->
+ let uris =
+ interactive_user_uri_choice
+ ~selection_mode:`MULTIPLE
+ ~nonvars_button:false
+ ~title:"titolo"
+ ~msg:"messaggio"
+ ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
+ "cic:/cinque.var"]
+ in
+ List.iter prerr_endline uris; print_newline ())
+let _ =
+ gui#main#debugMenuItem1#connect#activate (fun _ ->
+ Helm_registry.set_bool "mathita.auto_disambiguation"
+ (not (Helm_registry.get_bool "mathita.auto_disambiguation")))
-let _ = GtkThread.main ()
+let _ =
+(* gui#uriChoices#easy_append "pippo"; *)
+(* gui#uriChoices#list_store#clear (); *)
+ GtkThread.main ()
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
method newMenu = newMenu
- val image13 =
+ val image40 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image13" ~info:"GtkImage" xmldata))
- method image13 = image13
+ (Glade.get_widget_msg ~name:"image40" ~info:"GtkImage" xmldata))
+ method image40 = image40
val newMenu_menu =
new GMenu.menu (GtkMenu.Menu.cast
(Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
method openMenuItem = openMenuItem
- val image14 =
+ val image41 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image14" ~info:"GtkImage" xmldata))
- method image14 = image14
+ (Glade.get_widget_msg ~name:"image41" ~info:"GtkImage" xmldata))
+ method image41 = image41
val saveMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveMenuItem = saveMenuItem
- val image15 =
+ val image42 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image15" ~info:"GtkImage" xmldata))
- method image15 = image15
+ (Glade.get_widget_msg ~name:"image42" ~info:"GtkImage" xmldata))
+ method image42 = image42
val saveAsMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveAsMenuItem = saveAsMenuItem
- val image16 =
+ val image43 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image16" ~info:"GtkImage" xmldata))
- method image16 = image16
+ (Glade.get_widget_msg ~name:"image43" ~info:"GtkImage" xmldata))
+ method image43 = image43
val separator1 =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"separator1" ~info:"GtkMenuItem" xmldata))
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
method quitMenuItem = quitMenuItem
- val image17 =
+ val image44 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image17" ~info:"GtkImage" xmldata))
- method image17 = image17
+ (Glade.get_widget_msg ~name:"image44" ~info:"GtkImage" xmldata))
+ method image44 = image44
val editMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
(Glade.get_widget_msg ~name:"ShowProofMenuItem" ~info:"GtkCheckMenuItem" xmldata))
method showProofMenuItem = showProofMenuItem
+ val debugMenu =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata))
+ method debugMenu = debugMenu
+ val debugMenu_menu =
+ new GMenu.menu (GtkMenu.Menu.cast
+ (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata))
+ method debugMenu_menu = debugMenu_menu
+ val debugMenuItem0 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"DebugMenuItem0" ~info:"GtkMenuItem" xmldata))
+ method debugMenuItem0 = debugMenuItem0
+ val debugMenuItem1 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"DebugMenuItem1" ~info:"GtkMenuItem" xmldata))
+ method debugMenuItem1 = debugMenuItem1
+ val debugMenuItem2 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"DebugMenuItem2" ~info:"GtkMenuItem" xmldata))
+ method debugMenuItem2 = debugMenuItem2
val helpMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata))
toplevel#destroy ()
method check_widgets () = ()
end
+class debug ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"Debug" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val debug : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
+ method debug = debug
+ val dialog_vbox5 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"dialog-vbox5" ~info:"GtkVBox" xmldata))
+ method dialog_vbox5 = dialog_vbox5
+ val cancelbutton2 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"cancelbutton2" ~info:"GtkButton" xmldata))
+ method cancelbutton2 = cancelbutton2
+ val okbutton2 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"okbutton2" ~info:"GtkButton" xmldata))
+ method okbutton2 = okbutton2
+ method reparent parent =
+ dialog_vbox5#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
let check_all ?(show=false) () =
ignore (GMain.Main.init ());
+ let debug = new debug () in
+ if show then debug#toplevel#show ();
+ debug#check_widgets ();
let interpChoiceDialog = new interpChoiceDialog () in
if show then interpChoiceDialog#toplevel#show ();
interpChoiceDialog#check_widgets ();
unit ->
object
val aboutMenuItem : GMenu.menu_item
+ val debugMenu : GMenu.menu_item
+ val debugMenuItem0 : GMenu.menu_item
+ val debugMenuItem1 : GMenu.menu_item
+ val debugMenuItem2 : GMenu.menu_item
+ val debugMenu_menu : GMenu.menu
val editMenu : GMenu.menu_item
val fileMenu : GMenu.menu_item
val fileMenu_menu : GMenu.menu
val helpMenu : GMenu.menu_item
val helpMenu_menu : GMenu.menu
- val image13 : GMisc.image
- val image14 : GMisc.image
- val image15 : GMisc.image
- val image16 : GMisc.image
- val image17 : GMisc.image
+ val image40 : GMisc.image
+ val image41 : GMisc.image
+ val image42 : GMisc.image
+ val image43 : GMisc.image
+ val image44 : GMisc.image
val mainMenuBar : GMenu.menu_shell
val mainStatusBar : GMisc.statusbar
val mainVPanes : GPack.paned
method aboutMenuItem : GMenu.menu_item
method bind : name:string -> callback:(unit -> unit) -> unit
method check_widgets : unit -> unit
+ method debugMenu : GMenu.menu_item
+ method debugMenuItem0 : GMenu.menu_item
+ method debugMenuItem1 : GMenu.menu_item
+ method debugMenuItem2 : GMenu.menu_item
+ method debugMenu_menu : GMenu.menu
method editMenu : GMenu.menu_item
method fileMenu : GMenu.menu_item
method fileMenu_menu : GMenu.menu
method helpMenu : GMenu.menu_item
method helpMenu_menu : GMenu.menu
- method image13 : GMisc.image
- method image14 : GMisc.image
- method image15 : GMisc.image
- method image16 : GMisc.image
- method image17 : GMisc.image
+ method image40 : GMisc.image
+ method image41 : GMisc.image
+ method image42 : GMisc.image
+ method image43 : GMisc.image
+ method image44 : GMisc.image
method mainMenuBar : GMenu.menu_shell
method mainStatusBar : GMisc.statusbar
method mainVPanes : GPack.paned
method vbox3 : GPack.box
method xml : Glade.glade_xml Gtk.obj
end
+class debug :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val cancelbutton2 : GButton.button
+ val debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val dialog_vbox5 : GPack.box
+ val okbutton2 : GButton.button
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method cancelbutton2 : GButton.button
+ method check_widgets : unit -> unit
+ method debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method dialog_vbox5 : GPack.box
+ method okbutton2 : GButton.button
+ method reparent : GObj.widget -> unit
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method xml : Glade.glade_xml Gtk.obj
+ end
val check_all : ?show:bool -> unit -> unit
false
| _ -> false))
+class stringListModel (tree_view: GTree.view) =
+ let column_list = new GTree.column_list in
+ let text_column = column_list#add Gobject.Data.string in
+ let list_store = GTree.list_store column_list in
+ object (self)
+
+ initializer
+ let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
+ let view_column = GTree.view_column ~renderer () in
+ tree_view#set_model (Some (list_store :> GTree.model));
+ ignore (tree_view#append_column view_column)
+
+ method list_store = list_store
+
+ method easy_append s =
+ let tree_iter = list_store#append () in
+ list_store#set ~row:tree_iter ~column:text_column s
+
+ method easy_insert pos s =
+ let tree_iter = list_store#insert pos in
+ list_store#set ~row:tree_iter ~column:text_column s
+
+ method easy_selection () =
+ List.map
+ (fun tree_path ->
+ let iter = list_store#get_iter tree_path in
+ list_store#get ~row:iter ~column:text_column)
+ tree_view#selection#get_selected_rows
+
+ end
+
val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit
+ (** single string column list *)
+class stringListModel:
+ GTree.view ->
+ object
+ method list_store: GTree.list_store (** list_store forwarding *)
+
+ method easy_append: string -> unit (** append + set *)
+ method easy_insert: int -> string -> unit (** insert + set *)
+ method easy_selection: unit -> string list
+ end
+
* http://helm.cs.unibo.it/
*)
+(*
+class stringListModel' uriChoiceDialog =
+ let tree_view = uriChoiceDialog#uriChoiceTreeView in
+ let column_list = new GTree.column_list in
+ let text_column = column_list#add Gobject.Data.string in
+ let list_store = GTree.list_store column_list in
+ let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
+ let view_column = GTree.view_column ~renderer () in
+ let _ = tree_view#set_model (Some (list_store :> GTree.model)) in
+ let _ = tree_view#append_column view_column in
+ object
+ method append s =
+ let tree_iter = list_store#append () in
+ list_store#set ~row:tree_iter ~column:text_column s
+ method clear () = list_store#clear ()
+ end
+*)
+
open MathitaGeneratedGui
open MathitaGtkMisc
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ toolbar#toolBarEventBox; proof#proofWinEventBox ]
in
+ let uriChoices = new stringListModel uriChoice#uriChoiceTreeView in
object (self)
initializer
(* glade's check widgets *)
ignore (main#quitMenuItem#connect#activate callback);
self#addKeyBinding GdkKeysyms._q callback
+ method uriChoices = uriChoices
+
end
* http://helm.cs.unibo.it/
*)
-open MathitaGeneratedGui
+(*
+class type stringListModel =
+ object
+ method clear: unit -> unit
+ method append: string -> unit
+ end
+*)
(** @param fname name of the Glade file describing the GUI *)
class gui :
method setQuitCallback : (unit -> unit) -> unit
+ method uriChoices: MathitaGtkMisc.stringListModel
+
(** {2 Access to low-level GTK widgets} *)
- method about : MathitaGeneratedGui.aboutWin
- method dialog : MathitaGeneratedGui.genericDialog
- method fileSel : MathitaGeneratedGui.fileSelectionWin
+ method about : MathitaGeneratedGui.aboutWin
+ method dialog : MathitaGeneratedGui.genericDialog
+ method fileSel : MathitaGeneratedGui.fileSelectionWin
method interpChoice : MathitaGeneratedGui.interpChoiceDialog
- method main : MathitaGeneratedGui.mainWin
- method proof : MathitaGeneratedGui.proofWin
- method toolbar : MathitaGeneratedGui.toolBarWin
- method uriChoice : MathitaGeneratedGui.uriChoiceDialog
+ method main : MathitaGeneratedGui.mainWin
+ method proof : MathitaGeneratedGui.proofWin
+ method toolbar : MathitaGeneratedGui.toolBarWin
+ method uriChoice : MathitaGeneratedGui.uriChoiceDialog
end
projects / helm.git / commitdiff