Copyright | uni-bremen and DFKI |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | r.pascanu@jacobs-university.de |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
PGIP.XMLstate contains the description of the XMLstate and a function that produces such a state
- genProofStep :: String -> Element
- addPGIPMarkup :: String -> Element
- genPgipElem :: String -> Element
- genNormalResponse :: Node t => String -> t -> Element
- genErrorResponse :: Bool -> String -> Element
- addPGIPAnswer :: String -> String -> CmdlPgipState -> CmdlPgipState
- addPGIPError :: String -> CmdlPgipState -> CmdlPgipState
- addPGIPAttributes :: CmdlPgipState -> Element -> Element
- addPGIPElement :: CmdlPgipState -> Element -> CmdlPgipState
- addPGIPReady :: CmdlPgipState -> CmdlPgipState
- data CmdlPgipState = CmdlPgipState {}
- genCMDLPgipState :: Bool -> Handle -> Handle -> Int -> IO CmdlPgipState
- genPgipID :: IO String
- addToMsg :: String -> CmdlPgipState -> CmdlPgipState
- resetPGIPData :: CmdlPgipState -> CmdlPgipState
- convertPGIPDataToString :: CmdlPgipState -> String
- isRemote :: HetcatsOpts -> Bool
- sendPGIPData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
- sendMSGData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
- data CmdlXMLcommands
- = XmlExecute String
- | XmlExit
- | XmlProverInit
- | XmlAskpgip
- | XmlStartQuiet
- | XmlStopQuiet
- | XmlOpenGoal String
- | XmlCloseGoal String
- | XmlGiveUpGoal String
- | XmlUnknown String
- | XmlParseScript String
- | XmlUndo
- | XmlRedo
- | XmlForget String
- | XmlOpenTheory String
- | XmlCloseTheory String
- | XmlCloseFile String
- | XmlLoadFile String
- getRefseqNb :: String -> Maybe String
- parseXMLTree :: [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
- parseXMLElement :: Element -> Maybe CmdlXMLcommands
- parseMsg :: CmdlPgipState -> String -> [CmdlXMLcommands]
Documentation
genProofStep :: String -> Element
addPGIPMarkup :: String -> Element
adds xml structure to unstructured code
genPgipElem :: String -> Element
genNormalResponse :: Node t => String -> t -> Element
genErrorResponse :: Bool -> String -> Element
addPGIPAnswer :: String -> String -> CmdlPgipState -> CmdlPgipState
It inserts a given string into the XML packet as normal output
addPGIPError :: String -> CmdlPgipState -> CmdlPgipState
It inserts a given string into the XML packet as error output
addPGIPAttributes :: CmdlPgipState -> Element -> Element
addPGIPElement :: CmdlPgipState -> Element -> CmdlPgipState
data CmdlPgipState
State that keeps track of the comunication between Hets and the Broker
genCMDLPgipState :: Bool -> Handle -> Handle -> Int -> IO CmdlPgipState
Generates an empty CmdlPgipState
addToMsg :: String -> CmdlPgipState -> CmdlPgipState
Concatenates the input string to the message stored in the state
resetPGIPData :: CmdlPgipState -> CmdlPgipState
Resets the content of the message stored in the state
isRemote :: HetcatsOpts -> Bool
sendPGIPData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
data CmdlXMLcommands
List of all possible commands inside an XML packet
getRefseqNb :: String -> Maybe String
parseXMLTree :: [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parses the xml message creating a list of commands that it needs to execute
parseMsg :: CmdlPgipState -> String -> [CmdlXMLcommands]
Given a packet (a normal string or a xml formated string), the function converts it into a list of commands