X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.mli;h=1affd2a39e78822d2449ef7abe087d57102b4717;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=5753293304b52e6470561e4771f785d2c4122151;hpb=6e289c07138a9840beff4833b57521593fd732b1;p=helm.git

diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli
index 575329330..1affd2a39 100644
--- a/helm/matita/matitaGtkMisc.mli
+++ b/helm/matita/matitaGtkMisc.mli
@@ -35,6 +35,9 @@ val toggle_window_visibility:
 val toggle_widget_visibility:
   widget:GObj.widget -> check:GMenu.check_menu_item -> unit
 
+val toggle_callback:
+  callback:(bool -> unit) -> check:GMenu.check_menu_item -> unit
+  
 val toggle_win:
   ?check:GMenu.check_menu_item -> GWindow.window -> unit -> unit
 
@@ -67,16 +70,29 @@ val connect_key:
   (unit -> unit) -> (* callback *)
     unit
 
+  (** n-ary string column list *)
+class multiStringListModel:
+  cols:int ->
+  GTree.view ->
+  object
+    method list_store: GTree.list_store (** list_store forwarding *)
+
+    method easy_mappend:     string list -> unit        (** append + set *)
+    method easy_minsert:     int -> string list -> unit (** insert + set *)
+    method easy_mselection:  unit -> string list list
+  end
+  
   (** single string column list *)
 class stringListModel:
   GTree.view ->
   object
-    method list_store: GTree.list_store (** list_store forwarding *)
+    inherit multiStringListModel
 
     method easy_append:     string -> unit        (** append + set *)
     method easy_insert:     int -> string -> unit (** insert + set *)
     method easy_selection:  unit -> string list
   end
+  
 
   (** as above with Pixbuf associated to each row. Each time an insert is
    * performed a string tag should be specified, the corresponding pixbuf in the
@@ -97,24 +113,45 @@ class taggedStringListModel:
 class type gui =
   object  (* minimal gui object requirements *)
     method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
-    method newInterpDialog:       unit -> MatitaGeneratedGui.interpChoiceDialog
+    method newRecordDialog:       unit -> MatitaGeneratedGui.recordChoiceDialog
     method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
     method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
   end
 
-  (** {3 Dialogs} *)
+  (** {3 Dialogs}
+   * In functions below:
+   * @param title window title
+   * @param message content of the text label shown to the user *)
 
-  (** @return true if user hit "ok" button, false if user hit "cancel" button
-  * @param cancel if set to true a cancel button is shown to the user, otherwise
-  *   it is not (and indeed the function will return true). Defaults to true *)
+  (** @param parent to center the window on it *)
 val ask_confirmation:
-  gui:#gui ->
-  ?cancel:bool -> ?title:string -> ?msg:string -> unit ->
-    bool
+  title:string -> message:string -> 
+  ?parent:#GWindow.window_skel ->
+  unit ->
+    [`YES | `NO | `CANCEL]
 
   (** @param multiline (default: false) if true a TextView widget will be used
   * for prompting the user otherwise a TextEntry widget will be
   * @return the string given by the user *)
 val ask_text:
-  gui:#gui -> ?title:string -> ?msg:string -> ?multiline:bool -> unit -> string
+  gui:#gui ->
+  ?title:string -> ?message:string ->
+  ?multiline:bool -> ?default:string -> unit ->
+    string
+
+  (** @param fields field names
+   * @param records list of records, each record is a list of [fields] strings
+   * @return number of the chosen record, 0 for the first one *)
+val ask_record_choice:
+  gui:#gui ->
+  ?title:string -> ?message:string ->
+  fields:string list -> records:string list list ->
+  unit ->
+    int
+
+val report_error:
+  title:string -> message:string -> 
+  ?parent:#GWindow.window_skel ->
+  unit ->
+    unit