From fa6addea4fa1f37567dca9104164710870a50392 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 9 Feb 2007 16:18:01 +0000 Subject: [PATCH] Added toggle for enabling/disabling the conversion from multibyte unicode characters to TeX when converting CIC terms to textual formulae. The toggle is under the Edit menu (rational: it's near the paste commands, maybe it should be added to the GtkSourceView contextual menu too). The toggle governs the matita.paste_unicode_as_tex boolean registry value. The txt_of_* rendering functions have been changed to accept a new optional boolean parameter. --- .../software/components/content_pres/boxPp.ml | 24 +++++----- .../components/content_pres/boxPp.mli | 8 +++- helm/software/matita/applyTransformation.ml | 25 ++++++----- helm/software/matita/applyTransformation.mli | 13 ++++-- helm/software/matita/matita.glade | 45 +++++++++++-------- helm/software/matita/matitaGui.ml | 12 +++-- helm/software/matita/matitaMathView.ml | 4 +- 7 files changed, 83 insertions(+), 48 deletions(-) diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml index b9bb9fbbd..ca51c0ed3 100644 --- a/helm/software/components/content_pres/boxPp.ml +++ b/helm/software/components/content_pres/boxPp.ml @@ -93,7 +93,7 @@ let fixed_rendering s = let s_len = String.length s in (fun _ -> s_len, [s]) -let render_to_strings choose_action size markup = +let render_to_strings ?(map_unicode_to_tex = true) choose_action size markup = let max_size = max_int in let rec aux_box = function @@ -193,14 +193,17 @@ let render_to_strings choose_action size markup = | Pres.Mgliph (_, s) -> fixed_rendering s | Pres.Mo (_, s) -> let s = - if String.length s = 1 && Char.code s.[0] < 128 then - s - else - match Utf8Macro.tex_of_unicode s with - Some s -> s ^ " " - | None -> s + if map_unicode_to_tex then begin + if String.length s = 1 && Char.code s.[0] < 128 then + s + else + match Utf8Macro.tex_of_unicode s with + | Some s -> s ^ " " + | None -> s + end else + s in - fixed_rendering s + fixed_rendering s | Pres.Mspace _ -> fixed_rendering string_space | Pres.Mrow (attrs, children) -> let children' = List.map aux_mpres children in @@ -237,6 +240,7 @@ let render_to_strings choose_action size markup = in snd (aux_mpres markup size) -let render_to_string choose_action size markup = - String.concat "\n" (render_to_strings choose_action size markup) +let render_to_string ?map_unicode_to_tex choose_action size markup = + String.concat "\n" + (render_to_strings ?map_unicode_to_tex choose_action size markup) diff --git a/helm/software/components/content_pres/boxPp.mli b/helm/software/components/content_pres/boxPp.mli index fe05e24d9..66ae8ec95 100644 --- a/helm/software/components/content_pres/boxPp.mli +++ b/helm/software/components/content_pres/boxPp.mli @@ -23,15 +23,21 @@ * http://helm.cs.unibo.it/ *) - (** @return rows list of rows *) + (** + * @param map_unicode_to_tex if true converts multibye unicode sequences to + * TeX-like macros (when possible). Default: true + * @return rows list of rows *) val render_to_strings: + ?map_unicode_to_tex:bool -> (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> int -> CicNotationPres.markup -> string list (** helper function + * @param map_unicode_to_tex as above * @return s, concatenation of the return value of render_to_strings above * with newlines as separators *) val render_to_string: + ?map_unicode_to_tex:bool -> (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> int -> CicNotationPres.markup -> string diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 47e8dd231..499c1705b 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -70,7 +70,7 @@ let mml_of_cic_object obj = (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses, ids_to_inner_sorts,ids_to_inner_types))) -let txt_of_cic_sequent size metasenv sequent = +let txt_of_cic_sequent ?map_unicode_to_tex size metasenv sequent = let unsh_sequent,(asequent,ids_to_terms, ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses) = @@ -81,10 +81,10 @@ let txt_of_cic_sequent size metasenv sequent = CicNotationPres.mpres_of_box (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in - BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size - pres_sequent + BoxPp.render_to_string ?map_unicode_to_tex + (function x::_ -> x | _ -> assert false) size pres_sequent -let txt_of_cic_sequent_conclusion size metasenv sequent = +let txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv sequent = let _,(asequent,_,_,ids_to_inner_sorts,_) = Cic2acic.asequent_of_sequent metasenv sequent in @@ -92,11 +92,12 @@ let txt_of_cic_sequent_conclusion size metasenv sequent = let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in let t = TermContentPres.pp_ast t in let t = CicNotationPres.render ids_to_uris t in - BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size t + BoxPp.render_to_string ?map_unicode_to_tex + (function x::_ -> x | _ -> assert false) size t -let txt_of_cic_term size metasenv context t = +let txt_of_cic_term ?map_unicode_to_tex size metasenv context t = let fake_sequent = (-1,context,t) in - txt_of_cic_sequent_conclusion size metasenv fake_sequent + txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv fake_sequent ;; ignore ( @@ -139,7 +140,7 @@ ignore ( let remove_closed_substs s = Pcre.replace ~pat:"{...}" ~templ:"" s -let term2pres n ids_to_inner_sorts annterm = +let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm = let ast, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in @@ -151,10 +152,10 @@ let term2pres n ids_to_inner_sorts annterm = in let render = function _::x::_ -> x | _ -> assert false in let mpres = CicNotationPres.mpres_of_box bobj in - let s = BoxPp.render_to_string render n mpres in + let s = BoxPp.render_to_string ?map_unicode_to_tex render n mpres in remove_closed_substs s -let txt_of_cic_object n style prefix obj = +let txt_of_cic_object ?map_unicode_to_tex n style prefix obj = let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = try Cic2acic.acic_object_of_cic_object obj with e -> @@ -166,7 +167,9 @@ let txt_of_cic_object n style prefix obj = let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in remove_closed_substs ("\n\n" ^ - BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) + BoxPp.render_to_string ?map_unicode_to_tex + (function _::x::_ -> x | _ -> assert false) n + (CicNotationPres.mpres_of_box bobj) ) | GrafiteAst.Procedural depth -> let term_pp = term2pres (n - 8) ids_to_inner_sorts in diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 8e0b19361..2718d6401 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -56,15 +56,20 @@ val mml_of_cic_object: (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *) val txt_of_cic_term: - int -> Cic.metasenv -> Cic.context -> Cic.term -> string + ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term -> + string val txt_of_cic_sequent: - int -> Cic.metasenv -> Cic.conjecture -> string + ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> + string val txt_of_cic_sequent_conclusion: - int -> Cic.metasenv -> Cic.conjecture -> string + ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> + string (* columns, rendering style, name prefix, object *) val txt_of_cic_object: - int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string + ?map_unicode_to_tex:bool -> int -> GrafiteAst.presentation_style -> string -> + Cic.obj -> + string (* presentation_style, uri or baseuri, name prefix *) val txt_of_inline_macro: diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 4b3378513..6d11b4fa1 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1081,7 +1081,7 @@ - + True gtk-new 1 @@ -1102,7 +1102,7 @@ - + True gtk-open 1 @@ -1123,7 +1123,7 @@ - + True gtk-save 1 @@ -1144,7 +1144,7 @@ - + True gtk-save-as 1 @@ -1165,7 +1165,7 @@ - + True gtk-execute 1 @@ -1192,7 +1192,7 @@ - + True gtk-quit 1 @@ -1227,7 +1227,7 @@ - + True gtk-undo 1 @@ -1249,7 +1249,7 @@ - + True gtk-redo 1 @@ -1276,7 +1276,7 @@ - + True gtk-cut 1 @@ -1297,7 +1297,7 @@ - + True gtk-copy 1 @@ -1318,7 +1318,7 @@ - + True gtk-paste 1 @@ -1339,6 +1339,15 @@ + + + True + Paste Unicode as TeX + True + True + + + True @@ -1346,7 +1355,7 @@ True - + True gtk-delete 1 @@ -1387,7 +1396,7 @@ - + True gtk-find-and-replace 1 @@ -1555,7 +1564,7 @@ - + True gtk-zoom-in 1 @@ -1576,7 +1585,7 @@ - + True gtk-zoom-out 1 @@ -1597,7 +1606,7 @@ - + True gtk-zoom-100 1 @@ -1674,7 +1683,7 @@ - + True gtk-help 1 @@ -1694,7 +1703,7 @@ True - + True gtk-about 1 diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index f40efe867..a9faa592e 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1012,11 +1012,10 @@ class gui () = not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar") then main#tacticsBarMenuItem#set_active false; - MatitaGtkMisc.toggle_callback + MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem ~callback:(function | true -> main#toplevel#fullscreen () - | false -> main#toplevel#unfullscreen ()) - ~check:main#fullscreenMenuItem; + | false -> main#toplevel#unfullscreen ()); main#fullscreenMenuItem#set_active false; MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem ~callback:(function @@ -1027,6 +1026,13 @@ class gui () = CicNotation.set_active_notations []); MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem ~callback:(fun enabled -> Acic2content.hide_coercions := enabled); + MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem + ~callback:(fun enabled -> + Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled); + if not (Helm_registry.has "matita.paste_unicode_as_tex") then + Helm_registry.set_bool "matita.paste_unicode_as_tex" true; + main#unicodeAsTexMenuItem#set_active + (Helm_registry.get_bool "matita.paste_unicode_as_tex"); (* log *) HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index c32c00f20..4252014bd 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -452,7 +452,9 @@ object (self) let markup = CicNotationPres.render ids_to_uris pped_ast in BoxPp.render_to_string text_width markup *) - ApplyTransformation.txt_of_cic_sequent_conclusion + let map_unicode_to_tex = + Helm_registry.get_opt Helm_registry.bool "matita.paste_unicode_as_tex" in + ApplyTransformation.txt_of_cic_sequent_conclusion ?map_unicode_to_tex text_width metasenv cic_sequent method private pattern_of term context unsh_sequent = -- 2.39.2