added contextual menu to act over selected terms

[helm.git] / helm / matita / matitacLib.ml

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 1f9dad80f7dbcf1815dbdf7123c6a7032a7e5945..07d58b3955201e5e1de8836b5a4fa7cd01cc748e 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -27,6 +27,10 @@ open Printf
 
 open GrafiteTypes
 
+let pp_ast_statement =
+  GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj
+
 (** {2 Initialization} *)
 
 let status = ref None
@@ -44,9 +48,9 @@ let run_script is eval_function  =
     else 
       (fun status stm ->
         (* dump_status status; *)
-        let stm = GrafiteAstPp.pp_statement stm in
+        let stm = pp_ast_statement stm in
         let stm = Pcre.replace ~rex:slash_n_RE stm in
-        let stm = 
+        let stm =
           if String.length stm > 50 then
             String.sub stm 0 50 ^ " ..."
           else