GtkUtils.hs revision 2f1781ab0a0a58328ef9d1ad8bda1984fd80259d
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder{- |
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederModule : $Header$
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederDescription : Access to the .glade files stored as strings inside the binary
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Thiemo Wiedemeyer, Uni Bremen 2008
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederMaintainer : raider@informatik.uni-bremen.de
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : provisional
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederPortability : non-portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederThis module provides the ability to store xml stings in a temporary file to load
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederit with gtk2hs. This is needed, because gtk2hs needs glade files for input, but
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederwe want to distribute them within the binary.
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-}
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maedermodule GUI.GtkUtils
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder ( getGladeXML
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder , startMainLoop
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder , stopMainLoop
f353be6210f67ffd4a46967bba749afc968cee52Christian Maeder , forkIO_
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder , forkIOWithPostProcessing
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder -- * Windows for use inside Gtk thread
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder , infoDialog
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder , errorDialog
fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maeder , warningDialog
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder , questionDialog
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder , fileOpenDialog
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder , fileSaveDialog
d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maeder
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder , listChoiceAux
f9a73de15ef09dbd6b391c7b1f695c79b4446fe2Christian Maeder , listChoice
d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maeder
f9a73de15ef09dbd6b391c7b1f695c79b4446fe2Christian Maeder , progressBar
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder , pulseBar
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , textView
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , displayTheory
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , displayTheoryWithWarning
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- * Windows for use in Gtk windows
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , infoDialogExt
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , errorDialogExt
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , warningDialogExt
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , questionDialogExt
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder , fileOpenDialogExt
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder , fileSaveDialogExt
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder , listChoiceExt
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , progressBarExt
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder , pulseBarExt
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , textViewExt
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , displayTheoryExt
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , displayTheoryWithWarningExt
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder -- * Frequently used functions inside Gtk thread
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder , setListData
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder , updateListData
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder , setListSelectorSingle
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder , setListSelectorMultiple
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder , selectFirst
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder , getSelectedSingle
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder , getSelectedMultiple
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , selectAll
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , selectNone
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder , selectInvert
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , activate
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder -- * Datatypes and functions for prover
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , Goal (..)
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder , GStatus (..)
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder , proofStatusToGStatus
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder , basicProofToGStatus
d17834302eaa101395b4b806cd73670fd864445fChristian Maeder , genericConfigToGStatus
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder )
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder where
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maederimport Graphics.UI.Gtk
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Graphics.UI.Gtk.Glade
2dba752dedea77b7664117a46312d4a5ced6c979Christian Maeder
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maederimport qualified GUI.Glade.Utils as Utils
2dba752dedea77b7664117a46312d4a5ced6c979Christian Maeder
2dba752dedea77b7664117a46312d4a5ced6c979Christian Maederimport Static.GTheory
2dba752dedea77b7664117a46312d4a5ced6c979Christian Maeder
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederimport Common.DocUtils (showDoc)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport Control.Concurrent (forkIO)
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Control.Monad (when)
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maederimport Data.Maybe (fromMaybe)
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederimport System.Directory ( removeFile, getTemporaryDirectory, doesFileExist
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder , canonicalizePath)
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maederimport System.FilePath (takeFileName, takeDirectory)
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederimport System.IO (hFlush, hClose, hPutStr, openTempFile)
bf8221af2a4e579e1a616e3d472e9e8533cd8f8cChristian Maeder
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maederimport Logic.Prover
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Interfaces.GenericATPState
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-- | Returns a GladeXML Object of a xmlstring.
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedergetGladeXML :: (String, String) -> IO GladeXML
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedergetGladeXML (name, xmlstr) = do
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder temp <- getTemporaryDirectory
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder (filename, handle) <- openTempFile temp name
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder hPutStr handle xmlstr
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder hFlush handle
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder mxml <- xmlNew filename
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder hClose handle
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder removeFile filename
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder case mxml of
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder Just xml -> return xml
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Nothing -> error "GtkUtils: Can't load xml string."
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder-- | Starts the gtk main event loop in a thread
15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaederstartMainLoop :: IO ()
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaederstartMainLoop = forkIO_ $ do
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder unsafeInitGUIForThreadedRTS
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder mainGUI
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder
cc8b603388a7deb7fb8045db0341f550f8be5844Christian MaederstopMainLoop :: IO ()
15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaederstopMainLoop = postGUISync mainQuit
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
cc8b603388a7deb7fb8045db0341f550f8be5844Christian MaederforkIO_ :: IO () -> IO ()
cc8b603388a7deb7fb8045db0341f550f8be5844Christian MaederforkIO_ f = forkIO f >> return ()
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaederforkIOWithPostProcessing :: IO a -> (a -> IO ()) -> IO ()
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian MaederforkIOWithPostProcessing action post = forkIO_ $ do
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder result <- action
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder postGUIAsync $ post result
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder
e92ae8b45c138b6cf7db8b69e2d099d7f62f24f0Christian Maeder{- * Usefull windows and function.
d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maeder !!! IMPORTANT for all following functions !!!
f9a73de15ef09dbd6b391c7b1f695c79b4446fe2Christian Maeder Functions for use outside of the Gtk thread have a "Ext" postfix.
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder All other functions must be called from inside the Gtk thread. -}
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | Dialog for different typed messages
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdialog :: MessageType -- ^ Dialogtype
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> String -- ^ Title
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder -> String -- ^ Message
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder -> Maybe (IO()) -- ^ Action on Ok, Yes
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder -> IO Bool
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederdialog messageType title message mAction = do
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder dlg <- case messageType of
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder MessageInfo ->
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder messageDialogNew Nothing [] messageType ButtonsOk message
355a453397fa18360bbaeb0f1068ad6a299a1dffChristian Maeder MessageWarning ->
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder messageDialogNew Nothing [] messageType ButtonsYesNo message
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder MessageQuestion ->
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder messageDialogNew Nothing [] messageType ButtonsYesNo message
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder _ ->
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder messageDialogNew Nothing [] messageType ButtonsOk message
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder windowSetTitle dlg title
355a453397fa18360bbaeb0f1068ad6a299a1dffChristian Maeder
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder response <- dialogRun dlg
355a453397fa18360bbaeb0f1068ad6a299a1dffChristian Maeder choice <- case response of
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder ResponseOk -> return True
355a453397fa18360bbaeb0f1068ad6a299a1dffChristian Maeder ResponseYes -> return True
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder _ -> return False
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder widgetDestroy dlg
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder when choice $ fromMaybe (return ()) mAction
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder return choice
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder-- | create a window which displays a given text
15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaederinfoDialog :: String -- ^ Title
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder -> String -- ^ Message
20fe556546c9277cf017931a07d90add61f199d9Christian Maeder -> IO ()
20fe556546c9277cf017931a07d90add61f199d9Christian MaederinfoDialog title message = do
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder dialog MessageInfo title message Nothing
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return ()
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder-- | create a window which displays a given text
20fe556546c9277cf017931a07d90add61f199d9Christian MaederinfoDialogExt :: String -- ^ Title
20fe556546c9277cf017931a07d90add61f199d9Christian Maeder -> String -- ^ Message
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> IO ()
20fe556546c9277cf017931a07d90add61f199d9Christian MaederinfoDialogExt title = postGUISync . infoDialog title
20fe556546c9277cf017931a07d90add61f199d9Christian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | create a window which displays a given error
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaedererrorDialog :: String -- ^ Title
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder -> String -- ^ Message
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder -> IO ()
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaedererrorDialog title message = do
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder dialog MessageError title message Nothing
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return ()
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | create a window which displays a given error
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedererrorDialogExt :: String -- ^ Title
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder -> String -- ^ Message
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> IO ()
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedererrorDialogExt title = postGUISync . errorDialog title
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | create a window which displays a given warning and ask for continue
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederwarningDialog :: String -- ^ Title
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder -> String -- ^ Message
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder -> Maybe (IO ()) -- ^ Action on Ok
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder -> IO Bool
15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaederwarningDialog = dialog MessageWarning
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder-- | create a window which displays a given warning and ask for continue
15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaederwarningDialogExt :: String -- ^ Title
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> String -- ^ Message
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> Maybe (IO ()) -- ^ Action on Ok
20fe556546c9277cf017931a07d90add61f199d9Christian Maeder -> IO Bool
278de8173a1b7b7f6299f7c804135d14560176daChristian MaederwarningDialogExt title message = postGUISync . warningDialog title message
278de8173a1b7b7f6299f7c804135d14560176daChristian Maeder
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder-- | create a window which displays a given question
15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaederquestionDialog :: String -- ^ Title
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder -> String -- ^ Message
278de8173a1b7b7f6299f7c804135d14560176daChristian Maeder -> Maybe (IO ()) -- ^ Action on Yes
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder -> IO Bool
e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederquestionDialog = dialog MessageQuestion
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | create a window which displays a given question
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederquestionDialogExt :: String -- ^ Title
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder -> String -- ^ Message
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder -> Maybe (IO ()) -- ^ Action on Yes
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder -> IO Bool
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederquestionDialogExt title message = postGUISync . questionDialog title message
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder-- | Filedialog for opening and saving
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian MaederfileDialog :: FileChooserAction -- ^ Action
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> FilePath -- ^ Defaultname for file
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> [(String, [String])] -- ^ Filter (name, pattern list)
f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder -> Maybe (FilePath -> IO ()) -- ^ Action on open
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder -> IO (Maybe FilePath)
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaederfileDialog fAction fname' filters mAction = do
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder fname <- canonicalizePath fname'
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder dlg <- case fAction of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder FileChooserActionOpen -> do
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder dlg' <-fileChooserDialogNew Nothing Nothing FileChooserActionOpen
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder [ (stockCancel, ResponseCancel)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , (stockOpen, ResponseAccept)]
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder fileChooserSetCurrentFolder dlg' $ takeDirectory fname
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder fileChooserSetFilename dlg' $ takeFileName fname
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder return dlg'
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder FileChooserActionSave -> do
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder dlg' <- fileChooserDialogNew Nothing Nothing FileChooserActionSave
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder [ (stockCancel, ResponseCancel)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , (stockSave, ResponseAccept)]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder fileChooserSetCurrentFolder dlg' $ takeDirectory fname
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder fileChooserSetCurrentName dlg' $ takeFileName fname
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return dlg'
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder _ -> error "FileDialog: Wrong Type"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder mapM_ (\ (name, pattern) -> do
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder fileFilter <- fileFilterNew
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder mapM_ (fileFilterAddPattern fileFilter) pattern
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder fileFilterSetName fileFilter name
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder fileChooserAddFilter dlg fileFilter
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder ) filters
response <- dialogRun dlg
ret <- case response of
ResponseCancel -> return Nothing
ResponseAccept -> do
mpath <- fileChooserGetFilename dlg
case mpath of
Just path -> do
exist <- doesFileExist path
answer <- if exist then
dialog MessageQuestion "File already exist"
"Are you sure to overwrite existing file?" Nothing
else return True
if answer then
case mAction of
Just action -> do
action path
return mpath
Nothing -> return mpath
else return Nothing
Nothing -> return Nothing
_ -> return Nothing
widgetDestroy dlg
return ret
fileOpenDialog :: FilePath -- ^ Defaultname for file
-> [(String, [String])] -- ^ Filter (name, pattern list)
-> Maybe (FilePath -> IO ()) -- ^ Action on open
-> IO (Maybe FilePath)
fileOpenDialog = fileDialog FileChooserActionOpen
fileOpenDialogExt :: FilePath -- ^ Defaultname for file
-> [(String, [String])] -- ^ Filter (name, pattern list)
-> Maybe (FilePath -> IO ()) -- ^ Action on open
-> IO (Maybe FilePath)
fileOpenDialogExt p f = postGUISync . fileOpenDialog p f
fileSaveDialog :: FilePath -- ^ Defaultname for file
-> [(String, [String])] -- ^ Filter (name, pattern list)
-> Maybe (FilePath -> IO ()) -- ^ Action on save
-> IO (Maybe FilePath)
fileSaveDialog = fileDialog FileChooserActionSave
fileSaveDialogExt :: FilePath -- ^ Defaultname for file
-> [(String, [String])] -- ^ Filter (name, pattern list)
-> Maybe (FilePath -> IO ()) -- ^ Action on save
-> IO (Maybe FilePath)
fileSaveDialogExt p f = postGUISync . fileSaveDialog p f
-- | create a window with title and list of options, return selected option
listChoiceAux :: String -- ^ Title
-> (a -> String) -- ^ Name of element
-> [a] -- ^ Rows to display
-> IO (Maybe (Int,a)) -- ^ Selected row
listChoiceAux title showF items = do
xml <- getGladeXML Utils.get
-- get objects
dlg <- xmlGetWidget xml castToDialog "ListView"
trvList <- xmlGetWidget xml castToTreeView "trvList"
windowSetTitle dlg title
store <- setListData trvList showF items
selector <- treeViewGetSelection trvList
setListSelectorSingle trvList (return ())
mIter <- treeModelGetIterFirst store
case mIter of
Just iter -> treeSelectionSelectIter selector iter
Nothing -> return ()
dialogAddButton dlg stockCancel ResponseCancel
dialogAddButton dlg stockOk ResponseOk
response <- dialogRun dlg
ret <- case response of
ResponseCancel -> return Nothing
ResponseOk -> getSelectedSingle trvList store
_ -> return Nothing
widgetDestroy dlg
return ret
-- | create a window with title and list of options, return selected option
listChoice :: String -- ^ Title
-> [String] -- ^ Rows to display
-> IO (Maybe Int) -- ^ Selected row
listChoice title items = do
ret <- listChoiceAux title id items
return $ maybe Nothing (\ (i,_) -> Just i) ret
-- | create a window with title and list of options, return selected option
listChoiceExt :: String -- ^ Title
-> [String] -- ^ Rows to display
-> IO (Maybe Int) -- ^ Selected row
listChoiceExt title = postGUISync . listChoice title
-- | Progress/Pulse bar window
progressBarAux :: Bool -- ^ Percent or pulse
-> String -- ^ Title
-> String -- ^ Description
-> IO (Double -> String -> IO (), IO ())
progressBarAux isProgress title description = do
xml <- getGladeXML Utils.get
-- get window
window <- xmlGetWidget xml castToWindow "ProgressBar"
-- get progress bar
bar <- xmlGetWidget xml castToProgressBar "pbProgress"
windowSetTitle window title
progressBarSetText bar description
progressBarSetPulseStep bar 0.05
windowSetPosition window WinPosCenter
windowSetTypeHint window WindowTypeHintUtility
exit <- if isProgress then return (widgetDestroy window) else do
h <- timeoutAdd (do
progressBarPulse bar
return True
) 75
return (do timeoutRemove h; widgetDestroy window)
widgetShow window
let update p d = do
progressBarSetText bar d
when isProgress $ progressBarSetFraction bar p
return (update, exit)
progressBar :: String -- ^ Title
-> String -- ^ Description
-> IO (Double -> String -> IO (), IO ())
progressBar = progressBarAux True
progressBarExt :: String -- ^ Title
-> String -- ^ Description
-> IO (Double -> String -> IO (), IO ())
progressBarExt title description = do
(update, exit) <- postGUISync $ progressBar title description
return (\ a -> postGUISync . update a, postGUISync exit)
pulseBar :: String -- ^ Title
-> String -- ^ Description
-> IO (String -> IO (), IO ())
pulseBar title description = do
(update, exit) <- progressBarAux False title description
let update' = update 0
return (update', exit)
pulseBarExt :: String -- ^ Title
-> String -- ^ Description
-> IO (String -> IO (), IO ())
pulseBarExt title description = do
(update, exit) <- postGUISync $ pulseBar title description
return (postGUISync . update, postGUISync exit)
-- | Display text in an uneditable, scrollable editor. Not blocking!
textView :: String -- ^ Title
-> String -- ^ Message
-> Maybe (FilePath) -- ^ Filename
-> IO ()
textView title message mfile = do
xml <- getGladeXML Utils.get
-- get objects
dlg <- xmlGetWidget xml castToDialog "TextView"
tvText <- xmlGetWidget xml castToTextView "tvText"
windowSetTitle dlg title
buffer <- textViewGetBuffer tvText
textBufferInsertAtCursor buffer message
tagTable <- textBufferGetTagTable buffer
font <- textTagNew Nothing
set font [ textTagFont := "FreeMono" ]
textTagTableAdd tagTable font
start <- textBufferGetStartIter buffer
end <- textBufferGetEndIter buffer
textBufferApplyTag buffer font start end
case mfile of
Just file -> do
btnSave <- dialogAddButton dlg stockSave ResponseNone
onClicked btnSave $ do
fileDialog FileChooserActionSave file
[("Nothing", ["*"]), ("Text", ["*.txt"])]
$ Just (\ filepath -> writeFile filepath message)
return ()
return ()
Nothing -> return ()
btnClose <- dialogAddButton dlg stockClose ResponseNone
onClicked btnClose $ widgetDestroy dlg
widgetShow dlg
return ()
-- | Display text in an uneditable, scrollable editor. Not blocking!
textViewExt :: String -- ^ Title
-> String -- ^ Message
-> Maybe (FilePath) -- ^ Filename
-> IO ()
textViewExt title message = postGUIAsync . textView title message
-- | displays a theory in a window
displayTheory :: String -- ^ Kind of theory
-> String -- ^ Name of theory
-> G_theory -- ^ Theory
-> IO ()
displayTheory kind name gth =
textView ( kind ++ " of " ++ name) (showDoc gth "\n") $ Just $ name ++ ".het"
-- | displays a theory in a window
displayTheoryExt :: String -- ^ Kind of theory
-> String -- ^ Name of theory
-> G_theory -- ^ Theory
-> IO ()
displayTheoryExt kind name = postGUIAsync . displayTheory kind name
-- | displays a theory with warning in a window
displayTheoryWithWarning :: String -- ^ Kind of theory
-> String -- ^ Name of theory
-> String -- ^ Warning
-> G_theory -- ^ Theory
-> IO ()
displayTheoryWithWarning k n w t =
textView (k ++ " of " ++ n) (w ++ showDoc t "\n") $ Just $ n ++ ".het"
-- | displays a theory with warning in a window
displayTheoryWithWarningExt :: String -- ^ Kind of theory
-> String -- ^ Name of theory
-> String -- ^ Warning
-> G_theory -- ^ Theory
-> IO ()
displayTheoryWithWarningExt k n w =
postGUIAsync . displayTheoryWithWarning k n w
-- * Frequently used functions
-- | Setup list with single selection
setListSelectorSingle :: TreeView -> IO () -> IO ()
setListSelectorSingle view action= do
selector <- treeViewGetSelection view
treeSelectionSetMode selector SelectionSingle
onCursorChanged view action
selectFirst view
return ()
-- | Setup list with multiple selection
setListSelectorMultiple :: TreeView -> Button -> Button -> Button -> IO ()
-> IO ()
setListSelectorMultiple view btnAll btnNone btnInvert action = do
selector <- treeViewGetSelection view
treeSelectionSetMode selector SelectionMultiple
-- setup selector
onCursorChanged view action
treeSelectionSelectAll selector
-- setup buttons
onClicked btnAll $ do selectAll view; action
onClicked btnNone $ do selectNone view; action
onClicked btnInvert $ do selectInvert view; action
return ()
-- | Selects the first item if possible
selectFirst :: TreeView -> IO ()
selectFirst view = do
mModel <- treeViewGetModel view
case mModel of
Nothing -> return ()
Just model -> do
mIter <- treeModelGetIterFirst model
case mIter of
Nothing -> return ()
Just iter -> do
selector <- treeViewGetSelection view
treeSelectionSelectIter selector iter
-- | Select all rows
selectAll :: TreeView -> IO ()
selectAll view = treeViewGetSelection view >>= treeSelectionSelectAll
-- | Deselect all rows
selectNone :: TreeView -> IO ()
selectNone view = treeViewGetSelection view >>= treeSelectionUnselectAll
-- | Invert selection of list
selectInvert :: TreeView -> IO ()
selectInvert view = do
sel <- treeViewGetSelection view
selected <- treeSelectionGetSelectedRows sel
treeSelectionSelectAll sel
rows <- treeSelectionGetSelectedRows sel
mapM_ (\ row -> (if elem row selected
then treeSelectionUnselectPath else treeSelectionSelectPath) sel row
) rows
-- | Get selected item
getSelectedSingle :: TreeView -> ListStore a -> IO (Maybe (Int,a))
getSelectedSingle view list = do
mModel <- treeViewGetModel view
case mModel of
Nothing -> return Nothing
Just model -> do
selector <- treeViewGetSelection view
mIter <- treeSelectionGetSelected selector
case mIter of
Nothing -> return Nothing
Just iter -> do
path <- treeModelGetPath model iter
case path of
row:[] -> do
item <- listStoreGetValue list row
return $ Just (row, item)
_ -> error "List type not supported"
-- | Get selected items and row number
getSelectedMultiple :: TreeView -> ListStore a -> IO [(Int,a)]
getSelectedMultiple view list = do
selector <- treeViewGetSelection view
rows' <- treeSelectionGetSelectedRows selector
let rows = map head rows'
items <- mapM (listStoreGetValue list) rows
return $ zip rows items
-- | Sets data of list
setListData :: TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData view getT listData = do
store <- listStoreNew listData
treeViewSetModel view store
treeViewSetHeadersVisible view False
ren <- cellRendererTextNew
col <- treeViewColumnNew
treeViewColumnPackStart col ren True
cellLayoutSetAttributes col ren store
$ \i -> [ cellTextMarkup := Just $ getT i ]
treeViewAppendColumn view col
return store
-- | Updates data of list
updateListData :: ListStore a -> [a] -> IO ()
updateListData list listData = do
listStoreClear list
mapM_ (listStoreAppend list) listData
-- | Activates or deactivates a list of widgets
activate :: [Widget] -> Bool -> IO ()
activate widgets active = mapM_ (\ w -> widgetSetSensitive w active) widgets
-- * Datatypes and functions for prover
data Goal = Goal { gName :: String
, gStatus :: GStatus }
data GStatus = GOpen
| GTimeout
| GDisproved
| GInconsistent
| GProved
| GGuessed
| GConjectured
| GHandwritten
deriving (Eq, Ord)
instance Show Goal where
show (Goal { gName = n, gStatus = s }) = spanString s $ statusToPrefix s ++ n
instance Eq Goal where
(==) (Goal { gName = n1 }) (Goal { gName = n2 }) = n1 == n2
statusToColor :: GStatus -> String
statusToColor s = case s of
GOpen -> "black"
GProved -> "green"
GDisproved -> "red"
GTimeout -> "blue"
GInconsistent -> "orange"
GGuessed -> "darkgreen"
GConjectured -> "darkgreen"
GHandwritten -> "darkgreen"
statusToPrefix :: GStatus -> String
statusToPrefix s = case s of
GOpen -> "[ ] "
GProved -> "[+] "
GDisproved -> "[-] "
GTimeout -> "[t] "
GInconsistent -> "[*] "
GGuessed -> "[.] "
GConjectured -> "[:] "
GHandwritten -> "[/] "
spanString :: GStatus -> String -> String
spanString s m = "<span color=\"" ++ statusToColor s ++ "\">" ++ m ++ "</span>"
instance Show GStatus where
show GProved = spanString GProved "Proved"
show GInconsistent = spanString GInconsistent "Inconsistent"
show GDisproved = spanString GDisproved "Disproved"
show GOpen = spanString GOpen "Open"
show GTimeout = spanString GTimeout "Open (Timeout!)"
show GGuessed = spanString GGuessed "Guessed"
show GConjectured = spanString GConjectured "Conjectured"
show GHandwritten = spanString GHandwritten "Handwritten"
-- | Converts a ProofStatus into a GStatus
proofStatusToGStatus :: forall a . ProofStatus a -> GStatus
proofStatusToGStatus p = case goalStatus p of
Proved False -> GInconsistent
Proved True -> GProved
Disproved -> GDisproved
Open _ -> GOpen
-- | Converts a BasicProof into a GStatus
basicProofToGStatus :: BasicProof -> GStatus
basicProofToGStatus p = case p of
BasicProof _ st -> proofStatusToGStatus st
Guessed -> GGuessed
Conjectured -> GConjectured
Handwritten -> GHandwritten
-- | Converts a GenericConfig into a GStatus
genericConfigToGStatus :: GenericConfig a -> GStatus
genericConfigToGStatus cfg = case proofStatusToGStatus $ proofStatus cfg of
GOpen -> if timeLimitExceeded cfg then GTimeout else GOpen
s -> s