From 02763a89e6351dfb7770251d0507512e3f0ddb74 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Aug 2008 23:08:44 +0000 Subject: [PATCH] pango escape fixed --- helm/software/matita/.depend.opt | 14 ++++++-------- helm/software/matita/Makefile | 2 +- helm/software/matita/matitaAutoGui.ml | 14 +++++++++----- helm/software/matita/matitaGtkMisc.ml | 9 +++++++++ helm/software/matita/matitaGtkMisc.mli | 2 ++ helm/software/matita/matitaGui.ml | 13 ++++++------- 6 files changed, 33 insertions(+), 21 deletions(-) diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt index ee77638cc..19b605d2d 100644 --- 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 e350c80b6..bc317b4f3 100644 --- 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 23905905b..d01cac5d1 100644 --- 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 "" else "") ^ - (Pcre.replace ~pat:"<" ~templ:"<" - (Pcre.replace ~pat:">" ~templ:">" + (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 "" 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 9c00dfdde..872780540 100644 --- 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:"<" text in + let text = Pcre.replace ~pat:"'" ~templ:"'" text in + let text = Pcre.replace ~pat:"\"" ~templ:""" text in + text +;; + diff --git a/helm/software/matita/matitaGtkMisc.mli b/helm/software/matita/matitaGtkMisc.mli index e7d572658..adea6961d 100644 --- 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 9e8cfd86c..827bdf375 100644 --- 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:"<" text in - let text = Pcre.replace ~pat:"'" ~templ:"'" text in - let text = Pcre.replace ~pat:"\"" ~templ:""" text in - let text = Pcre.replace ~pat:">" ~templ:">" 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 ^ "" ^ 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; *) @@ -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 = -- 2.39.2