diff options
Diffstat (limited to 'proofs/tactic_debug.ml')
| -rw-r--r-- | proofs/tactic_debug.ml | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 08446d011..61ccbcac7 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -21,26 +21,27 @@ type debug_info = (* Prints the goal if it exists *) let db_pr_goal = function - | None -> mSGNL [< 'sTR "No goal" >] + | None -> + msgnl (str "No goal") | Some g -> - mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >] + msgnl (str "Goal:" ++ fnl () ++ Proof_trees.pr_goal (Tacmach.sig_it g)) (* Prints the commands *) let help () = - mSGNL [< 'sTR "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit" >] + msgnl (str "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit") (* Prints the state and waits for an instruction *) let debug_prompt goalopt tac_ast = db_pr_goal goalopt; - mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL >]; -(* 'sTR "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*) -(* mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL; - 'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >];*) + msg (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl ()); +(* str "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*) +(* mSG (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl () ++ fnl () ++ + str "----<Enter>=Continue----s=Skip----x=Exit----");*) let rec prompt () = - mSG [<'fNL; 'sTR "TcDebug > " >]; + msg (fnl () ++ str "TcDebug > "); flush stdout; let inst = read_line () in -(* mSGNL [<>];*) +(* mSGNL (mt ());*) match inst with | "" -> DebugOn | "s" -> DebugOff @@ -56,15 +57,15 @@ let debug_prompt goalopt tac_ast = (* Prints a constr *) let db_constr debug env c = if debug = DebugOn then - mSGNL [< 'sTR "Evaluated term --> "; prterm_env env c >] + msgnl (str "Evaluated term --> " ++ prterm_env env c) (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,c) = if debug = DebugOn then - mSGNL [< 'sTR "Matched hypothesis --> "; 'sTR (id^": "); - prterm_env env c >] + msgnl (str "Matched hypothesis --> " ++ str (id^": ") ++ + prterm_env env c) (* Prints the matched conclusion *) let db_matched_concl debug env c = if debug = DebugOn then - mSGNL [< 'sTR "Matched goal --> "; prterm_env env c >] + msgnl (str "Matched goal --> " ++ prterm_env env c) |