2155N/A{-# LANGUAGE ExistentialQuantification #-}
2155N/ACopyright : (c) K. Luettich, Rene Wagner, Uni Bremen 2002-2005
2155N/AMaintainer : luecke@informatik.uni-bremen.de
2155N/APortability : non-portable (imports HTk)
2155N/A-- | Type for storing the proof management window
2155N/Atype GUIMVar = MVar (Maybe Toplevel)
2155N/A-- | create a window with title and list of options, return selected option
2155N/AlistBox :: String -> [String] -> IO (Maybe Int)
2155N/A main <- createToplevel [text title]
2155N/A lb <- newListBox main [value entries, bg "white", size (100, 39)] ::
2155N/A pack lb [Side AtLeft, Expand On, Fill Both]
2155N/A scb <- newScrollBar main []
2155N/A pack scb [Side AtRight, Fill Y]
lb # scrollbar Vertical scb
(press, _) <- bindSimple lb (ButtonPress (Just 1))
(closeWindow,_) <- bindSimple main Destroy
-- Display some (longish) text in an uneditable, scrollable editor.
-- Returns immediately-- the display is forked off to separate thread.
createTextSaveDisplayExt :: String -- ^ title of the window
-> String -- ^ default filename for saving the text
-> String -- ^ text to be displayed
-> [Config Editor] -- ^ configuration options for
-> IO() -- ^ action to be executed when
-> IO (Toplevel,Editor) -- ^ the window in which
createTextSaveDisplayExt title fname txt conf upost =
do win <- createToplevel [text title]
b <- newFrame win [relief Groove, borderwidth (cm 0.05)]
t <- newLabel b [text title, font (Helvetica, Roman, 18::Int)]
q <- newButton b [text "Close", width 12]
s <- newButton b [text "Save", width 12]
(sb, ed) <- newScrollBox b (flip newEditor conf) []
pack b [Side AtTop, Fill Both,Expand On]
pack t [Side AtTop, Expand Off, PadY 10]
pack sb [Side AtTop, Expand On,Fill Both]
pack ed [Side AtTop, Expand On, Fill Both]
pack q [Side AtRight, PadX 8, PadY 5]
pack s [Side AtLeft, PadX 5, PadY 5]
(editClicked, _) <- bindSimple ed (ButtonPress (Just 1))
_ <- spawnEvent $ forever $ quit >>> (destroy win >> upost)
askFileNameAndSave fname txt
+> editClicked >>> forceFocus ed
where disableButs b1 b2 = disable b1 >> disable b2
enableButs b1 b2 = enable b1 >> enable b2
-- Display some (longish) text in an uneditable, scrollable editor.
-- Simplified version of createTextSaveDisplayExt
createTextSaveDisplay :: String -- ^ title of the window
-> String -- ^ default filename for saving the text
-> String -- ^ text to be displayed
createTextSaveDisplay t f txt = do
createTextSaveDisplayExt t f txt [size(100,44)] done
-- opens a FileDialog and saves to the selected file if OK is clicked
-- otherwise nothing happens
askFileNameAndSave :: String -- ^ default filename for saving the text
-> String -- ^ text to be saved
askFileNameAndSave defFN txt =
do curDir <- getCurrentDirectory
selev <- newFileDialogStr "Save file" (curDir ++ '/' : defFN)
maybe done saveFile mfile
where saveFile fp = writeFile fp txt
-- | displays a theory in a window
displayTheory :: String -- ^ kind of theory
-> String -- ^ name of theory
displayTheory kind thname gth =
let str = showDoc gth "\n"
title = kind ++ " of " ++ thname
in createTextSaveDisplay title (thname++".het") str
{- | returns a window displaying the given theory and the given
displayTheoryWithWarning :: String -- ^ kind of theory
-> String -- ^ name of theory
-> String -- ^ warning text
-> G_theory -- ^ to be shown theory
displayTheoryWithWarning kind thname warningTxt gth =
let str = warningTxt ++ showDoc gth "\n"
title = kind ++ " of " ++ thname
in createTextSaveDisplay title (thname++".het") str
Represents the state of a goal in a 'ListBox' that uses 'populateGoalsListBox'
data LBStatusIndicator = LBIndicatorProved
| LBIndicatorProvedInconsistent
-- Converts a 'LBStatusIndicator' into a short 'String' representing it in
indicatorString :: LBStatusIndicator
indicatorString i = case i of
LBIndicatorProved -> "[+]"
LBIndicatorProvedInconsistent -> "[*]"
LBIndicatorDisproved -> "[-]"
LBIndicatorGuessed -> "[.]"
LBIndicatorConjectured -> "[:]"
LBIndicatorHandwritten -> "[/]"
-- Represents a goal in a 'ListBox' that uses 'populateGoalsListBox'
data LBGoalView = LBGoalView { -- | status indicator
statIndicator :: LBStatusIndicator,
goalDescription :: String
-- Populates a 'ListBox' with goals. After the initial call to this function
-- the number of goals is assumed to remain constant in ensuing calls.
populateGoalsListBox :: ListBox String -- ^ listbox
-> [LBGoalView] -- ^ list of goals
-- length must remain constant after the first call
populateGoalsListBox lb v = do
selectedOld <- getSelection lb :: IO (Maybe [Int])
maybe (return ()) (mapM_ (flip selection lb)) selectedOld
toString = map (\ LBGoalView {statIndicator = i, goalDescription = d} ->
indicatorString i ++ ' ' : d)
indicatorFromProofStatus :: ProofStatus a
indicatorFromProofStatus st = case goalStatus st of
Proved c -> if c then LBIndicatorProved else LBIndicatorProvedInconsistent
Disproved -> LBIndicatorDisproved
Open _ -> LBIndicatorOpen
-- | Converts a 'BasicProof' into a 'LBStatusIndicator'
indicatorFromBasicProof :: BasicProof
indicatorFromBasicProof p = case p of
BasicProof _ st -> indicatorFromProofStatus st
Guessed -> LBIndicatorGuessed
Conjectured -> LBIndicatorConjectured
Handwritten -> LBIndicatorHandwritten
-- | existential type for widgets that can be enabled and disabled
data EnableWid = forall wid . HasEnable wid => EnW wid
enableWids :: [EnableWid] -> IO ()
enableWids = mapM_ ( \ ew -> case ew of EnW w -> enable w >> return ())
disableWids :: [EnableWid] -> IO ()
disableWids = mapM_ ( \ ew -> case ew of EnW w -> disable w >> return ())
-- | enables widgets only if at least one entry is selected in the listbox,
-- otherwise the widgets are disabled
enableWidsUponSelection :: ListBox String -> [EnableWid] -> IO ()
enableWidsUponSelection lb goalSpecificWids =
(getSelection lb :: IO (Maybe [Int])) >>=
maybe (disableWids goalSpecificWids)
(const $ enableWids goalSpecificWids)