X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=8fbe6b8d1c709b84dc995fd6bb020e3603346927;hb=4dc87cc7384ba61136bc82a23effe6a52160e720;hp=5f1213fa48578d59c3970a8e8b9b40f8089037be;hpb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 5f1213fa4..8fbe6b8d1 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -89,7 +89,7 @@ let pp_just ~term_pp =
   | `Auto params -> pp_auto_params ~term_pp params
 ;;
 
-let pp_ntactic ~map_unicode_to_tex = function
+let rec pp_ntactic ~map_unicode_to_tex = function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
   | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
@@ -119,6 +119,11 @@ let pp_ntactic ~map_unicode_to_tex = function
         (String.concat " " (List.map string_of_int l))
   | NUnfocus _ -> "##unfocus"
   | NSkip _ -> "##skip"
+  | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac
+  | NAssumption _ -> "nassumption"
+  | NBlock (_,l) -> 
+     "(" ^ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) l)^ ")"
+  | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
@@ -368,8 +373,9 @@ let pp_command ~term_pp ~obj_pp = function
      "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
-  | Include (_,true,path) -> "include \"" ^ path ^ "\""
-  | Include (_,false,path) -> "include source \"" ^ path ^ "\""
+  | Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\""
+  | Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\""
+  | Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ path
   | Obj (_,obj) -> obj_pp obj
   | Qed _ -> "qed"
   | Relation (_,id,a,aeq,refl,sym,trans) ->