]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitaGui.ml
pango escape fixed
[helm.git] / helm / software / matita / matitaGui.ml
index a77800c1e05192395e141aa075a5e361dde61944..827bdf375ceee5ed004ecc62379eaacd347ef707 100644 (file)
@@ -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 ^ "<b>" ^ str2 ^ "</b>" ^ colorize stop tl
+          escape_pango_markup str1 ^ "<b>" ^ 
+          escape_pango_markup str2 ^ "</b>" ^ 
+          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 =