From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 17 Aug 2008 14:38:40 +0000 (+0000)
Subject: escape < in pango attrs
X-Git-Tag: make_still_working~4863
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=37137e82f6e002d36c8052b506bf2d0a36fcd6de;p=helm.git

escape < in pango attrs
---

diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index a4d7ce85f..23905905b 100644
--- a/helm/software/matita/matitaAutoGui.ml
+++ b/helm/software/matita/matitaAutoGui.ml
@@ -49,8 +49,11 @@ 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 "") ^
-    ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
-      max_int [] c t^(if size > 0 then "</span>" else "")
+  (Pcre.replace ~pat:"<" ~templ:"&lt;"
+   (Pcre.replace ~pat:">" ~templ:"&gt;"
+    (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
+      max_int [] c t)))^
+  (if size > 0 then "</span>" else "")
 ;;
 let pp_goal context x = 
   if x == fake_goal then "" else pp context x
@@ -110,7 +113,7 @@ let cell_of_candidate height context ?(active=false) g id c =
 let cell_of_goal height win_width context goal = 
   GMisc.label 
     ~markup:(pp_goal context goal) ~xalign:0.0 
-    ~width:(min (win_width * 60 / 100) 500) 
+    ~width:(min (win_width * 30 / 100) 500) 
     ~line_wrap:false
     ~ellipsize:`END
     ~height