some hacks to make the sequent window pretty nice

[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index f781ea3d763b33a6570989eeee5bb825b79fb0c7..9fb8455f9260a7aaa3d1d27049a8e5ab99d712ca 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -125,6 +125,8 @@ let pp_macro pp_term = function
   | Undo (_, Some n) -> sprintf "Undo %d" n
   | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
+  | Instance _
+  | Match _ -> assert false
 
 let pp_macro_ast = pp_macro pp_term_ast
 let pp_macro_cic = pp_macro pp_term_cic
@@ -198,3 +200,15 @@ and pp_tacticals tacs =
 let pp_tactical tac = pp_tactical tac ^ tactical_terminator
 let pp_tactic tac = pp_tactic tac ^ tactic_terminator
 
+let pp_executable = function
+  | Macro (_,x) -> pp_macro_ast x
+  | Tactical (_,x) -> pp_tactical x
+  | Command (_,x) -> pp_command x
+                      
+let pp_comment = function
+  | Note (_,str) -> sprintf "(* %s *)" str
+  | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code)
+
+let pp_statement = function
+  | Executable (_, ex) -> pp_executable ex
+  | Comment (_, c) -> pp_comment c