Even nicer script.

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 8ffa5fc914e77f522f1b9849b1f19f1bfcda4268..e9302d5ac3d57a4bb664755ea9ee7ceec7ab2eb6 100644 (file)
--- a/matita/matitaGui.ml
+++ b/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
@@ -1025,8 +1030,6 @@ class gui () =
       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" false;
       main#unicodeAsTexMenuItem#set_active
         (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)