X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=827bdf375ceee5ed004ecc62379eaacd347ef707;hb=02763a89e6351dfb7770251d0507512e3f0ddb74;hp=a77800c1e05192395e141aa075a5e361dde61944;hpb=558224e07a053eb99eaba1aed56c686056840dec;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index a77800c1e..827bdf375 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1232,7 +1232,8 @@ class gui () = method private updateFontSize () = self#sourceView#misc#modify_font_by_name - (sprintf "%s %d" BuildTimeConf.script_font font_size) + (sprintf "%s %d" BuildTimeConf.script_font font_size); + MatitaAutoGui.set_font_size font_size method increaseFontSize () = font_size <- font_size + 1; @@ -1376,9 +1377,10 @@ class interpModel = tree_store#get ~row:iter ~column:interp_no_col end + let interactive_string_choice text prefix_len ?(title = "") ?(msg = "") () ~id locs uris -= += let gui = instance () in let dialog = gui#newUriDialog () in dialog#uriEntryHBox#misc#hide (); @@ -1394,13 +1396,15 @@ let interactive_string_choice let rec colorize acc_len = function | [] -> let floc = HExtlib.floc_of_loc (acc_len,hack_len) in - fst(MatitaGtkMisc.utf8_parsed_text text floc) + escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc)) | he::tl -> let start, stop = HExtlib.loc_of_floc he in let floc1 = HExtlib.floc_of_loc (acc_len,start) in let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in - str1 ^ "" ^ str2 ^ "" ^ colorize stop tl + escape_pango_markup str1 ^ "" ^ + escape_pango_markup str2 ^ "" ^ + colorize stop tl in (* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in Printf.eprintf "(%d,%d)" start stop) locs; *) @@ -1419,6 +1423,7 @@ let interactive_string_choice let txt,_ = MatitaGtkMisc.utf8_parsed_text txt (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) in + prerr_endline ("txt:" ^ txt); dialog#uriChoiceLabel#set_label txt; List.iter model#easy_append uris; let return v =