module PGIP.XMLstate where
import Common.Utils (getEnvDef, trim)
import Common.ToXml
import Driver.Options
import Text.XML.Light
import Data.List (find, intercalate)
import Data.Time.Clock.POSIX (getPOSIXTime)
import System.IO (Handle, hPutStrLn, hFlush)
genProofStep :: String -> Element
genProofStep :: String -> Element
genProofStep str :: String
str = let
iname :: String
iname = case String -> String
trim String
str of
"" -> "whitespace"
'#' : _ -> "comment"
_ -> "theoryitem"
in String -> Content -> Element
forall t. Node t => String -> t -> Element
unode String
iname (Content -> Element) -> Content -> Element
forall a b. (a -> b) -> a -> b
$ String -> Content
mkText (String -> Content) -> String -> Content
forall a b. (a -> b) -> a -> b
$ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
addPGIPMarkup :: String -> Element
addPGIPMarkup :: String -> Element
addPGIPMarkup str :: String
str = case String -> [String]
lines String
str of
[] -> String -> Element
forall a. HasCallStack => String -> a
error "addPgipMarkUp.empty"
hd :: String
hd : tl :: [String]
tl ->
String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "parseresult"
([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "thyname" "whatever") (String -> Content -> Element
forall t. Node t => String -> t -> Element
unode "opentheory" (Content -> Element) -> Content -> Element
forall a b. (a -> b) -> a -> b
$ String -> Content
mkText String
hd)
Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: (String -> Element) -> [String] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map String -> Element
genProofStep [String]
tl
[Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ [String -> () -> Element
forall t. Node t => String -> t -> Element
unode "closetheory" ()]
genPgipElem :: String -> Element
genPgipElem :: String -> Element
genPgipElem = String -> Content -> Element
forall t. Node t => String -> t -> Element
unode "pgipelem" (Content -> Element) -> (String -> Content) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Content
mkText
genNormalResponse :: Node t => String -> t -> Element
genNormalResponse :: String -> t -> Element
genNormalResponse areaValue :: String
areaValue = String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "normalresponse"
(Element -> Element) -> (t -> Element) -> t -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "area" String
areaValue)
(Element -> Element) -> (t -> Element) -> t -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> t -> Element
forall t. Node t => String -> t -> Element
unode "pgml"
genErrorResponse :: Bool -> String -> Element
genErrorResponse :: Bool -> String -> Element
genErrorResponse fatality :: Bool
fatality =
[Attr] -> Element -> Element
add_attrs [ String -> String -> Attr
mkAttr "fatality" "fatal" | Bool
fatality]
(Element -> Element) -> (String -> Element) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "errorresponse"
(Element -> Element) -> (String -> Element) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Content -> Element
forall t. Node t => String -> t -> Element
unode "pgmltext" (Content -> Element) -> (String -> Content) -> String -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Content
mkText
addPGIPAnswer :: String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer :: String -> String -> CmdlPgipState -> CmdlPgipState
addPGIPAnswer msgtxt :: String
msgtxt errmsg :: String
errmsg st :: CmdlPgipState
st =
if CmdlPgipState -> Bool
useXML CmdlPgipState
st
then let resp :: CmdlPgipState
resp = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
msgtxt then CmdlPgipState
st else
CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
st (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ String -> Content -> Element
forall t. Node t => String -> t -> Element
genNormalResponse "message"
(Content -> Element) -> Content -> Element
forall a b. (a -> b) -> a -> b
$ String -> Content
mkText String
msgtxt
in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
errmsg then CmdlPgipState
resp
else CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
resp (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ Bool -> String -> Element
genErrorResponse Bool
False String
errmsg
else String -> CmdlPgipState -> CmdlPgipState
addToMsg String
errmsg (CmdlPgipState -> CmdlPgipState) -> CmdlPgipState -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ String -> CmdlPgipState -> CmdlPgipState
addToMsg String
msgtxt CmdlPgipState
st
addPGIPError :: String -> CmdlPgipState -> CmdlPgipState
addPGIPError :: String -> CmdlPgipState -> CmdlPgipState
addPGIPError str :: String
str st :: CmdlPgipState
st = case String
str of
"" -> CmdlPgipState
st
_ | CmdlPgipState -> Bool
useXML CmdlPgipState
st -> CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
st (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ Bool -> String -> Element
genErrorResponse Bool
True String
str
_ -> String -> CmdlPgipState -> CmdlPgipState
addToMsg String
str CmdlPgipState
st
addPGIPAttributes :: CmdlPgipState -> Element -> Element
addPGIPAttributes :: CmdlPgipState -> Element -> Element
addPGIPAttributes pgipData :: CmdlPgipState
pgipData e :: Element
e = ([Attr] -> Element -> Element
add_attrs
((case CmdlPgipState -> Maybe String
refSeqNb CmdlPgipState
pgipData of
Nothing -> []
Just v :: String
v -> [String -> String -> Attr
mkAttr "refseq" String
v])
[Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ [ String -> String -> Attr
mkAttr "tag" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> String
name CmdlPgipState
pgipData
, String -> String -> Attr
mkAttr "class" "pg"
, String -> String -> Attr
mkAttr "id" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> String
pgipId CmdlPgipState
pgipData
, String -> String -> Attr
mkAttr "seq" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> Int
seqNb CmdlPgipState
pgipData ])
(Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "pgip" ()) { elContent :: [Content]
elContent = [Element -> Content
Elem Element
e]}
addPGIPElement :: CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement :: CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement pgData :: CmdlPgipState
pgData el :: Element
el =
CmdlPgipState
pgData { xmlElements :: [Element]
xmlElements = CmdlPgipState -> Element -> Element
addPGIPAttributes CmdlPgipState
pgData Element
el Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: CmdlPgipState -> [Element]
xmlElements CmdlPgipState
pgData
, seqNb :: Int
seqNb = CmdlPgipState -> Int
seqNb CmdlPgipState
pgData Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
addPGIPReady :: CmdlPgipState -> CmdlPgipState
addPGIPReady :: CmdlPgipState -> CmdlPgipState
addPGIPReady pgData :: CmdlPgipState
pgData = CmdlPgipState -> Element -> CmdlPgipState
addPGIPElement CmdlPgipState
pgData (Element -> CmdlPgipState) -> Element -> CmdlPgipState
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "ready" ()
data CmdlPgipState = CmdlPgipState
{ CmdlPgipState -> String
pgipId :: String
, CmdlPgipState -> String
name :: String
, CmdlPgipState -> Int
seqNb :: Int
, CmdlPgipState -> Maybe String
refSeqNb :: Maybe String
, CmdlPgipState -> [String]
msgs :: [String]
, CmdlPgipState -> [Element]
xmlElements :: [Element]
, CmdlPgipState -> Handle
hout :: Handle
, CmdlPgipState -> Handle
hin :: Handle
, CmdlPgipState -> Bool
stop :: Bool
, CmdlPgipState -> Bool
resendMsgIfTimeout :: Bool
, CmdlPgipState -> Bool
useXML :: Bool
, CmdlPgipState -> Int
maxWaitTime :: Int }
genCMDLPgipState :: Bool -> Handle -> Handle -> Int -> IO CmdlPgipState
genCMDLPgipState :: Bool -> Handle -> Handle -> Int -> IO CmdlPgipState
genCMDLPgipState swXML :: Bool
swXML h_in :: Handle
h_in h_out :: Handle
h_out timeOut :: Int
timeOut = do
String
pgId <- IO String
genPgipID
CmdlPgipState -> IO CmdlPgipState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlPgipState :: String
-> String
-> Int
-> Maybe String
-> [String]
-> [Element]
-> Handle
-> Handle
-> Bool
-> Bool
-> Bool
-> Int
-> CmdlPgipState
CmdlPgipState
{ pgipId :: String
pgipId = String
pgId
, name :: String
name = "Hets"
, seqNb :: Int
seqNb = 1
, refSeqNb :: Maybe String
refSeqNb = Maybe String
forall a. Maybe a
Nothing
, msgs :: [String]
msgs = []
, xmlElements :: [Element]
xmlElements = []
, hin :: Handle
hin = Handle
h_in
, hout :: Handle
hout = Handle
h_out
, stop :: Bool
stop = Bool
False
, resendMsgIfTimeout :: Bool
resendMsgIfTimeout = Bool
True
, useXML :: Bool
useXML = Bool
swXML
, maxWaitTime :: Int
maxWaitTime = Int
timeOut }
genPgipID :: IO String
genPgipID :: IO String
genPgipID =
do
String
t1 <- String -> String -> IO String
getEnvDef "HOSTNAME" ""
String
t2 <- String -> String -> IO String
getEnvDef "USER" ""
POSIXTime
t3 <- IO POSIXTime
getPOSIXTime
String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ POSIXTime -> String
forall a. Show a => a -> String
show POSIXTime
t3
addToMsg :: String -> CmdlPgipState -> CmdlPgipState
addToMsg :: String -> CmdlPgipState -> CmdlPgipState
addToMsg str :: String
str pgD :: CmdlPgipState
pgD = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
str then CmdlPgipState
pgD else CmdlPgipState
pgD { msgs :: [String]
msgs = String
str String -> [String] -> [String]
forall a. a -> [a] -> [a]
: CmdlPgipState -> [String]
msgs CmdlPgipState
pgD }
resetPGIPData :: CmdlPgipState -> CmdlPgipState
resetPGIPData :: CmdlPgipState -> CmdlPgipState
resetPGIPData pgD :: CmdlPgipState
pgD = CmdlPgipState
pgD
{ msgs :: [String]
msgs = []
, xmlElements :: [Element]
xmlElements = [] }
convertPGIPDataToString :: CmdlPgipState -> String
convertPGIPDataToString :: CmdlPgipState -> String
convertPGIPDataToString =
String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String)
-> (CmdlPgipState -> [String]) -> CmdlPgipState -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String])
-> (CmdlPgipState -> [String]) -> CmdlPgipState -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element -> String) -> [Element] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Element -> String
showElement ([Element] -> [String])
-> (CmdlPgipState -> [Element]) -> CmdlPgipState -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlPgipState -> [Element]
xmlElements
isRemote :: HetcatsOpts -> Bool
isRemote :: HetcatsOpts -> Bool
isRemote opts :: HetcatsOpts
opts = HetcatsOpts -> Int
connectP HetcatsOpts
opts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= -1 Bool -> Bool -> Bool
|| HetcatsOpts -> Int
listen HetcatsOpts
opts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= -1
sendPGIPData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendPGIPData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendPGIPData opts :: HetcatsOpts
opts pgData :: CmdlPgipState
pgData =
do
let xmlMsg :: String
xmlMsg = CmdlPgipState -> String
convertPGIPDataToString CmdlPgipState
pgData
pgData' :: CmdlPgipState
pgData' = String -> CmdlPgipState -> CmdlPgipState
addToMsg String
xmlMsg CmdlPgipState
pgData
HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData HetcatsOpts
opts CmdlPgipState
pgData'
sendMSGData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData :: HetcatsOpts -> CmdlPgipState -> IO CmdlPgipState
sendMSGData opts :: HetcatsOpts
opts pgData :: CmdlPgipState
pgData = do
let msg :: String
msg = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> [String]
msgs CmdlPgipState
pgData
if HetcatsOpts -> Bool
isRemote HetcatsOpts
opts
then Handle -> String -> IO ()
hPutStrLn (CmdlPgipState -> Handle
hout CmdlPgipState
pgData) String
msg
else HetcatsOpts -> Int -> String -> IO ()
putIfVerbose HetcatsOpts
opts 1 String
msg
Handle -> IO ()
hFlush (Handle -> IO ()) -> Handle -> IO ()
forall a b. (a -> b) -> a -> b
$ CmdlPgipState -> Handle
hout CmdlPgipState
pgData
CmdlPgipState -> IO CmdlPgipState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlPgipState
pgData
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 deriving (CmdlXMLcommands -> CmdlXMLcommands -> Bool
(CmdlXMLcommands -> CmdlXMLcommands -> Bool)
-> (CmdlXMLcommands -> CmdlXMLcommands -> Bool)
-> Eq CmdlXMLcommands
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CmdlXMLcommands -> CmdlXMLcommands -> Bool
$c/= :: CmdlXMLcommands -> CmdlXMLcommands -> Bool
== :: CmdlXMLcommands -> CmdlXMLcommands -> Bool
$c== :: CmdlXMLcommands -> CmdlXMLcommands -> Bool
Eq, Int -> CmdlXMLcommands -> String -> String
[CmdlXMLcommands] -> String -> String
CmdlXMLcommands -> String
(Int -> CmdlXMLcommands -> String -> String)
-> (CmdlXMLcommands -> String)
-> ([CmdlXMLcommands] -> String -> String)
-> Show CmdlXMLcommands
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [CmdlXMLcommands] -> String -> String
$cshowList :: [CmdlXMLcommands] -> String -> String
show :: CmdlXMLcommands -> String
$cshow :: CmdlXMLcommands -> String
showsPrec :: Int -> CmdlXMLcommands -> String -> String
$cshowsPrec :: Int -> CmdlXMLcommands -> String -> String
Show)
getRefseqNb :: String -> Maybe String
getRefseqNb :: String -> Maybe String
getRefseqNb input :: String
input =
let xmlTree :: [Content]
xmlTree = String -> [Content]
forall s. XmlSource s => s -> [Content]
parseXML String
input
elRef :: Maybe Content
elRef = (Content -> Bool) -> [Content] -> Maybe Content
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ x :: Content
x -> case Content
x of
Elem dt :: Element
dt -> QName -> String
qName (Element -> QName
elName Element
dt) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "pgip"
_ -> Bool
False) [Content]
xmlTree
in case Maybe Content
elRef of
Nothing -> Maybe String
forall a. Maybe a
Nothing
Just el :: Content
el -> case Content
el of
Elem dt :: Element
dt -> case (Attr -> Bool) -> [Attr] -> Maybe Attr
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ x :: Attr
x -> QName -> String
qName (Attr -> QName
attrKey Attr
x) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "seq") ([Attr] -> Maybe Attr) -> [Attr] -> Maybe Attr
forall a b. (a -> b) -> a -> b
$
Element -> [Attr]
elAttribs Element
dt of
Nothing -> Maybe String
forall a. Maybe a
Nothing
Just elatr :: Attr
elatr -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Attr -> String
attrVal Attr
elatr
_ -> Maybe String
forall a. Maybe a
Nothing
parseXMLTree :: [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parseXMLTree :: [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parseXMLTree xmltree :: [Content]
xmltree acc :: [CmdlXMLcommands]
acc = case [Content]
xmltree of
Elem info :: Element
info : ls :: [Content]
ls -> case Element -> Maybe CmdlXMLcommands
parseXMLElement Element
info of
Just c :: CmdlXMLcommands
c -> [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parseXMLTree [Content]
ls (CmdlXMLcommands
c CmdlXMLcommands -> [CmdlXMLcommands] -> [CmdlXMLcommands]
forall a. a -> [a] -> [a]
: [CmdlXMLcommands]
acc)
Nothing -> [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parseXMLTree (Element -> [Content]
elContent Element
info [Content] -> [Content] -> [Content]
forall a. [a] -> [a] -> [a]
++ [Content]
ls) [CmdlXMLcommands]
acc
_ : ls :: [Content]
ls -> [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parseXMLTree [Content]
ls [CmdlXMLcommands]
acc
[] -> [CmdlXMLcommands]
acc
parseXMLElement :: Element -> Maybe CmdlXMLcommands
parseXMLElement :: Element -> Maybe CmdlXMLcommands
parseXMLElement info :: Element
info = let cnt :: String
cnt = Element -> String
strContent Element
info in
case QName -> String
qName (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ Element -> QName
elName Element
info of
"proverinit" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlProverInit
"proverexit" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlExit
"startquiet" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlStartQuiet
"stopquiet" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlStopQuiet
"opengoal" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlOpenGoal String
cnt
"proofstep" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
"closegoal" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlCloseGoal String
cnt
"giveupgoal" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlGiveUpGoal String
cnt
"spurioscmd" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
"dostep" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
"editobj" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
"undostep" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlUndo
"redostep" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlRedo
"forget" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlForget String
cnt
"opentheory" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlOpenTheory String
cnt
"theoryitem" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlExecute String
cnt
"closetheory" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlCloseTheory String
cnt
"closefile" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlCloseFile String
cnt
"loadfile" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlLoadFile String
cnt
"askpgip" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just CmdlXMLcommands
XmlAskpgip
"parsescript" -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlParseScript String
cnt
"pgip" -> Maybe CmdlXMLcommands
forall a. Maybe a
Nothing
s :: String
s -> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a. a -> Maybe a
Just (CmdlXMLcommands -> Maybe CmdlXMLcommands)
-> CmdlXMLcommands -> Maybe CmdlXMLcommands
forall a b. (a -> b) -> a -> b
$ String -> CmdlXMLcommands
XmlUnknown String
s
parseMsg :: CmdlPgipState -> String -> [CmdlXMLcommands]
parseMsg :: CmdlPgipState -> String -> [CmdlXMLcommands]
parseMsg st :: CmdlPgipState
st input :: String
input = if CmdlPgipState -> Bool
useXML CmdlPgipState
st
then [Content] -> [CmdlXMLcommands] -> [CmdlXMLcommands]
parseXMLTree (String -> [Content]
forall s. XmlSource s => s -> [Content]
parseXML String
input) []
else (String -> [CmdlXMLcommands]) -> [String] -> [CmdlXMLcommands]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ x :: String
x -> [ String -> CmdlXMLcommands
XmlExecute String
x | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String -> String
trim String
x ]) ([String] -> [CmdlXMLcommands]) -> [String] -> [CmdlXMLcommands]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
input