module Ast = CicNotationPt
-let tactical_terminator = "."
+let tactical_terminator = ""
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
| Try (_, tac) -> "try " ^ pp_tactical tac
| Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
-and pp_tacticals ~sep tacs =
- String.concat sep (List.map pp_tactical tacs)
+ | Dot _ -> "."
+ | Semicolon _ -> ";"
+ | Branch _ -> "["
+ | Shift _ -> "|"
+ | Pos (_, i) -> sprintf "%d:" i
+ | Merge _ -> "]"
+ | Focus (_, goals) ->
+ sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
+ | Unfocus _ -> "unfocus"
+ | Skip _ -> "skip"
-let pp_tactical tac = pp_tactical tac ^ tactical_terminator
-let pp_tactic tac = pp_tactic tac ^ tactic_terminator
-let pp_command tac = pp_command tac ^ command_terminator
+and pp_tacticals ~sep tacs = String.concat sep (List.map pp_tactical tacs)
+
+let pp_tactical tac = pp_tactical tac
+let pp_tactic tac = pp_tactic tac
+let pp_command tac = pp_command tac
let pp_executable = function
| Macro (_,x) -> pp_macro_ast x
- | Tactical (_,x) -> pp_tactical x
+ | Tactical (_, tac, Some punct) -> pp_tactical tac ^ pp_tactical punct
+ | Tactical (_, tac, None) -> pp_tactical tac
| Command (_,x) -> pp_command x
let pp_comment = function