new nrepeat (and block '('...')' ) tactical

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 5f1213fa48578d59c3970a8e8b9b40f8089037be..8fbe6b8d1c709b84dc995fd6bb020e3603346927 100644 (file)
--- 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) ->