isa-parser/Isabelle/ParseFile.hs

--
-- Copyright 2016, NICTA
--
-- This software may be distributed and modified according to the terms of
-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
-- See "LICENSE_GPLv2.txt" for details.
--
-- @TAG(NICTA_GPL)
--

module Isabelle.Main
where

-- system imports
import System.Environment
import System.Exit
import Text.Printf
import Text.Parsec
import Text.Parsec.String
import Text.PrettyPrint.ANSI.Leijen

-- friends
import Isabelle.Parser

getFile :: IO (Maybe String)
getFile = do
  args <- getArgs
  return $ case args of 
             []     -> Nothing
             file:_ -> Just file

exitOnNothing :: String -> IO (Maybe a) -> IO a
exitOnNothing errorString io = do
  mb <- io
  case mb of
    Nothing -> putStrLn errorString >> exitWith (ExitFailure 1)
    Just x  -> return x
  

parseFile :: String -> IO ()
parseFile path = do
  eRes <- parseFromFile topLevelL path
  case eRes of
    Left err  -> printf "Error parsing %s\n%s\n" path (show err)
    Right res -> putDoc $ pretty res


main :: IO ()
main = do
  file <- exitOnNothing "You must provide a file name as first argument" getFile
  parseFile file