Ticket #4849: IsaParse.hs

module Isabelle.IsaParse (
          theoryBody
       ) where

import Control.Monad
import Parsec (Parser, (<|>), skipMany, space, string)

isaSkip :: Parser ()
isaSkip = skipMany space

lexS :: String -> Parser String
lexS str = (<< isaSkip) (string str)

theoryBody :: Parser String
theoryBody = lexS "wibble1"
         <|> lexS "wibble2"
         <|> lexS "wibble3"
         <|> lexS "wibble4"
         <|> lexS "wibble4"
         <|> lexS "wibble5"
         <|> lexS "wibble6"
         <|> lexS "wibble7"
         <|> lexS "wibble8"
         <|> lexS "wibbleA"
         <|> lexS "wibbleB"
         <|> lexS "wibbleC"
         <|> lexS "wibbleD"

(<<) :: Monad m => m a -> m b -> m a
(<<) = liftM2 const