cb6d5bbb36150e28e40794320773e779e0c25d7bChristian MaederDescription : Gtk GUI for adding a sentence
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian MaederCopyright : (c) C. Maeder DFKI GmbH 2010
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian MaederMaintainer : Christian.Maeder@dfki.de
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian MaederStability : provisional
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian MaederPortability : non-portable (imports existential types)
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian MaederThis module provides a GUI to add a sentence
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maederimport qualified GUI.Glade.TextField as TextField
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbrichtimport Static.FromXmlUtils (BasicExtResponse (..), extendByBasicSpec)
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian MaedergtkAddSentence :: GInfo -> Int -> DGraph -> IO ()
33e57f95ad297df25f3873a8e1446acde262ce1bChristian MaedergtkAddSentence gi n dg = postGUIAsync $ do
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder xml <- getGladeXML TextField.get
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder -- get objects
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder window <- xmlGetWidget xml castToWindow "TextField"
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder btnAbort <- xmlGetWidget xml castToButton "abort"
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder btnAdd <- xmlGetWidget xml castToButton "add"
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder entry <- xmlGetWidget xml castToEntry "entry"
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder let lbl = labDG dg n
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder name = getDGNodeName lbl
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder windowSetTitle window $ "Add sentence to " ++ name
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder onClicked btnAbort $ widgetDestroy window
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder onClicked btnAdd $ do
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder sen <- entryGetText entry
3d10e93f6c8a8467cc8f8bdcbacf228600cca856Christian Maeder abort <- anaSentence gi (globalAnnos dg) n lbl sen
33e57f95ad297df25f3873a8e1446acde262ce1bChristian Maeder when abort $ widgetDestroy window
cb6d5bbb36150e28e40794320773e779e0c25d7bChristian Maeder widgetShow window
33e57f95ad297df25f3873a8e1446acde262ce1bChristian MaedererrorFeedback :: Bool -> String -> IO Bool
33e57f95ad297df25f3873a8e1446acde262ce1bChristian MaedererrorFeedback abort msg =
b6728819add93c157d17f1719d6bf94c462f7b0fChristian Maeder errorDialog "Error" msg >> return abort
3d10e93f6c8a8467cc8f8bdcbacf228600cca856Christian MaederanaSentence :: GInfo -> GlobalAnnos -> Int -> DGNodeLab -> String -> IO Bool
3d10e93f6c8a8467cc8f8bdcbacf228600cca856Christian MaederanaSentence gi ga n lbl sen = case extendByBasicSpec ga sen $ dgn_theory lbl of
50dc4ddf772893ad09019b3b39d2e4feb8486638Christian Maeder (Success gTh num _ sameSig, str)
50dc4ddf772893ad09019b3b39d2e4feb8486638Christian Maeder | not sameSig -> errorFeedback False $ "signature must not change\n" ++ str
50dc4ddf772893ad09019b3b39d2e4feb8486638Christian Maeder | num < 1 -> errorFeedback False "no sentence recognized"
50dc4ddf772893ad09019b3b39d2e4feb8486638Christian Maeder | num > 1 -> errorFeedback False $ "multiple sentences recognized\n" ++ str
50dc4ddf772893ad09019b3b39d2e4feb8486638Christian Maeder | otherwise -> do
50dc4ddf772893ad09019b3b39d2e4feb8486638Christian Maeder addSentence gi n lbl gTh
50dc4ddf772893ad09019b3b39d2e4feb8486638Christian Maeder (Failure b, str) -> errorFeedback b str
b6728819add93c157d17f1719d6bf94c462f7b0fChristian MaederaddSentence :: GInfo -> Int -> DGNodeLab -> G_theory -> IO ()
b6728819add93c157d17f1719d6bf94c462f7b0fChristian MaederaddSentence gi n lbl th = do
b6728819add93c157d17f1719d6bf94c462f7b0fChristian Maeder let ln = libName gi
b6728819add93c157d17f1719d6bf94c462f7b0fChristian Maeder iSt = intState gi
b6728819add93c157d17f1719d6bf94c462f7b0fChristian Maeder ost <- readIORef iSt
04391313ab10a1fd428d8f23188a2adf77c80611Christian Maeder let (ost', hist) = updateNodeProof ln ost (n, lbl) th
b6728819add93c157d17f1719d6bf94c462f7b0fChristian Maeder writeIORef iSt ost'
04391313ab10a1fd428d8f23188a2adf77c80611Christian Maeder runAndLock gi $ updateGraph gi hist