X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;fp=helm%2Fmatita%2FmatitaGui.ml;h=16712c4541b77047970d8530b69c165427021340;hb=99b249b23524cda2d91602ee088fef1a7be253ee;hp=5aa3d59e9c69edb491a4bd3c0189d33d16cf6489;hpb=6a149d262dfcb03a7d57f8ecabf23b0b59e99f85;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5aa3d59e9..16712c454 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -548,14 +548,18 @@ class gui () =
       let tac ast _ =
         if (MatitaScript.current ())#onGoingProof () then
           (MatitaScript.current ())#advance
-            ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+            ~statement:("\n"
+              ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term
+                ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast)))
             ()
       in
       let tac_w_term ast _ =
         if (MatitaScript.current ())#onGoingProof () then
           let buf = source_buffer in
           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
-            ("\n" ^ GrafiteAstPp.pp_tactic ast)
+            ("\n"
+            ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+              ~lazy_term_pp:CicNotationPp.pp_term ast)
       in
       let tbar = main in
       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
@@ -823,24 +827,23 @@ class gui () =
 
       (** selections / clipboards handling *)
 
-    method private markup_selected = MatitaMathView.has_selection ()
-    method private text_selected =
+    method markupSelected = MatitaMathView.has_selection ()
+    method private textSelected =
       (source_buffer#get_iter_at_mark `INSERT)#compare
         (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
-    method private something_selected =
-      self#markup_selected || self#text_selected
-    method private markup_stored = MatitaMathView.has_clipboard ()
-    method private text_stored = clipboard#text <> None
-    method private something_stored = self#markup_stored || self#text_stored
+    method private somethingSelected = self#markupSelected || self#textSelected
+    method private markupStored = MatitaMathView.has_clipboard ()
+    method private textStored = clipboard#text <> None
+    method private somethingStored = self#markupStored || self#textStored
 
-    method canCopy = self#something_selected
-    method canCut = self#text_selected
-    method canDelete = self#text_selected
-    method canPaste = self#something_stored
-    method canPastePattern = self#markup_stored
+    method canCopy = self#somethingSelected
+    method canCut = self#textSelected
+    method canDelete = self#textSelected
+    method canPaste = self#somethingStored
+    method canPastePattern = self#markupStored
 
     method copy () =
-      if self#text_selected
+      if self#textSelected
       then begin
         MatitaMathView.empty_clipboard ();
         source_view#buffer#copy_clipboard clipboard;