{-# LANGUAGE ExistentialQuantification #-}
{- |
Module      :  ./GUI/HTkUtils.hs
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)

Utilities on top of HTk
-}

module GUI.HTkUtils
  ( LBGoalView (..)
  , LBStatusIndicator (..)
  , EnableWid (..)
  , GUIMVar
  , listBox
  , errorMess
  , confirmMess
  , messageMess
  , askFileNameAndSave
  , createTextSaveDisplay
  , newFileDialogStr
  , fileDialogStr
  , displayTheoryWithWarning
  , populateGoalsListBox
  , indicatorFromProofStatus
  , indicatorFromBasicProof
  , indicatorString
  , enableWids
  , disableWids
  , enableWidsUponSelection
  , module X
  ) where

import System.Directory

import Util.Messages
import HTk.Toplevel.HTk as X hiding (x, y)
import HTk.Toolkit.ScrollBox as X
import HTk.Toolkit.SimpleForm as X
import HTk.Toolkit.TextDisplay as X
import HTk.Toolkit.FileDialog

import Logic.Prover
import Static.GTheory

import Common.DocUtils

import Control.Concurrent.MVar


-- ** some types

-- | Type for storing the proof management window
type GUIMVar = MVar (Maybe Toplevel)

-- | create a window with title and list of options, return selected option
listBox :: String -> [String] -> IO (Maybe Int)
listBox title entries =
  do
    main <- createToplevel [text title]
    lb <- newListBox main [value entries, bg "white", size (100, 39)] ::
             IO (ListBox String)
    pack lb [Side AtLeft, Expand On, Fill Both]
    scb <- newScrollBar main []
    pack scb [Side AtRight, Fill Y]
    lb # scrollbar Vertical scb
    (press, _) <- bindSimple lb (ButtonPress (Just 1))
    (closeWindow, _) <- bindSimple main Destroy
    sync ( (press >>> do
              sel <- getSelection lb
              destroy main
              return (case sel of
                 Just [i] -> Just i
                 _ -> Nothing) )
      +> (closeWindow >>> do
            destroy main
            return Nothing ))

{- |
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
                         the text editor -}
                         -> IO () {- ^ action to be executed when
                         the window is closed -}
                         -> IO (Toplevel, Editor) {- ^ the window in which
                         the text is displayed -}
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 (`newEditor` conf) []
     ed # state Disabled
     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]
     ed # state Normal
     ed # value txt
     ed # state Disabled
     forceFocus ed
     (editClicked, _) <- bindSimple ed (ButtonPress (Just 1))
     quit <- clicked q
     save <- clicked s
     _ <- spawnEvent $ forever $ quit >>> (destroy win >> upost)
       +> save >>> do
           disableButs q s
           askFileNameAndSave fname txt
           enableButs q s
           done
       +> editClicked >>> forceFocus ed
     return (win, 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
                      -> IO ()
createTextSaveDisplay t f txt = do
  createTextSaveDisplayExt t f txt [size (100, 44)] done
  done

{- - added by KL

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
                   -> IO ()
askFileNameAndSave defFN txt =
    do curDir <- getCurrentDirectory
       selev <- newFileDialogStr "Save file" (curDir ++ '/' : defFN)
       mfile <- sync selev
       maybe done saveFile mfile
    where saveFile fp = writeFile fp txt

{- | returns a window displaying the given theory and the given
     warning text.
-}
displayTheoryWithWarning :: String -- ^ kind of theory
                         -> String -- ^ name of theory
                         -> String -- ^ warning text
                         -> G_theory -- ^ to be shown theory
                         -> IO ()
displayTheoryWithWarning kind thname warningTxt gth =
    let str = warningTxt ++ showDoc gth "\n"
        title = kind ++ " of " ++ thname
     in createTextSaveDisplay title (thname ++ ".het") str

{- - added by RW
Represents the state of a goal in a 'ListBox' that uses 'populateGoalsListBox'
-}
data LBStatusIndicator = LBIndicatorProved
                       | LBIndicatorProvedInconsistent
                       | LBIndicatorDisproved
                       | LBIndicatorOpen
                       | LBIndicatorGuessed
                       | LBIndicatorConjectured
                       | LBIndicatorHandwritten

{- |
Converts a 'LBStatusIndicator' into a short 'String' representing it in
a 'ListBox' -}
indicatorString :: LBStatusIndicator
                -> String
indicatorString i = case i of
  LBIndicatorProved -> "[+]"
  LBIndicatorProvedInconsistent -> "[*]"
  LBIndicatorDisproved -> "[-]"
  LBIndicatorOpen -> "[ ]"
  LBIndicatorGuessed -> "[.]"
  LBIndicatorConjectured -> "[:]"
  LBIndicatorHandwritten -> "[/]"

{- |
Represents a goal in a 'ListBox' that uses 'populateGoalsListBox' -}
data LBGoalView = LBGoalView { -- | status indicator
                               statIndicator :: LBStatusIndicator,
                               -- | description
                               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 -}
                     -> IO ()
populateGoalsListBox lb v = do
  selectedOld <- getSelection lb :: IO (Maybe [Int])
  lb # value (toString v)
  maybe (return ()) (mapM_ (`selection` lb)) selectedOld
  where
    toString = map (\ LBGoalView {statIndicator = i, goalDescription = d} ->
                        indicatorString i ++ ' ' : d)

-- | Converts a 'Logic.Prover.ProofStatus' into a 'LBStatusIndicator'
indicatorFromProofStatus :: ProofStatus a
                          -> LBStatusIndicator
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
                        -> LBStatusIndicator
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)
