X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=d04fbcadab4b8bcace82958733d197b007742cc4;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=deef158a335d517c3c59a0ef400d40071c673f3c;hpb=09c14db5b8930390bfc394857ae0247fb00f139c;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index deef158a3..d04fbcada 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1032,8 +1032,11 @@ class gui () = (* focus *) self#sourceView#misc#grab_focus (); (* main win dimension *) - let width = Gdk.Screen.width () in - let height = Gdk.Screen.height () in + let width = Gdk.Screen.width ~screen:(Gdk.Screen.default ()) () in + let height = Gdk.Screen.height ~screen:(Gdk.Screen.default ()) () in + (* hack for xinerama, no proper support of monitors from lablgtk *) + let width = if width > 1600 then width / 2 else width in + let height = if height > 1200 then height / 2 else height in let main_w = width * 90 / 100 in let main_h = height * 80 / 100 in let script_w = main_w * 6 / 10 in @@ -1129,12 +1132,11 @@ class gui () = let inplaceof, symb = Virtuals.symbol_of_virtual last_word in self#reset_similarsymbols; let s = Glib.Utf8.from_unichar symb in - let iter = source_buffer#get_iter_at_mark `INSERT in assert(Glib.Utf8.validate s); source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars (MatitaGtkMisc.utf8_string_length inplaceof + len)); - source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) + source_buffer#insert ~iter (if inplaceof.[0] = '\\' then s else (s ^ tok)); true with Virtuals.Not_a_virtual -> false