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

diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli
index e5d0e9be9..1affd2a39 100644
--- a/helm/matita/matitaGtkMisc.mli
+++ b/helm/matita/matitaGtkMisc.mli
@@ -113,31 +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 -> ?default:string -> unit ->
+  ?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
+