]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGtkMisc.mli
ocaml 3.09 transition
[helm.git] / helm / matita / matitaGtkMisc.mli
index 7d4e289551cce5435cea4d1e7f6bcf8d9fedbc38..1affd2a39e78822d2449ef7abe087d57102b4717 100644 (file)
@@ -70,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
@@ -100,29 +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 *)
 
-  (* @param parent to center the window on it *)
+  (** @param parent to center the window on it *)
 val ask_confirmation:
-  title:string -> 
-  message:string -> 
+  title:string -> message:string -> 
   ?parent:#GWindow.window_skel ->
-    unit -> [`YES | `NO | `CANCEL]
-
-val report_error:
-  title:string -> 
-  message:string -> 
-  ?parent:#GWindow.window_skel ->
-    unit -> unit
+  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