| Copyright | (c) K. Luettich, Rene Wagner, Uni Bremen 2002-2005 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | luecke@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | non-portable (imports HTk) |
| Safe Haskell | None |
GUI.HTkUtils
Description
Utilities on top of HTk
- data LBGoalView = LBGoalView {}
- data LBStatusIndicator
- data EnableWid = forall wid . HasEnable wid => EnW wid
- type GUIMVar = MVar (Maybe Toplevel)
- listBox :: String -> [String] -> IO (Maybe Int)
- errorMess :: String -> IO ()
- confirmMess :: String -> IO Bool
- messageMess :: String -> IO ()
- askFileNameAndSave :: String -> String -> IO ()
- createTextSaveDisplay :: String -> String -> String -> IO ()
- newFileDialogStr :: String -> FilePath -> IO (Event (Maybe FilePath))
- fileDialogStr :: String -> FilePath -> IO (Event (Maybe FilePath))
- displayTheoryWithWarning :: String -> String -> String -> G_theory -> IO ()
- populateGoalsListBox :: ListBox String -> [LBGoalView] -> IO ()
- indicatorFromProofStatus :: ProofStatus a -> LBStatusIndicator
- indicatorFromBasicProof :: BasicProof -> LBStatusIndicator
- indicatorString :: LBStatusIndicator -> String
- enableWids :: [EnableWid] -> IO ()
- disableWids :: [EnableWid] -> IO ()
- enableWidsUponSelection :: ListBox String -> [EnableWid] -> IO ()
Documentation
data LBGoalView
Represents a goal in a ListBox that uses populateGoalsListBox
Constructors
| LBGoalView | |
Fields
| |
data LBStatusIndicator
data EnableWid
existential type for widgets that can be enabled and disabled
listBox :: String -> [String] -> IO (Maybe Int)
create a window with title and list of options, return selected option
confirmMess :: String -> IO Bool
Confirm something with the user.
messageMess :: String -> IO ()
Display some informational message.
Arguments
| :: String | title of the window |
| -> String | default filename for saving the text |
| -> String | text to be displayed |
| -> IO () |
Display some (longish) text in an uneditable, scrollable editor. Simplified version of createTextSaveDisplayExt
Arguments
| :: String | the window title of the file dialog box. |
| -> FilePath | the filepath to browse. |
| -> IO (Event (Maybe FilePath)) | An event (returning the selected FilePath if available) that is invoked when the file dialog is finished. |
Opens a file dialog box for a file which is to be created.
Arguments
| :: String | the window title of the file dialog box. |
| -> FilePath | the filepath to browse. |
| -> IO (Event (Maybe FilePath)) | An event (returning the selected FilePath if available) that is invoked when the file dialog is finished. |
Opens a file dialog box for a file which should already exist.
Arguments
| :: String | kind of theory |
| -> String | name of theory |
| -> String | warning text |
| -> G_theory | to be shown theory |
| -> IO () |
returns a window displaying the given theory and the given warning text.
Arguments
| :: ListBox String | listbox |
| -> [LBGoalView] | list of goals length must remain constant after the first call |
| -> IO () |
Populates a ListBox with goals. After the initial call to this function
the number of goals is assumed to remain constant in ensuing calls.
indicatorFromProofStatus :: ProofStatus a -> LBStatusIndicator
Converts a ProofStatus into a LBStatusIndicator
indicatorFromBasicProof :: BasicProof -> LBStatusIndicator
Converts a BasicProof into a LBStatusIndicator
indicatorString :: LBStatusIndicator -> String
Converts a LBStatusIndicator into a short String representing it in
a ListBox
enableWids :: [EnableWid] -> IO ()
disableWids :: [EnableWid] -> IO ()
enableWidsUponSelection :: ListBox String -> [EnableWid] -> IO ()
enables widgets only if at least one entry is selected in the listbox, otherwise the widgets are disabled