content: module IsabelleDecl where
  import IsabelleType(ConstsDecl,TypesDecl,DomainType,DomainDecl(..))
  import IsabelleTerm(HMatches,FixrecDecl(..))
  import IsabelleProp(PredDecl,PropDecl)
  import Mixfix
  
  -- For top level declarations:
  
  data IsaDecl
    = IsaTypes TypesDecl
    | IsaDomain DomainDecl
    | IsaConsts ConstsDecl
    | IsaFixrec FixrecDecl
    | IsaPredDecl PredDecl
    | IsaPropDecl PropDecl
    | IsaComment String
  
  data Module = Module (String, [String]) [IsaDecl]
  
  ------------------------------------------------------------
  
  instance Show IsaDecl where
    showsPrec p x = case x of
      IsaTypes d -> shows d
      IsaDomain d -> shows d
      IsaConsts d -> shows d
      IsaFixrec d -> shows d
      IsaPropDecl d -> shows d
      IsaPredDecl d -> shows d
      IsaComment s -> showLR "(*\n" "*)\n" (showString s)
  
  instance Show Module where
    showsPrec p (Module (name,imports) decls) =
      showString "theory " . showString name .
      showString "\nimports " . showSpaceSep (map showString imports) .
      showString "\nbegin\n\n" .
      showSep (showString "\n") (map shows decls) .
      showString "\nend\n"
    