X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=e9302d5ac3d57a4bb664755ea9ee7ceec7ab2eb6;hb=c497867b0452f544661fd73b7f5dc8afbe8460e4;hp=f032831cbe2687c4638319f598407affd3e79883;hpb=111df95ac03f2ee21dfa2422a7f531f675b1c16d;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index f032831cb..e9302d5ac 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
@@ -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" true;
       main#unicodeAsTexMenuItem#set_active
         (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)
@@ -1173,6 +1176,12 @@ class gui () =
       connect_menu_item main#saveMenuItem   saveScript;
       connect_menu_item main#saveAsMenuItem saveAsScript;
       connect_menu_item main#newMenuItem    newScript;
+      connect_menu_item main#showCoercionsGraphMenuItem 
+        (fun _ -> 
+          let c = MatitaMathView.cicBrowser () in
+          c#load (`About `Coercions));
+      connect_menu_item main#showAutoGuiMenuItem 
+        (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
          (* script monospace font stuff *)  
       self#updateFontSize ();
         (* debug menu *)