exec :: Command -> Env -> (Proof,String)
exec c env@(calculus,tree) =
 case c of
   CRefine g (i,j) r  -> (t, m ++++ prProof t)
                            where (t,m) = refine (calculus,tree) g (i,j) r
   CInstance par term -> (t, prProof t)
                            where t = instantiate calculus par term tree
   CTry g limit       -> (t, m ++++ prProof t)
                            where (t,m) = tryRefine (calculus,tree) g limit
   CNew sequent       -> (t, prProof t)
                            where t = Goal sequent
   CRemove ints       -> (t, m ++++ prProof t)
                            where (t,m) = remove tree ints
   CShowGoals         -> (tree, prGoals (goalsOfProof tree))
   CShowTree          -> (tree, prProofNodes True tree)
   CShowApplicable g  -> (tree, showAllApplicableRules (calculus,tree) g)
   CChange _          -> (tree, "")
   CAxioms file       -> (tree, "axioms written in" +++ file ++ ".rules.tex")
   CLatex file        -> (tree, "proof written in" +++ file ++ ".tex")
   CNatural file      -> (tree, "natural deduction tree written in" +++ file ++ ".tex")
   CHistory file      -> (tree, "history written in" +++ file)
   CHelp              -> (tree, helpMessage)
   CManual            -> (tree, "")
   CQuit              -> (tree, "Goodbye")
   _                  -> (tree, "no command processed")
exec :: Command -> Env -> (Proof,String)
exec c env@(calculus,tree) =
 case c of
   CRefine g (i,j) r  -> (t, m ++++ prProof t)
                            where (t,m) = refine (calculus,tree) g (i,j) r
   CInstance par term -> (t, prProof t)
                            where t = instantiate calculus par term tree
   CTry g limit       -> (t, m ++++ prProof t)
                            where (t,m) = tryRefine (calculus,tree) g limit
   CNew sequent       -> (t, prProof t)
                            where t = Goal sequent
   CRemove ints       -> (t, m ++++ prProof t)
                            where (t,m) = remove tree ints
   CShowGoals         -> (tree, prGoals (goalsOfProof tree))
   CShowTree          -> (tree, prProofNodes True tree)
   CShowApplicable g  -> (tree, showAllApplicableRules (calculus,tree) g)
   CChange _          -> (tree, "")
   CAxioms file       -> (tree, "axioms written in" +++ file ++ ".rules.tex")
   CLatex file        -> (tree, "proof written in" +++ file ++ ".tex")
   CNatural file      -> (tree, "natural deduction tree written in" +++ file ++ ".tex")
   CHistory file      -> (tree, "history written in" +++ file)
   CHelp              -> (tree, helpMessage)
   CManual            -> (tree, "")
   CQuit              -> (tree, "Goodbye")
   _                  -> (tree, "no command processed")
exec c env@(calculus,tree) =
 case c of
   CRefine g (i,j) r  -> (t, m ++++ prProof t)
                            where (t,m) = refine (calculus,tree) g (i,j) r
   CInstance par term -> (t, prProof t)
                            where t = instantiate calculus par term tree
   CTry g limit       -> (t, m ++++ prProof t)
                            where (t,m) = tryRefine (calculus,tree) g limit
   CNew sequent       -> (t, prProof t)
                            where t = Goal sequent
   CRemove ints       -> (t, m ++++ prProof t)
                            where (t,m) = remove tree ints
   CShowGoals         -> (tree, prGoals (goalsOfProof tree))
   CShowTree          -> (tree, prProofNodes True tree)
   CShowApplicable g  -> (tree, showAllApplicableRules (calculus,tree) g)
   CChange _          -> (tree, "")
   CAxioms file       -> (tree, "axioms written in" +++ file ++ ".rules.tex")
   CLatex file        -> (tree, "proof written in" +++ file ++ ".tex")
   CNatural file      -> (tree, "natural deduction tree written in" +++ file ++ ".tex")
   CHistory file      -> (tree, "history written in" +++ file)
   CHelp              -> (tree, helpMessage)
   CManual            -> (tree, "")
   CQuit              -> (tree, "Goodbye")
   _                  -> (tree, "no command processed")