some experiments

[helm.git] / matita / matitaGtkMisc.ml

diff --git a/matita/matitaGtkMisc.ml b/matita/matitaGtkMisc.ml
index a41dbffe373713d3ca3fa5858e215f801afe5a58..6407ae35d1e8654fb89022b574704f50fea84422 100644 (file)
--- a/matita/matitaGtkMisc.ml
+++ b/matita/matitaGtkMisc.ml
@@ -439,3 +439,21 @@ let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "")
   GtkThread.main ();
   (match !record_no with Some n -> n | _ -> raise MatitaTypes.Cancel)
 
+let utf8_parsed_text s floc = 
+  let start, stop = HExtlib.loc_of_floc floc in
+  let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in
+  let stop_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:stop in
+  assert(stop_bytes >= start_bytes);
+  let bytes = stop_bytes - start_bytes in
+  try
+    String.sub s start_bytes bytes, bytes
+  with Invalid_argument _ -> 
+    Printf.eprintf "%s/%d/%d\n" s start_bytes bytes;
+    assert false
+    
+  
+let utf8_string_length s = 
+  if BuildTimeConf.debug then
+    assert(Glib.Utf8.validate s);
+  Glib.Utf8.length s
+