content: {-# LANGUAGE FlexibleContexts #-}
  {- |
  Module      :  ./GUI/HTkGenericATP.hs
  Description :  Generic Prover GUI.
  Copyright   :  (c) Klaus Luettich, Rainer Grabbe, Uni Bremen 2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  needs POSIX
  
  Generic GUI for automatic theorem provers. Based upon former SPASS Prover GUI.
  -}
  
  module GUI.HTkGenericATP (genericATPgui) where
  
  import Logic.Prover
  
  import qualified Common.AS_Annotation as AS_Anno
  import qualified Data.Map as Map
  import Common.Utils (getEnvSave, readMaybe)
  import Common.Result
  
  import Data.List
  import Data.Maybe
  import qualified Control.Exception as Exception
  import qualified Control.Concurrent as Conc
  import qualified Control.Monad.Fail as Fail
  
  import HTk.Toolkit.SpinButton
  import HTk.Toolkit.Separator
  import HTk.Devices.XSelection
  import HTk.Widgets.Space
  
  import GUI.Utils
  import GUI.HTkUtils hiding (createTextSaveDisplay, createTextDisplay)
  
  import Interfaces.GenericATPState
  
  import Proofs.BatchProcessing
  
  {- |
    Utility function to set the time limit of a Config.
    For values <= 0 a default value is used.
  -}
  setTimeLimit :: Int -> GenericConfig proofTree -> GenericConfig proofTree
  setTimeLimit n c = c { timeLimit = if n > 0 then Just n else Nothing }
  
  {- |
    Utility function to set the extra options of a Config.
  -}
  setExtraOpts :: [String] -> GenericConfig proofTree -> GenericConfig proofTree
  setExtraOpts opts c = c { extraOpts = opts }
  
  -- ** Constants
  
  
  -- ** Defining the view
  
  {- |
    Colors used by the GUI to indicate the status of a goal.
  -}
  data ProofStatusColour
    -- | Proved
    = Green
    -- | Proved, but theory is inconsistent
    | Brown
    -- | Disproved
    | Red
    -- | Open
    | Black
    -- | Running
    | Blue
     deriving (Bounded, Enum, Show)
  
  {- |
    Generates a ('ProofStatusColour', 'String') tuple representing a Proved proof
    status.
  -}
  statusProved :: (ProofStatusColour, String)
  statusProved = (Green, "Proved")
  
  {- |
    Generates a ('ProofStatusColour', 'String') tuple representing a Proved
    (but inconsistent) proof status.
  -}
  statusProvedButInconsistent :: (ProofStatusColour, String)
  statusProvedButInconsistent = (Brown, "Proved/Inconsistent")
  
  {- |
    Generates a ('ProofStatusColour', 'String') tuple representing a Disproved
    proof status.
  -}
  statusDisproved :: (ProofStatusColour, String)
  statusDisproved = (Red, "Disproved")
  
  {- |
    Generates a ('ProofStatusColour', 'String') tuple representing an Open proof
    status.
  -}
  statusOpen :: (ProofStatusColour, String)
  statusOpen = (Black, "Open")
  
  {- |
    Generates a ('ProofStatusColour', 'String') tuple representing an Open proof
    status in case the time limit has been exceeded.
  -}
  statusOpenTExceeded :: (ProofStatusColour, String)
  statusOpenTExceeded = (Black, "Open (Time is up!)")
  
  {- |
    Generates a ('ProofStatusColour', 'String') tuple representing a Running proof
    status.
  -}
  statusRunning :: (ProofStatusColour, String)
  statusRunning = (Blue, "Running")
  
  {- |
    Converts a 'ProofStatus' into a ('ProofStatusColour', 'String') tuple to be
    displayed by the GUI.
  -}
  toGuiStatus :: GenericConfig proofTree -- ^ current prover configuration
              -> ProofStatus a -- ^ status to convert
              -> (ProofStatusColour, String)
  toGuiStatus cf st = case goalStatus st of
    Proved c -> if c then statusProved else statusProvedButInconsistent
    Disproved -> statusDisproved
    _ -> if timeLimitExceeded cf
                 then statusOpenTExceeded
                 else statusOpen
  
  -- | stores widgets of an options frame and the frame itself
  data OpFrame = OpFrame { ofFrame :: Frame
                         , ofTimeSpinner :: SpinButton
                         , ofTimeEntry :: Entry Int
                         , ofOptionsEntry :: Entry String
                         }
  
  {- |
    Generates a list of 'GUI.HTkUtils.LBGoalView' representations of all goals
    from a 'GenericATPState.GenericState'.
  -}
  goalsView
      :: GenericState sentence proofTree pst -- ^ current global prover state
      -> [LBGoalView] -- ^ resulting ['LBGoalView'] list
  goalsView s = map ((\ g ->
                        let cfg = Map.lookup g (configsMap s)
                            statind = maybe LBIndicatorOpen
                                       (indicatorFromProofStatus . proofStatus)
                                       cfg
                         in
                           LBGoalView {statIndicator = statind,
                                       goalDescription = g})
                    . AS_Anno.senAttr) $ goalsList s
  
  -- * GUI Implementation
  
  -- ** Utility Functions
  
  {- |
    Retrieves the value of the time limit 'Entry'. Ignores invalid input.
  -}
  getValueSafe
      :: Int       -- ^ default time limt
      -> Entry Int -- ^ time limit 'Entry'
      -> IO Int    -- ^ user-requested time limit or default for errors
  getValueSafe defaultTimeLimit timeEntry =
      Exception.catch (getValue timeEntry :: IO Int)
        $ \ e -> do
           putStrLn $ "Warning: Error " ++ show (e :: Exception.SomeException)
              ++ " was ignored"
           return defaultTimeLimit
  
  {- |
    reads passed ENV-variable and if it exists and has an Int-value this value is
    returned otherwise the value of 'batchTimeLimit' is returned.
  -}
  
  getBatchTimeLimit :: String -- ^ ENV-variable containing batch time limit
                    -> IO Int
  getBatchTimeLimit env =
      getEnvSave batchTimeLimit env readMaybe
  
  {- |
    Text displayed by the batch mode window.
  -}
  batchInfoText :: Int -- ^ batch time limt
                -> Int -- ^ total number of goals
                -> Int -- ^ number of that have been processed
                -> String
  batchInfoText tl gTotal gDone =
    let totalSecs = (gTotal - gDone) * tl
        (remMins, secs) = divMod totalSecs 60
        (hours, mins) = divMod remMins 60
    in
    "Batch mode running.\n" ++
    show gDone ++ "/" ++ show gTotal ++ " goals processed.\n" ++
    "At most " ++ show hours ++ "h " ++ show mins ++ "m " ++ show secs
    ++ "s remaining."
  
  
  -- ** Callbacks
  
  {- |
     Updates the display of the status of the current goal.
  -}
  updateDisplay
      :: GenericState sentence proofTree pst
         -- ^ current global prover state
      -> Bool -- ^ set to 'True' if you want the 'ListBox' to be updated
      -> ListBox String
         -- ^ 'ListBox' displaying the status of all goals (see 'goalsView')
      -> Label
         {- ^ 'Label' displaying the status of the currently selected goal
         (see 'toGuiStatus') -}
      -> Entry Int -- ^ 'Entry' containing the time limit of the current goal
      -> Entry String -- ^ 'Entry' containing the extra options
      -> ListBox String
         -- ^ 'ListBox' displaying all axioms used to prove a goal (if any)
      -> IO ()
  updateDisplay st updateLb goalsLb statusLabel timeEntry optionsEntry axiomsLb =
  {- the code in comments only works with an updated uni version that
     will be installed when switching to ghc-6.6.1 -}
    do
      when updateLb (do
             (offScreen, _) <- view Vertical goalsLb
             populateGoalsListBox goalsLb (goalsView st)
             moveto Vertical goalsLb offScreen
            )
      maybe (return ())
            (\ go ->
                 let mprfst = Map.lookup go (configsMap st)
                     cf = Map.findWithDefault
                          (error "GUI.GenericATP.updateDisplay")
                          go (configsMap st)
                     t' = fromMaybe guiDefaultTimeLimit (timeLimit cf)
                     opts' = unwords (extraOpts cf)
                     (color, label) = maybe statusOpen
                                      (toGuiStatus cf . proofStatus)
                                      mprfst
                     usedAxs = maybe [] (usedAxioms . proofStatus) mprfst
  
                 in do
                  statusLabel # text label
                  statusLabel # foreground (show color)
                  timeEntry # value t'
                  optionsEntry # value opts'
                  axiomsLb # value (usedAxs :: [String])
                  return ())
            (currentGoal st)
  
  newOptionsFrame
      :: Container par
      => par -- ^ the parent container
      -> (Entry Int -> Spin -> IO a)
         -- ^ Function called by pressing one spin button
      -> Bool -- ^ extra options input line
      -> IO OpFrame
  newOptionsFrame con updateFn isExtraOps = do
    right <- newFrame con []
  
    -- contents of newOptionsFrame
    l1 <- newLabel right [text "Options:"]
    pack l1 [Anchor NorthWest]
    opFrame <- newFrame right []
    pack opFrame [Expand On, Fill X, Anchor North]
  
    spacer <- newLabel opFrame [text "   "]
    pack spacer [Side AtLeft]
  
    opFrame2 <- newVBox opFrame []
    pack opFrame2 [Expand On, Fill X, Anchor NorthWest]
  
    timeLimitFrame <- newFrame opFrame2 []
    pack timeLimitFrame [Expand On, Fill X, Anchor West]
  
    l2 <- newLabel timeLimitFrame [text "TimeLimit"]
    pack l2 [Side AtLeft]
  
    -- extra HBox for time limit display
    timeLimitLine <- newHBox timeLimitFrame []
    pack timeLimitLine [Expand On, Side AtRight, Anchor East]
  
    timeEntry <- newEntry timeLimitLine [width 18,
                                         value guiDefaultTimeLimit]
    pack (timeEntry :: Entry Int) []
  
    timeSpinner <- newSpinButton timeLimitLine (updateFn timeEntry) []
    pack timeSpinner []
  
    l3 <- newLabel opFrame2 [text "Extra Options:"]
    when isExtraOps $
         pack l3 [Anchor West]
    optionsEntry <- newEntry opFrame2 [width 37]
    when isExtraOps $
         pack (optionsEntry :: Entry String) [Fill X, PadX (cm 0.1)]
  
    return OpFrame
      { ofFrame = right
      , ofTimeSpinner = timeSpinner
      , ofTimeEntry = timeEntry
      , ofOptionsEntry = optionsEntry }
  
  -- ** Main GUI
  
  {- |
    Invokes the prover GUI. Users may start the batch prover run on all goals,
    or use a detailed GUI for proving each goal manually.
  -}
  genericATPgui
      :: (Show sentence, Ord proofTree, Ord sentence)
      => ATPFunctions sign sentence mor proofTree pst
         -- ^ prover specific functions
      -> Bool   -- ^ prover supports extra options
      -> String -- ^ prover name
      -> String -- ^ theory name
      -> Theory sign sentence proofTree
         -- ^ theory with signature and sentences
      -> [FreeDefMorphism sentence mor] -- ^ freeness constraints
      -> proofTree                      -- ^ initial empty proofTree
      -> IO [ProofStatus proofTree]     -- ^ proof status for each goal
  genericATPgui atpFun isExtraOptions prName thName th freedefs pt = do
    -- create initial backing data structure
    let initState = initialGenericState prName
                                        (initialProverState atpFun)
                                        (atpTransSenName atpFun) th freedefs pt
    stateMVar <- Conc.newMVar initState
    batchTLimit <- getBatchTimeLimit $ batchTimeEnv atpFun
  
    -- main window
    main <- createToplevel [text $ thName ++ " - " ++ prName ++ " Prover"]
    pack main [Expand On, Fill Both]
  
    -- VBox for the whole window
    b <- newVBox main []
    pack b [Expand On, Fill Both]
  
    -- HBox for the upper part (goals on the left, options/results on the right)
    b2 <- newHBox b []
    pack b2 [Expand On, Fill Both]
  
    -- left frame (goals)
    left <- newFrame b2 []
    pack left [Expand On, Fill Both]
  
    b3 <- newVBox left []
    pack b3 [Expand On, Fill Both]
  
    l0 <- newLabel b3 [text "Goals:"]
    pack l0 [Anchor NorthWest]
  
    lbFrame <- newFrame b3 []
    pack lbFrame [Expand On, Fill Both]
  
    lb <- newListBox lbFrame [bg "white", exportSelection False,
                              selectMode Single, height 15] :: IO (ListBox String)
    pack lb [Expand On, Side AtLeft, Fill Both]
    sb <- newScrollBar lbFrame []
    pack sb [Expand On, Side AtRight, Fill Y, Anchor West]
    lb # scrollbar Vertical sb
  
    -- right frame (options/results)
    OpFrame { ofFrame = right
            , ofTimeSpinner = timeSpinner
            , ofTimeEntry = timeEntry
            , ofOptionsEntry = optionsEntry}
        <- newOptionsFrame b2
                   (\ timeEntry sp -> synchronize main
                     (do
                 st <- Conc.readMVar stateMVar
                 maybe noGoalSelected
                       (\ goal ->
                        do
                        curEntTL <- getValueSafe guiDefaultTimeLimit timeEntry
                        s <- Conc.takeMVar stateMVar
                        let sEnt = s {configsMap =
                                          adjustOrSetConfig
                                               (setTimeLimit curEntTL)
                                               prName goal pt (configsMap s)}
                            cfg = getConfig prName goal pt (configsMap sEnt)
                            t = timeLimit cfg
                            t' = case sp of
                                  Up -> maybe (guiDefaultTimeLimit + 10)
                                              (+ 10)
                                              t
                                  _ -> maybe (guiDefaultTimeLimit - 10)
                                              (subtract 10)
                                              t
                            s' = sEnt {configsMap =
                                           adjustOrSetConfig
                                                (setTimeLimit t')
                                                prName goal pt (configsMap sEnt)}
                        Conc.putMVar stateMVar s'
                        timeEntry # value
                                      (fromMaybe guiDefaultTimeLimit
                                      $ timeLimit $ getConfig prName goal pt
                                      $ configsMap s')
                        done)
                       (currentGoal st)))
                   isExtraOptions
    pack right [Expand On, Fill Both, Anchor NorthWest]
  
    -- buttons for options
    buttonsHb1 <- newHBox right []
    pack buttonsHb1 [Anchor NorthEast]
  
    saveProbButton <- newButton buttonsHb1 [text $ "Save "
        ++ removeFirstDot (problemOutput $ fileExtensions atpFun)
        ++ " File"]
    pack saveProbButton [Side AtLeft]
    proveButton <- newButton buttonsHb1 [text "Prove"]
    pack proveButton [Side AtRight]
  
    -- result frame
    resultFrame <- newFrame right []
    pack resultFrame [Expand On, Fill Both]
  
    l4 <- newLabel resultFrame [text ("Results:" ++ replicate 70 ' ')]
    pack l4 [Anchor NorthWest]
  
    spacer <- newLabel resultFrame [text "   "]
    pack spacer [Side AtLeft]
  
    resultContentBox <- newHBox resultFrame []
    pack resultContentBox [Expand On, Anchor West, Fill Both]
  
    -- labels on the left side
    rc1 <- newVBox resultContentBox []
    pack rc1 [Expand Off, Anchor North]
    l5 <- newLabel rc1 [text "Status"]
    pack l5 [Anchor West]
    l6 <- newLabel rc1 [text "Used Axioms"]
    pack l6 [Anchor West]
  
    -- contents on the right side
    rc2 <- newVBox resultContentBox []
    pack rc2 [Expand On, Fill Both, Anchor North]
  
    statusLabel <- newLabel rc2 [text " -- "]
    pack statusLabel [Anchor West]
    axiomsFrame <- newFrame rc2 []
    pack axiomsFrame [Expand On, Anchor West, Fill Both]
    axiomsLb <- newListBox axiomsFrame [value ([] :: [String]),
                                        bg "white", exportSelection False,
                                        selectMode Browse,
                                        height 6, width 19] :: IO (ListBox String)
    pack axiomsLb [Side AtLeft, Expand On, Fill Both]
    axiomsSb <- newScrollBar axiomsFrame []
    pack axiomsSb [Side AtRight, Fill Y, Anchor West]
    axiomsLb # scrollbar Vertical axiomsSb
  
    detailsButton <- newButton resultFrame [text "Show Details"]
    pack detailsButton [Anchor NorthEast]
  
    -- separator
    sp1 <- newSpace b (cm 0.15) []
    pack sp1 [Expand Off, Fill X, Side AtBottom]
  
    newHSeparator b
  
    sp2 <- newSpace b (cm 0.15) []
    pack sp2 [Expand Off, Fill X, Side AtBottom]
  
    -- batch mode frame
    batch <- newFrame b []
    pack batch [Expand Off, Fill X]
  
    batchTitle <- newLabel batch [text $ prName ++ " Batch Mode:"]
    pack batchTitle [Side AtTop]
  
    batchIFrame <- newFrame batch []
    pack batchIFrame [Expand On, Fill X]
  
    batchRight <- newVBox batchIFrame []
    pack batchRight [Expand On, Fill X, Side AtRight]
  
    batchBtnBox <- newHBox batchRight []
    pack batchBtnBox [Expand On, Fill X, Side AtRight]
    stopBatchButton <- newButton batchBtnBox [text "Stop"]
    pack stopBatchButton []
    runBatchButton <- newButton batchBtnBox [text "Run"]
    pack runBatchButton []
  
    batchSpacer <- newSpace batchRight (pp 150) [orient Horizontal]
    pack batchSpacer [Side AtRight]
    batchStatusLabel <- newLabel batchRight [text "\n\n"]
    pack batchStatusLabel []
  
    OpFrame { ofFrame = batchLeft
            , ofTimeSpinner = batchTimeSpinner
            , ofTimeEntry = batchTimeEntry
            , ofOptionsEntry = batchOptionsEntry}
        <- newOptionsFrame batchIFrame
                   (\ tEntry sp -> synchronize main
                     (do
                      curEntTL <- getValueSafe batchTLimit tEntry
                      let t' = case sp of
                                Up -> curEntTL + 10
                                _ -> max batchTLimit (curEntTL - 10)
                      tEntry # value t'
                      done))
                   isExtraOptions
  
    pack batchLeft [Expand On, Fill X, Anchor NorthWest, Side AtLeft]
  
    batchGoal <- newHBox batch []
    pack batchGoal [Expand On, Fill X, Anchor West, Side AtBottom]
    batchCurrentGoalTitle <- newLabel batchGoal [text "Current goal:"]
    pack batchCurrentGoalTitle []
    batchCurrentGoalLabel <- newLabel batchGoal [text "--"]
    pack batchCurrentGoalLabel []
  
  
    saveProblem_batch <- createTkVariable False
    saveProblem_batch_checkBox <-
           newCheckButton batchLeft
                        [variable saveProblem_batch,
                         text $ "Save "
                     ++ removeFirstDot (problemOutput $ fileExtensions atpFun)]
  
    enableSaveCheckBox <- getEnvSave False "HETS_ENABLE_BATCH_SAVE" readMaybe
    when enableSaveCheckBox $
         pack saveProblem_batch_checkBox [Expand Off, Fill None, Side AtBottom]
  
    batchTimeEntry # value batchTLimit
  
    -- separator 2
    sp1_2 <- newSpace b (cm 0.15) []
    pack sp1_2 [Expand Off, Fill X, Side AtBottom]
  
    newHSeparator b
  
    sp2_2 <- newSpace b (cm 0.15) []
    pack sp2_2 [Expand Off, Fill X, Side AtBottom]
  
    -- global options frame
    globalOptsFr <- newFrame b []
    pack globalOptsFr [Expand Off, Fill Both]
  
    gOptsTitle <- newLabel globalOptsFr [text "Global Options:"]
    pack gOptsTitle [Side AtTop]
  
    inclProvedThsTK <- createTkVariable True
    inclProvedThsCheckButton <-
           newCheckButton globalOptsFr
                          [variable inclProvedThsTK,
                           text ("include preceding proven therorems"
                                 ++ " in next proof attempt")]
    pack inclProvedThsCheckButton [Side AtLeft]
  
    -- separator 3
    sp1_3 <- newSpace b (cm 0.15) []
    pack sp1_3 [Expand Off, Fill X, Side AtBottom]
  
    newHSeparator b
  
    sp2_3 <- newSpace b (cm 0.15) []
    pack sp2_3 [Expand Off, Fill X, Side AtBottom]
  
    -- bottom frame (help/save/exit buttons)
    bottom <- newHBox b []
    pack bottom [Expand Off, Fill Both]
  
    helpButton <- newButton bottom [text "Help"]
    pack helpButton [PadX (cm 0.3), IPadX (cm 0.1)]  -- wider "Help" button
    saveButton <- newButton bottom [text "Save Prover Configuration"]
    pack saveButton [PadX (cm 0.3)]
    exitButton <- newButton bottom [text "Exit Prover"]
    pack exitButton [PadX (cm 0.3)]
  
    populateGoalsListBox lb (goalsView initState)
    putWinOnTop main
  
    -- MVars for thread-safe communication
    mVar_batchId <- Conc.newEmptyMVar :: IO (Conc.MVar Conc.ThreadId)
    windowDestroyedMVar <- Conc.newEmptyMVar :: IO (Conc.MVar ())
  
    -- events
    (selectGoal, _) <- bindSimple lb (ButtonPress (Just 1))
    doProve <- clicked proveButton
    saveProb <- clicked saveProbButton
    showDetails <- clicked detailsButton
  
    runBatch <- clicked runBatchButton
    stopBatch <- clicked stopBatchButton
  
    help <- clicked helpButton
    saveConfiguration <- clicked saveButton
    exit <- clicked exitButton
  
    (closeWindow, _) <- bindSimple main Destroy
  
    let goalSpecificWids = [EnW timeEntry, EnW timeSpinner, EnW optionsEntry] ++
                           map EnW [proveButton, detailsButton, saveProbButton]
        wids = EnW lb : goalSpecificWids ++
               [EnW batchTimeEntry, EnW batchTimeSpinner,
                EnW saveProblem_batch_checkBox,
                EnW batchOptionsEntry, EnW inclProvedThsCheckButton] ++
               map EnW [helpButton, saveButton, exitButton, runBatchButton]
  
    disableWids goalSpecificWids
    disable stopBatchButton
  
    -- event handlers
    _ <- spawnEvent $ forever
        $ selectGoal >>> do
            s <- Conc.takeMVar stateMVar
            let oldGoal = currentGoal s
            curEntTL <- getValueSafe guiDefaultTimeLimit timeEntry :: IO Int
            let s' = maybe s
                           (\ og -> s
                               {configsMap =
                                    adjustOrSetConfig (setTimeLimit curEntTL)
                                                      prName og pt
                                                      (configsMap s)})
                           oldGoal
            sel <- getSelection lb :: IO (Maybe [Int])
            let s'' = maybe s' (\ sg -> s' {currentGoal =
                                                Just $ AS_Anno.senAttr
                                                 (goalsList s' !! head sg)})
                               sel
            Conc.putMVar stateMVar s''
            batchModeRunning <- isBatchModeRunning mVar_batchId
            when (isJust sel && not batchModeRunning)
                 (enableWids goalSpecificWids)
            when (isJust sel) $ enableWids [EnW detailsButton, EnW saveProbButton]
            updateDisplay s'' False lb statusLabel timeEntry optionsEntry axiomsLb
            done
        +> saveProb >>> do
              rs <- Conc.readMVar stateMVar
              curEntTL <- getValueSafe guiDefaultTimeLimit
                                        timeEntry :: IO Int
              inclProvedThs <- readTkVariable inclProvedThsTK
              maybe (return ())
                    (\ goal -> do
                        let (nGoal, lp') =
                                prepareLP (proverState rs)
                                          rs goal inclProvedThs
                            s = rs {configsMap = adjustOrSetConfig
                                              (setTimeLimit curEntTL)
                                              prName goal pt
                                              (configsMap rs)}
                        extraOptions <- getValue optionsEntry :: IO String
                        let s' = s {configsMap = adjustOrSetConfig
                                              (setExtraOpts (words extraOptions))
                                              prName goal pt
                                              (configsMap s)}
  
                        prob <- goalOutput atpFun lp' nGoal $
                          createProverOptions atpFun
                            (getConfig prName goal pt $ configsMap s')
                        createTextSaveDisplay
                          (prName ++ " Problem for Goal " ++ goal)
                          (thName ++ '_' : goal
                                 ++ problemOutput (fileExtensions atpFun))
                          prob)
                    $ currentGoal rs
              done
        +> doProve >>> do
              rs <- Conc.readMVar stateMVar
              case currentGoal rs of
                Nothing -> noGoalSelected >> done
                Just goal -> do
                  curEntTL <- getValueSafe guiDefaultTimeLimit
                                            timeEntry :: IO Int
                  inclProvedThs <- readTkVariable inclProvedThsTK
                  let s = rs {configsMap = adjustOrSetConfig
                                              (setTimeLimit curEntTL)
                                              prName goal pt
                                              (configsMap rs)}
                      (nGoal, lp') = prepareLP (proverState rs)
                                          rs goal inclProvedThs
                  extraOptions <- getValue optionsEntry :: IO String
                  let s' = s {configsMap = adjustOrSetConfig
                                              (setExtraOpts (words extraOptions))
                                              prName goal pt
                                              (configsMap s)}
                  statusLabel # text (snd statusRunning)
                  statusLabel # foreground (show $ fst statusRunning)
                  disableWids wids
                  (retval, cfg) <- runProver atpFun lp'
                            (getConfig prName goal pt $ configsMap s') False
                            thName nGoal
                  -- check if window was closed
                  wDestroyed <- windowDestroyed windowDestroyedMVar
                  if wDestroyed
                   then done
                   else do
                   case retval of
                     ATPError m -> errorDialog "Error" m
                     _ -> return ()
                   let s'' = s' {
                       configsMap =
                          adjustOrSetConfig
                             (\ c -> c {timeLimitExceeded = isTimeLimitExceeded
                                                              retval,
                                        proofStatus = (proofStatus cfg)
                                             {usedTime = timeUsed cfg},
                                        resultOutput = resultOutput cfg,
                                        timeUsed = timeUsed cfg})
                             prName goal pt (configsMap s')}
                   Conc.modifyMVar_ stateMVar (return . const s'')
                  -- check again if window was closed
                   wDestroyed2 <- windowDestroyed windowDestroyedMVar
                   if wDestroyed2
                    then done
                    else do
                      enable lb
                      enable axiomsLb
                      updateDisplay s'' True lb statusLabel timeEntry
                                    optionsEntry axiomsLb
                      enableWids wids
                   done
        +> showDetails >>> do
              Conc.yield
              s <- Conc.readMVar stateMVar
              case currentGoal s of
                Nothing -> noGoalSelected >> done
                Just goal -> do
                  let result = Map.lookup goal (configsMap s)
                      output = maybe ["This goal hasn't been run through " ++
                                       "the prover yet."]
                                     resultOutput
                                     result
                      detailsText = concatMap ('\n' :) output
                  createTextSaveDisplay (prName ++ " Output for Goal " ++ goal)
                          (goal ++ proverOutput (fileExtensions atpFun))
                          (seq (length detailsText) detailsText)
                  done
        +> runBatch >>> do
              s <- Conc.readMVar stateMVar
              -- get options for this batch run
              curEntTL <- getValueSafe batchTLimit batchTimeEntry :: IO Int
              let tLimit = if curEntTL > 0 then curEntTL else batchTLimit
              batchTimeEntry # value tLimit
              extOpts <- getValue batchOptionsEntry :: IO String
              let extOpts' = words extOpts
                  openGoalsMap = filterOpenGoals $ configsMap s
                  numGoals = Map.size openGoalsMap
                  firstGoalName = fromMaybe "--" $
                                  find (`Map.member` openGoalsMap) $
                                  map AS_Anno.senAttr (goalsList s)
              if numGoals > 0
               then do
                let afterEachProofAttempt gPSF nSen nextSen cfg@(retval, _) = do
                  {- this function is called after the prover returns from a
                  proof attempt (... -> IO Bool) -}
                       cont <- goalProcessed stateMVar tLimit extOpts'
                                             numGoals prName gPSF nSen False cfg
                       Conc.tryTakeMVar mVar_batchId >>=
                         maybe (return False) (\ tId -> do
                             stored <- Conc.tryPutMVar
                                                   mVar_batchId
                                                   tId
                             if not stored
                                then Fail.fail $ "GenericATP: Thread " ++
                                            "run check failed"
                                else do
                              wDestroyed <- windowDestroyed windowDestroyedMVar
                              if wDestroyed
                                then return False
                                else do
                                 batchStatusLabel #
                                    text (if cont
                                          then batchInfoText tLimit numGoals gPSF
                                          else "Batch mode finished\n\n")
                                 setCurrentGoalLabel batchCurrentGoalLabel
                                    (if cont
                                        then maybe "--" AS_Anno.senAttr nextSen
                                        else "--")
                                 st <- Conc.readMVar stateMVar
                                 updateDisplay st True lb statusLabel timeEntry
                                              optionsEntry axiomsLb
                                 case retval of
                                  ATPError m -> errorDialog "Error" m
                                  _ -> return ()
                                 batchModeRunning <-
                                     isBatchModeRunning mVar_batchId
                                 let cont' = cont && batchModeRunning
                                 unless cont $ do
                                      disable stopBatchButton
                                      enableWids wids
                                      enableWidsUponSelection lb goalSpecificWids
                                      cleanupThread mVar_batchId
                                 return cont')
                      -- END of afterEachProofAttempt
                batchStatusLabel # text (batchInfoText tLimit numGoals 0)
                setCurrentGoalLabel batchCurrentGoalLabel firstGoalName
                disableWids wids
                enable stopBatchButton
                enableWidsUponSelection lb [EnW detailsButton, EnW saveProbButton]
                enable lb
                inclProvedThs <- readTkVariable inclProvedThsTK
                saveProblem_F <- readTkVariable saveProblem_batch
                batchProverId <- Conc.forkIO $
                  genericProveBatch False tLimit extOpts' inclProvedThs
                                        saveProblem_F
                            afterEachProofAttempt
                            (atpInsertSentence atpFun) (runProver atpFun)
                            prName thName s Nothing
                  >> return ()
                stored <- Conc.tryPutMVar mVar_batchId batchProverId
                if stored
                   then done
                   else Fail.fail "GenericATP: MVar for batchProverId already taken!!"
               else {- numGoals < 1 -} do
                batchStatusLabel # text "No further open goals\n\n"
                batchCurrentGoalLabel # text "--"
                done
        +> stopBatch >>> do
              cleanupThread mVar_batchId
              wDestroyed <- windowDestroyed windowDestroyedMVar
              if wDestroyed
                 then done
                 else do
                    disable stopBatchButton
                    enableWids wids
                    enableWidsUponSelection lb goalSpecificWids
                    batchStatusLabel # text "Batch mode stopped\n\n"
                    batchCurrentGoalLabel # text "--"
                    st <- Conc.readMVar stateMVar
                    updateDisplay st True lb statusLabel timeEntry
                                  optionsEntry axiomsLb
                    done
        +> help >>> do
              createTextDisplay (prName ++ " Help")
                                (proverHelpText atpFun)
              done
        +> saveConfiguration >>> do
              s <- Conc.readMVar stateMVar
              let cfgText = show $ printCfgText $ configsMap s
              createTextSaveDisplay
                  (prName ++ " Configuration for Theory " ++ thName)
                  (thName ++ theoryConfiguration (fileExtensions atpFun))
                  cfgText
              done
    sync $ exit >>> destroy main
        +> closeWindow >>> do
                   Conc.putMVar windowDestroyedMVar ()
                   cleanupThread mVar_batchId
                   destroy main
    s <- Conc.takeMVar stateMVar
    let Result _ proofstats = revertRenamingOfLabels s $
            map ((\ g -> let
                   res = Map.lookup g (configsMap s)
                   g' = Map.findWithDefault
                        (error ("Lookup of name failed: (1) "
                                ++ "should not happen \""
                                ++ g ++ "\""))
                        g (namesMap s)
                 in maybe (openProofStatus g' prName $ currentProofTree s)
                                proofStatus res) . AS_Anno.senAttr)
            $ goalsList s
    -- diags should not be plainly shown by putStrLn here
    maybe (Fail.fail "reverse translation of names failed") return proofstats
  
    where
      cleanupThread mVar_TId =
           Conc.tryTakeMVar mVar_TId >>= maybe (return ()) Conc.killThread
  
      windowDestroyed sMVar =
         Conc.yield >>
         Conc.tryTakeMVar sMVar >>=
           maybe (return False) (\ un -> Conc.putMVar sMVar un >> return True)
  
      isBatchModeRunning tIdMVar =
         Conc.tryTakeMVar tIdMVar >>=
          maybe (return False) (\ tId -> Conc.putMVar tIdMVar tId >> return True)
  
      noGoalSelected = errorDialog "Error" "Please select a goal first."
      prepareLP prS s goal inclProvedThs =
         let (beforeThis, afterThis) =
                splitAt (fromMaybe (error "GUI.GenericATP: goal shoud be found")
                        $ findIndex ((== goal) . AS_Anno.senAttr)
                        $ goalsList s) $ goalsList s
             proved = filter (checkGoal (configsMap s) . AS_Anno.senAttr)
                      beforeThis
         in if inclProvedThs
               then (head afterThis,
                     foldl (\ lp provedGoal ->
                       atpInsertSentence atpFun
                         lp provedGoal {AS_Anno.isAxiom = True})
                           prS
                           (reverse proved))
               else (fromMaybe (error ("GUI.GenericATP.prepareLP: Goal "
                                       ++ goal ++ " not found!!"))
                           (find ((== goal) . AS_Anno.senAttr) (goalsList s)),
                     prS)
      setCurrentGoalLabel batchLabel s = batchLabel # text (take 65 s)
      removeFirstDot [] = error "GenericATP: no extension given"
      removeFirstDot e@(h : ext) =
         case h of
              '.' -> ext
              _ -> e
  