From: Stefano Zacchiroli Date: Tue, 20 Apr 2004 08:54:23 +0000 (+0000) Subject: snapshot X-Git-Tag: dead_dir_walking~27 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=07287062d5b84a0f2b66380d0d380bbf68217a27;p=helm.git snapshot --- diff --git a/helm/mathita/.depend b/helm/mathita/.depend index d322c64f4..1fea79aff 100644 --- a/helm/mathita/.depend +++ b/helm/mathita/.depend @@ -4,6 +4,6 @@ mathitaGtkMisc.cmo: mathitaGtkMisc.cmi 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 diff --git a/helm/mathita/mathita.glade b/helm/mathita/mathita.glade index 9f5a5f4f6..cc299bad6 100644 --- a/helm/mathita/mathita.glade +++ b/helm/mathita/mathita.glade @@ -40,7 +40,7 @@ True - + True gtk-new 1 @@ -83,7 +83,7 @@ - + True gtk-open 1 @@ -104,7 +104,7 @@ - + True gtk-save 1 @@ -124,7 +124,7 @@ True - + True gtk-save-as 1 @@ -151,7 +151,7 @@ - + True gtk-quit 1 @@ -208,6 +208,43 @@ + + + True + Debug + True + + + + + + + True + 0 + True + + + + + + True + 1 + True + + + + + + True + 2 + True + + + + + + + True @@ -574,7 +611,6 @@ 280 - True Uri choice GTK_WINDOW_TOPLEVEL GTK_WIN_POS_CENTER @@ -675,6 +711,7 @@ True + False True True Try Constants @@ -980,4 +1017,64 @@ + + True + dialog1 + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + True + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + + + + + diff --git a/helm/mathita/mathita.ml b/helm/mathita/mathita.ml index b1cfaddcc..f22a035a5 100644 --- a/helm/mathita/mathita.ml +++ b/helm/mathita/mathita.ml @@ -26,14 +26,16 @@ 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 = @@ -42,123 +44,53 @@ let interactive_user_uri_choice (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 = @@ -173,9 +105,50 @@ 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 () diff --git a/helm/mathita/mathitaGeneratedGui.ml b/helm/mathita/mathitaGeneratedGui.ml index f09c13a11..2b2e03ded 100644 --- a/helm/mathita/mathitaGeneratedGui.ml +++ b/helm/mathita/mathitaGeneratedGui.ml @@ -32,10 +32,10 @@ class mainWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -52,26 +52,26 @@ class mainWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -80,10 +80,10 @@ class mainWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -104,6 +104,26 @@ class mainWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -421,9 +441,41 @@ class interpChoiceDialog ?(file="mathita.glade") ?domain ?autoconnect(*=true*) ( 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 (); diff --git a/helm/mathita/mathitaGeneratedGui.mli b/helm/mathita/mathitaGeneratedGui.mli index 8fa10245f..6b72a8b27 100644 --- a/helm/mathita/mathitaGeneratedGui.mli +++ b/helm/mathita/mathitaGeneratedGui.mli @@ -5,16 +5,21 @@ class mainWin : 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 @@ -40,16 +45,21 @@ class mainWin : 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 @@ -274,4 +284,26 @@ class interpChoiceDialog : 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 diff --git a/helm/mathita/mathitaGtkMisc.ml b/helm/mathita/mathitaGtkMisc.ml index 36478d529..fc4fecc8f 100644 --- a/helm/mathita/mathitaGtkMisc.ml +++ b/helm/mathita/mathitaGtkMisc.ml @@ -44,3 +44,34 @@ let add_key_binding key callback (evbox: GBin.event_box) = 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 + diff --git a/helm/mathita/mathitaGtkMisc.mli b/helm/mathita/mathitaGtkMisc.mli index 987ad1857..03847ac87 100644 --- a/helm/mathita/mathitaGtkMisc.mli +++ b/helm/mathita/mathitaGtkMisc.mli @@ -35,3 +35,14 @@ val toggle_win: 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 + diff --git a/helm/mathita/mathitaGui.ml b/helm/mathita/mathitaGui.ml index cda4a474f..957c5edcc 100644 --- a/helm/mathita/mathitaGui.ml +++ b/helm/mathita/mathitaGui.ml @@ -23,6 +23,24 @@ * 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 @@ -39,6 +57,7 @@ class gui file = 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 *) @@ -85,5 +104,7 @@ class gui file = ignore (main#quitMenuItem#connect#activate callback); self#addKeyBinding GdkKeysyms._q callback + method uriChoices = uriChoices + end diff --git a/helm/mathita/mathitaGui.mli b/helm/mathita/mathitaGui.mli index 0c19204a6..4dcc0a5d7 100644 --- a/helm/mathita/mathitaGui.mli +++ b/helm/mathita/mathitaGui.mli @@ -23,7 +23,13 @@ * 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 : @@ -32,16 +38,18 @@ 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