X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=95d0a76310ebea5d645935ee81ea0b1914791ad7;hb=397b5f9d848e63a9703a1f90faf9869092ec8893;hp=94cb736b89d33982d02575aaf498834d7bd0854e;hpb=8405aa804344fd6c4e54b0d019e56dce14bfdf1e;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 94cb736b8..95d0a7631 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -968,7 +968,10 @@ class gui () =
         if (MatitaScript.current ())#onGoingProof () then
           (MatitaScript.current ())#advance
             ~statement:("\n"
-              ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+              ^ GrafiteAstPp.pp_tactic
+                ~map_unicode_to_tex:(Helm_registry.get_bool
+                  "matita.paste_unicode_as_tex")
+                ~term_pp:CicNotationPp.pp_term
                 ~lazy_term_pp:CicNotationPp.pp_term ast)
             ()
       in
@@ -978,6 +981,8 @@ class gui () =
           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
             ("\n"
             ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+              ~map_unicode_to_tex:(Helm_registry.get_bool
+                "matita.paste_unicode_as_tex")
               ~lazy_term_pp:CicNotationPp.pp_term ast)
       in
       let tbar = main in
@@ -1026,7 +1031,7 @@ class gui () =
         ~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;
+        Helm_registry.set_bool "matita.paste_unicode_as_tex" false;
       main#unicodeAsTexMenuItem#set_active
         (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)