X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGtkMisc.ml;h=6407ae35d1e8654fb89022b574704f50fea84422;hb=fe39d8e524aef8839f21be44fe1f3af53379e458;hp=553406635aac812e87ba39576f566bbe747f1e08;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/matitaGtkMisc.ml b/matita/matitaGtkMisc.ml
index 553406635..6407ae35d 100644
--- a/matita/matitaGtkMisc.ml
+++ b/matita/matitaGtkMisc.ml
@@ -28,16 +28,18 @@
 exception PopupClosed
 open Printf
 
-let wrap_callback f = f
+let wrap_callback0 f = fun _ -> try f () with Not_found -> assert false
+let wrap_callback1 f = fun _ -> try f () with Not_found -> assert false
+let wrap_callback2 f = fun _ -> try f () with Not_found -> assert false
 
 let connect_button (button: #GButton.button) callback =
-  ignore (button#connect#clicked (wrap_callback callback))
+  ignore (button#connect#clicked (wrap_callback0 callback))
 
 let connect_toggle_button (button: #GButton.toggle_button) callback =
-  ignore (button#connect#toggled (wrap_callback callback))
+  ignore (button#connect#toggled (wrap_callback1 callback))
 
 let connect_menu_item (menu_item: #GMenu.menu_item) callback =
-  ignore (menu_item#connect#activate (wrap_callback callback))
+  ignore (menu_item#connect#activate (wrap_callback2 callback))
 
 let connect_key (ev:GObj.event_ops) ?(modifiers = []) ?(stop = false) key
   callback
@@ -437,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
+