640b2adac05bb7f5e9fba064434c91852c3a72e6nd{- |

640b2adac05bb7f5e9fba064434c91852c3a72e6ndModule : $Header$

640b2adac05bb7f5e9fba064434c91852c3a72e6ndCopyright : (c) Heng Jiang, Klaus Luettich Uni Bremen 2004-2006

640b2adac05bb7f5e9fba064434c91852c3a72e6ndLicense : GPLv2 or higher, see LICENSE.txt

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6ndMaintainer : Christian.Maeder@dfki.de

640b2adac05bb7f5e9fba064434c91852c3a72e6ndStability : provisional

640b2adac05bb7f5e9fba064434c91852c3a72e6ndPortability : non-portable(imports Logic.Logic)

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6ndInterface for web page with WASH/CGI

640b2adac05bb7f5e9fba064434c91852c3a72e6nd-}

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6ndmodule Main where

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6ndimport WASH.CGI.CGI as CGI

640b2adac05bb7f5e9fba064434c91852c3a72e6nd

640b2adac05bb7f5e9fba064434c91852c3a72e6ndimport Driver.Options

640b2adac05bb7f5e9fba064434c91852c3a72e6ndimport Driver.WriteLibDefn

640b2adac05bb7f5e9fba064434c91852c3a72e6ndimport Driver.ReadFn

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Driver.Version

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport qualified Data.Set as Set

ef685e00a47967e27d89709461728a229d762172nd

ef685e00a47967e27d89709461728a229d762172ndimport qualified Common.Result as CRes

ef685e00a47967e27d89709461728a229d762172ndimport Common.DocUtils (showGlobalDoc)

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.GlobalAnnotations

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.LibName

51853aa2ebfdf9903a094467e1d02099f143639daaronimport Common.ResultT

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Common.PrintLaTeX

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Comorphisms.LogicGraph

b44815871de48215476ad1d4cc46d3f99da532a5erikabele

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Static.AnalysisLibrary

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Static.DevGraph

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Syntax.AS_Library

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Syntax.ToXml

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabeleimport Text.XML.Light

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

ef685e00a47967e27d89709461728a229d762172ndimport System.Random

ef685e00a47967e27d89709461728a229d762172ndimport System.IO

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport System.Time

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport System.Cmd

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport System.Posix.IO

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport System.Posix.Types

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport System.Posix.Files

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport System.Posix.Process

b44815871de48215476ad1d4cc46d3f99da532a5erikabele

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveimport Control.Monad

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- ---- Configuration section -------------------------

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- - site specific configuration

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele-- a valid email address for the contact field / link

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecontactUrl :: String

ef685e00a47967e27d89709461728a229d762172ndcontactUrl = "mailto:" ++ contactText

2a7c98db85d4969dcbe7711a5ec3264ee4fc6222yoshiki

ef685e00a47967e27d89709461728a229d762172nd-- the text displayed with the previous link

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecontactText :: String

2a7c98db85d4969dcbe7711a5ec3264ee4fc6222yoshikicontactText = "hets-devel@informatik.uni-bremen.de"

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive{- a directory which must be accessable and exposed by the web server,

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivewhere all the generated files are stored. This string must end with

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivea slash! -}

b44815871de48215476ad1d4cc46d3f99da532a5erikabelebaseDirGenerated :: String

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivebaseDirGenerated = "/home/www.informatik.uni-bremen.de/cofi/hets-tmp/"

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- path to the log file

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivelogFile :: String

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivelogFile = baseDirGenerated ++ "hets.log"

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele-- the url pointing to the above specified directory

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivebaseUrlGenerated :: String

ef685e00a47967e27d89709461728a229d762172ndbaseUrlGenerated = "http://www.informatik.uni-bremen.de/cofi/hets-tmp/"

ef685e00a47967e27d89709461728a229d762172nd

ef685e00a47967e27d89709461728a229d762172nd{- the directory where the Hets-lib repository is checked out. Must be

a27e9e05958bc51ea09edb8d8d862fe8b125313bsliveaccessable by the cgi script -}

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivecaslLibDir :: String

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivecaslLibDir = "/home/cofi/Hets-lib"

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- where is the pdflatex command for the generation of PDF-files

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivepdflatexCmd :: String

b44815871de48215476ad1d4cc46d3f99da532a5erikabelepdflatexCmd = "/opt/csw/bin/pdflatex"

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive-- - site independant configuration

a27e9e05958bc51ea09edb8d8d862fe8b125313bslive

a27e9e05958bc51ea09edb8d8d862fe8b125313bslivecofiUrl :: String

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivecofiUrl =

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx "http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/"

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx-- link to the homepage of hetcasl

ef685e00a47967e27d89709461728a229d762172ndhetcaslUrl :: String

ef685e00a47967e27d89709461728a229d762172ndhetcaslUrl = cofiUrl ++ "HetCASL/index_e.htm"

ef685e00a47967e27d89709461728a229d762172nd

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxhetsUrl :: String

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxhetsUrl = "http://www.dfki.de/sks/hets/"

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx-- link to the manual of Hets

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxhetsManualUrl :: String

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxhetsManualUrl = hetsUrl ++ "UserGuide.pdf"

b44815871de48215476ad1d4cc46d3f99da532a5erikabele

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx-- link to the hetcasl.sty file

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxhetcaslStyUrl :: String

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkxhetcaslStyUrl = hetsUrl ++ "hetcasl.sty"

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx

cd51960ffc0f49d7a9e702162ed49b3eb0909276dirkx-- ---- End of Configuration section ------------------

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickwebOpts :: HetcatsOpts

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickwebOpts = defaultHetcatsOpts

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick { outputToStdout = False

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick , libdirs = [caslLibDir]

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick , verbose = 0 }

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickdata SelectedBoxes = SB

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick { outputTree :: Bool

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick , outputTxt :: Bool

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick , outputTex :: Bool

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick , archive :: Bool

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick } deriving Show

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawickdata Output = OP

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick { asciiTxt :: String

b5468eddc0cb1691af19ddc70a6e205daf00a94ctrawick , parseTree :: String }

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabeledefaultOutput :: Output

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivedefaultOutput = OP "" ""

ef685e00a47967e27d89709461728a229d762172nd

ef685e00a47967e27d89709461728a229d762172ndnewtype RESL = RESL (CRes.Result Output)

ef685e00a47967e27d89709461728a229d762172nd

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58sliveinstance Read RESL where

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive readsPrec _ _ = error "Read for \"RESL\" not implemented!!"

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58sliveinstance Show RESL where

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive showsPrec _ _ _ = error "Show for \"RESL\" not implemented!!"

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

b44815871de48215476ad1d4cc46d3f99da532a5erikabelemain :: IO ()

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivemain = run mainCGI

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slive

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivemainCGI :: CGI ()

222f0f03c2f9ee6343c18f80f0cb6e9aad21bc58slivemainCGI = ask $ html $ do

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele CGI.head $ title $ text "Hets Web Interface"

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele CGI.body $ makeForm $ page1 $ "Hets " ++ hetcats_version

d2a771c01de1a39b6f6770d9edd8b271d8e4f10eerikabele

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabelepage1 :: String -> WithHTML x CGI ()

ef685e00a47967e27d89709461728a229d762172ndpage1 title1 = do

ef685e00a47967e27d89709461728a229d762172nd h1 $ text title1

ef685e00a47967e27d89709461728a229d762172nd p $ do

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele text "You may also want to try out our experimental "

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele hlink (URL "http://pollux.informatik.uni-bremen.de:8000/")

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele $ text "Hets Server"

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele p $ do

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele text "Enter a "

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele hlink (URL hetcaslUrl) $ text "HetCASL"

b44815871de48215476ad1d4cc46d3f99da532a5erikabele text

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele " specification or library in the input zone, then press SUBMIT:"

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele -- Input field

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele input <- p $ makeTextarea "" (attr "rows" "22" ## attr "cols" "68")

1f2a7403f1389cbf2da0a53a2b2fb425dea75506erikabele -- check box

81622596373177e079337e956f7a5800895443b3erikabele selectTxt <- checkboxInputField (attr "valus" "yes")

81622596373177e079337e956f7a5800895443b3erikabele text "output pretty print ASCII"

81622596373177e079337e956f7a5800895443b3erikabele selectTex <- checkboxInputField (attr "valus" "yes")

81622596373177e079337e956f7a5800895443b3erikabele text "output pretty print LaTeX"

ef685e00a47967e27d89709461728a229d762172nd selectTree <- checkboxInputField (attr "valus" "yes")

ef685e00a47967e27d89709461728a229d762172nd text "output xml tree"

ef685e00a47967e27d89709461728a229d762172nd selectAchiv <- p $ b $ checkboxInputField (attr "checked" "checked") ##

81622596373177e079337e956f7a5800895443b3erikabele text "If this checkbox is selected, your input will be logged!"

81622596373177e079337e956f7a5800895443b3erikabele -- submit/reset botton

81622596373177e079337e956f7a5800895443b3erikabele p $ do

81622596373177e079337e956f7a5800895443b3erikabele submit (F5 input selectTree selectTxt selectTex selectAchiv)

81622596373177e079337e956f7a5800895443b3erikabele handle (fieldVALUE "Submit")

81622596373177e079337e956f7a5800895443b3erikabele submit0 mainCGI (fieldVALUE "reset")

81622596373177e079337e956f7a5800895443b3erikabele hr_S CGI.empty

81622596373177e079337e956f7a5800895443b3erikabele p $ do

81622596373177e079337e956f7a5800895443b3erikabele text "Contact address: "

81622596373177e079337e956f7a5800895443b3erikabele hlink (URL contactUrl) $ text contactText

81622596373177e079337e956f7a5800895443b3erikabele

ef685e00a47967e27d89709461728a229d762172nd-- handle of the submit botton

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelehandle :: HasValue i => F5 (i String) (i Bool) (i Bool) (i Bool) (i Bool) VALID

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele -> CGI ()

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabelehandle (F5 input box1 box2 box3 box4) = do

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele random1 <- io $ getStdRandom $ randomR (100000, 999999)

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele processID <- io getProcessID

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele let outputfile = baseDirGenerated ++ "result" ++ show processID

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele ++ show (random1 :: Int)

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele str = CGI.value input

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele selectedBoxes = SB

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele { outputTree = CGI.value box1

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele , outputTxt = CGI.value box2

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele , outputTex = CGI.value box3

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele , archive = CGI.value box4 }

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele RESL res <- io $ fmap RESL $ anaInput str selectedBoxes outputfile

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele ask $ html $ do

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele CGI.head $ title $ text "HETS results"

f0eae6f6191f5730fa8db049f7391e93b4ff41b9erikabele CGI.body $ printR str res selectedBoxes outputfile

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki-- Analyze the input

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikianaInput :: String -> SelectedBoxes -> FilePath

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki -> IO (CRes.Result Output)

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki{-

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikianaInput contents selectedBoxes outputfiles =

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki maybe (return $ CRes.Result parseErrors Nothing) ana_ast mast

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki where

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki CRes.Result parseErrors mast =

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki readLibDefnM logicGraph webOpts "<stdin>" contents

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki-}

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshikianaInput contents selectedBoxes outputfiles = do

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki ast <- readLibDefnM logicGraph webOpts "<stdin>" contents

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki CRes.Result ds mres <- runResultT

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki $ anaLibDefn logicGraph webOpts Set.empty emptyLibEnv emptyDG ast

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki let ds1 = filter diagFilter ds

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki if CRes.hasErrors ds1

4a67c5c0053e1c1c2202122e46a42987f6fd28dfyoshiki then return $ CRes.Result ds1 Nothing

else maybe (return $ CRes.Result ds1 Nothing)

(\ res -> do

saveLog (archive selectedBoxes)

process_result ds1 res outputfiles selectedBoxes)

mres

where

diagFilter d = case CRes.diagKind d of

CRes.Hint -> False

CRes.Debug -> False

_ -> True

process_result :: [CRes.Diagnosis]

-> (LibName, LIB_DEFN, GlobalAnnos, LibEnv)

-> FilePath

-> SelectedBoxes

-> IO (CRes.Result Output)

process_result ds (_, libDefn, gannos, _) outputfile conf = do

let fMode = foldl unionFileModes nullFileMode

[ownerReadMode, ownerWriteMode,

groupReadMode, groupWriteMode,

otherReadMode]

when (outputTex conf) $ do

let pptexFile = outputfile ++ ".pp.tex"

latexFile = outputfile ++ ".tex"

pdfFile = outputfile ++ ".pdf"

tmpFile = outputfile ++ ".tmp"

writeLibDefnLatex webOpts

gannos pptexFile libDefn

writeFile latexFile (latexHeader ++

"\\input{" ++ pptexFile ++

"}\n \\end{document}\n")

setFileMode pptexFile fMode

setFileMode latexFile fMode

system ("(cd " ++ baseDirGenerated ++ " ; ls -lh " ++

pdflatexCmd ++ " ; " ++ pdflatexCmd ++ " " ++

latexFile ++ ") > " ++ tmpFile)

setFileMode pdfFile fMode

when (outputTxt conf) $ do

let txtFile = outputfile ++ ".txt"

writeFile txtFile $ showGlobalDoc gannos libDefn "\n"

setFileMode txtFile fMode

when (outputTree conf) $ do

let txtFile = outputfile ++ ".pp.xml"

writeFile txtFile $ ppTopElement $ xmlLibDefn gannos libDefn

setFileMode txtFile fMode

return (CRes.Result ds $ Just $ selectOut conf libDefn gannos)

selectOut :: SelectedBoxes -> LIB_DEFN -> GlobalAnnos -> Output

selectOut conf ld ga = defaultOutput

{ asciiTxt = if outputTxt conf then showGlobalDoc ga ld "" else ""

, parseTree = if outputTree conf then ppElement $ xmlLibDefn ga ld

else "" }

-- log file

saveLog :: Bool -> IO ()

saveLog willSave = when willSave $ do

fd <- openFd logFile ReadWrite Nothing

defaultFileFlags {append = True}

fSize <- sizeof fd

let filelock = (WriteLock, AbsoluteSeek, 0, fSize)

fileunlock = (Unlock, AbsoluteSeek, 0, fSize)

aktTime <- timeStamp

setLock fd filelock

fdWrite fd (aktTime ++ "\n" ++ contents ++ "\n\n")

setLock fd fileunlock

closeFd fd

timeStamp :: IO String

timeStamp = do

t <- getClockTime

ct <- toCalendarTime t

return $ calendarTimeToString ct

sizeof :: Fd -> IO FileOffset

sizeof fd = do

fstatus <- getFdStatus fd

return $ fileSize fstatus

catcher :: IO a -> IO String

catcher act = catch (act >> return "") (return . show)

-- Print the result

printR :: String -> CRes.Result Output -> SelectedBoxes

-> FilePath

-> WithHTML x CGI ()

printR str (CRes.Result ds mres) conf outputFile =

do h3 $ text "You have submitted the HetCASL library:"

mapM_ (\ l -> text l >> br CGI.empty) $ lines str

h3 $ text "Diagnostic messages of parsing and static analysis:"

mapM_ (\ l -> text (show l) >> br CGI.empty) ds

maybe CGI.empty printRes mres

hr_S CGI.empty

p $ do

text "Not the result you expected? Please check the "

hlink (read hetsManualUrl) $ text "Hets Manual"

text "."

hr_S CGI.empty

p $ do

text "Contact address: "

hlink (read contactUrl) $ text contactText

where

adjustOutfile ext = baseUrlGenerated ++

drop (length baseDirGenerated) (outputFile ++ ext)

printRes res = do

when (outputTxt conf) $ do

heading3 "Pretty printed text:"

formatTxt (asciiTxt res)

p $ i $ do

text "You can download the "

hlink (read $ adjustOutfile ".txt") $ text "text file"

text " here. The file will be deleted after 30 minutes.\n"

when (outputTex conf) $ do

heading3 "LaTeX code:"

p $ i $ do

text "You can download the "

hlink (read $ adjustOutfile ".pp.tex") $ text "LaTeX file"

text " here. For compiling the LaTeX output, you need "

hlink (read hetcaslStyUrl) $ text "hetcasl.sty"

text "."

p $ i $ do

text "You can also download the "

hlink (read $ adjustOutfile ".pdf") $ text "PDF file"

text ". All files will be deleted after 30 minutes.\n"

when (outputTree conf) $ do

heading3 "XML parse tree:"

formatTxt (parseTree res)

p $ i $ do

text "You can download the "

hlink (read $ adjustOutfile ".pp.xml") $ text "XML file"

text " here. The file will be deleted after 30 minutes.\n"

formatTxt = p . mapM_ (\ l -> text l >> br CGI.empty) . lines

heading3 = h3 . text