]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matitaGtkMisc.mli
tagging rc-1
[helm.git] / matita / matitaGtkMisc.mli
index 1affd2a39e78822d2449ef7abe087d57102b4717..0f78a4a61b45eadaa1a4cfe51e12e75ee9405765 100644 (file)
@@ -113,7 +113,6 @@ class taggedStringListModel:
 class type gui =
   object  (* minimal gui object requirements *)
     method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
-    method newRecordDialog:       unit -> MatitaGeneratedGui.recordChoiceDialog
     method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
     method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
   end
@@ -139,19 +138,17 @@ val ask_text:
   ?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
 
+    (* given an utf8 string a floc returns the parsed substring and its length
+     * in bytes *)
+val utf8_parsed_text: string -> Stdpp.location -> string * int
+
+    (* the length in characters, not bytes *)
+val utf8_string_length: string -> int
+
+