From 37137e82f6e002d36c8052b506bf2d0a36fcd6de Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 17 Aug 2008 14:38:40 +0000 Subject: [PATCH] escape < in pango attrs --- helm/software/matita/matitaAutoGui.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) 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 "" else "") ^ - ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false - max_int [] c t^(if size > 0 then "" else "") + (Pcre.replace ~pat:"<" ~templ:"<" + (Pcre.replace ~pat:">" ~templ:">" + (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false + max_int [] c t)))^ + (if size > 0 then "" 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 -- 2.39.2