pango escape fixed

diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt
index ee77638cc8508d5779d434d89d5ca0709d131444..19b605d2de31e9c862c60b5362144ac33c383d2f 100644 (file)
--- a/helm/software/matita/.depend.opt
+++ b/helm/software/matita/.depend.opt
@@ -4,10 +4,10 @@ dump_moo.cmo: buildTimeConf.cmx
 dump_moo.cmx: buildTimeConf.cmx 
 lablGraphviz.cmo: lablGraphviz.cmi 
 lablGraphviz.cmx: lablGraphviz.cmi 
-matitaAutoGui.cmo: matitaGeneratedGui.cmx applyTransformation.cmi \
-    matitaAutoGui.cmi 
-matitaAutoGui.cmx: matitaGeneratedGui.cmx applyTransformation.cmx \
-    matitaAutoGui.cmi 
+matitaAutoGui.cmo: matitaGeneratedGui.cmx buildTimeConf.cmx \
+    applyTransformation.cmi matitaAutoGui.cmi 
+matitaAutoGui.cmx: matitaGeneratedGui.cmx buildTimeConf.cmx \
+    applyTransformation.cmx matitaAutoGui.cmi 
 matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi 
 matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi 
 matitacLib.cmo: matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmx \
@@ -34,10 +34,8 @@ matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
 matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
     matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \
     matitaExcPp.cmx matitaAutoGui.cmx buildTimeConf.cmx matitaGui.cmi 
-matitaInit.cmo: matitacLib.cmi matitaExcPp.cmi buildTimeConf.cmx \
-    matitaInit.cmi 
-matitaInit.cmx: matitacLib.cmx matitaExcPp.cmx buildTimeConf.cmx \
-    matitaInit.cmi 
+matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi 
+matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi 
 matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
     matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \
     buildTimeConf.cmx applyTransformation.cmi matitaMathView.cmi 

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index e350c80b6c3cac51bd757a1d9a0f3c69700fee00..bc317b4f3a37997e67b241e3443b7d85841265d5 100644 (file)
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -36,8 +36,8 @@ MLI = \
        applyTransformation.mli \
        matitacLib.mli          \
        matitaInit.mli          \
-       matitaAutoGui.mli       \
        matitaGtkMisc.mli       \
+       matitaAutoGui.mli       \
        matitaScript.mli        \
        matitaMathView.mli      \
        matitaGui.mli           \

diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index 23905905bf73b11f16aa1a2a05e7aa40572e399c..d01cac5d14a698166a25637fcd379f0aadc4c9f7 100644 (file)
--- a/helm/software/matita/matitaAutoGui.ml
+++ b/helm/software/matita/matitaAutoGui.ml
@@ -49,10 +49,9 @@ let pp ?(size=(!font_size)) c t =
       ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t
   in
   (if size > 0 then "<span font_desc=\""^string_of_int size^"\">" else "") ^
-  (Pcre.replace ~pat:"<" ~templ:"&lt;"
-   (Pcre.replace ~pat:">" ~templ:"&gt;"
+  (MatitaGtkMisc.escape_pango_markup
     (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
-      max_int [] c t)))^
+      max_int [] c t))^
   (if size > 0 then "</span>" else "")
 ;;
 let pp_goal context x = 
@@ -161,7 +160,7 @@ let old_displayed_status = ref [];;
 let old_size = ref 0;;
 
 let fill_win (win : MatitaGeneratedGui.autoWin) cb =
-  let init = Unix.gettimeofday () in
+(*   let init = Unix.gettimeofday () in *)
     try 
       let (status : status) = cb () in
       let win_size = win#toplevel#misc#allocation.Gtk.width in
@@ -181,8 +180,10 @@ let fill_win (win : MatitaGeneratedGui.autoWin) cb =
           List.iter win#table#remove win#table#children;
           let height = win#viewportAREA#misc#allocation.Gtk.height in
           elems_to_rows height ctx win_size win#table displayed_status;
+(*
           Printf.eprintf 
             "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -.  init);
+*)
         end
     with exn -> prerr_endline (Printexc.to_string exn); ()
 ;;
@@ -214,7 +215,10 @@ let auto_dialog elems =
       Auto.step ();
       win#toplevel#destroy ();
       GMain.Main.quit ();true));
-  let redraw_callback _ = fill_win win elems;true in
+  let redraw_callback _ = 
+    fill_win win elems;
+    true 
+  in
   let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
   ignore(win#buttonPAUSE#connect#clicked 
     (fun _ -> 

diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml
index 9c00dfddef4aa1b7879026c85e12fa1df0c3700d..872780540197ab9f2f98eaf2c42718606af391cb 100644 (file)
--- a/helm/software/matita/matitaGtkMisc.ml
+++ b/helm/software/matita/matitaGtkMisc.ml
@@ -411,4 +411,13 @@ let utf8_string_length s =
   if BuildTimeConf.debug then
     assert(Glib.Utf8.validate s);
   Glib.Utf8.length s
+
+let escape_pango_markup text =
+   let text = Pcre.replace ~pat:"&" ~templ:"&" text in
+   let text = Pcre.replace ~pat:"<" ~templ:"&lt;" text in
+   let text = Pcre.replace ~pat:"'" ~templ:"&apos;" text in
+   let text = Pcre.replace ~pat:"\"" ~templ:"&quot;" text in
+   text
+;;
+
     

diff --git a/helm/software/matita/matitaGtkMisc.mli b/helm/software/matita/matitaGtkMisc.mli
index e7d57265854244ed0d6ca549315c68a2a69d9760..adea6961d1ee44896e29c8176809ab80bcb904aa 100644 (file)
--- a/helm/software/matita/matitaGtkMisc.mli
+++ b/helm/software/matita/matitaGtkMisc.mli
@@ -150,3 +150,5 @@ val utf8_parsed_text: string -> Stdpp.location -> string * int
 
     (* the length in characters, not bytes *)
 val utf8_string_length: string -> int
+
+val escape_pango_markup: string -> string

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 9e8cfd86cd4c3163be5906acf735fd63df9d9c0f..827bdf375ceee5ed004ecc62379eaacd347ef707 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -1377,14 +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 text = Pcre.replace ~pat:"<" ~templ:"&lt;" text in
-  let text = Pcre.replace ~pat:"'" ~templ:"&apos;" text in
-  let text = Pcre.replace ~pat:"\"" ~templ:"&quot;" text in
-  let text = Pcre.replace ~pat:">" ~templ:"&gt;" text in
   let gui = instance () in
     let dialog = gui#newUriDialog () in
     dialog#uriEntryHBox#misc#hide ();
@@ -1400,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; *)
@@ -1425,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 =