5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland{- |

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandModule : $Header$

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandCopyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach,

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Swansea University 2008

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandMaintainer : csliam@swansea.ac.uk

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandStability : provisional

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandPortability : portable

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandPrinting abstract syntax of Isabelle Proofs

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland-}

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandmodule Isabelle.IsaProofPrint where

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandimport Common.Doc

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandimport Common.DocUtils

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandimport Isabelle.IsaConsts

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandimport Isabelle.IsaProof

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandinstance Pretty IsaProof where

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland pretty = printIsaProof

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandprintIsaProof :: IsaProof -> Doc

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandprintIsaProof (IsaProof p e) = fsep $ map pretty p ++ [pretty e]

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandinstance Pretty ProofCommand where

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland pretty = printProofCommand

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandprintProofCommand :: ProofCommand -> Doc

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandprintProofCommand pc =

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland case pc of

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Apply pm -> text applyS <+> pretty pm

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Using ls -> text usingS <+> fsep (map text ls)

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Back -> text backS

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Defer x -> text deferS <+> pretty x

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Prefer x -> text preferS <+> pretty x

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Refute -> text refuteS

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandinstance Pretty ProofEnd where

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland pretty = printProofEnd

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandprintProofEnd :: ProofEnd -> Doc

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandprintProofEnd pe =

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland case pe of

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland By pm -> text byS <+> pretty pm

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland DotDot -> text dotDot

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Done -> text doneS

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Oops -> text oopsS

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Sorry -> text sorryS

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterlandinstance Pretty ProofMethod where

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland pretty = printProofMethod

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandprintProofMethod :: ProofMethod -> Doc

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah WaterlandprintProofMethod pm =

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland case pm of

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Auto -> text autoS

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Simp -> text simpS

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Induct var -> (text inductS) <+> doubleQuotes (text var)

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland CaseTac t -> text caseTacS <+> doubleQuotes (text t)

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland SubgoalTac t -> text subgoalTacS <+> doubleQuotes (text t)

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Insert t -> text insertS <+> text t

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland Other s -> parens $ text s

5c51f1241dbbdf2656d0e10011981411ed0c9673Moriah Waterland