some experiments

[helm.git] / matita / matitaGtkMisc.mli

diff --git a/matita/matitaGtkMisc.mli b/matita/matitaGtkMisc.mli
index 1affd2a39e78822d2449ef7abe087d57102b4717..16b0591b2651a5a09856f5bdfad0c192c66d9c58 100644 (file)
--- a/matita/matitaGtkMisc.mli
+++ b/matita/matitaGtkMisc.mli
@@ -155,3 +155,11 @@ val report_error:
   unit ->
     unit
 
+    (* given an utf8 string a floc returns the parsed substring and its length
+     * in bytes *)
+val utf8_parsed_text: string -> Token.flocation -> string * int
+
+    (* the length in characters, not bytes *)
+val utf8_string_length: string -> int
+
+