Added toggle for enabling/disabling the conversion from multibyte unicode

[helm.git] / matita / matitaMathView.ml

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index c32c00f203c12c4fa99dad0730cdd3b79335bae0..4252014bd83115bfae8ad9927dfd88cabcef0967 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/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 =