content: {- |
  Module      :  ./GUI/HTkProofDetails.hs
  Description :  GUI for showing and saving proof details.
  Copyright   :  (c) Rainer Grabbe 2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  needs POSIX
  
  Additional window used by 'GUI.ProofManagement' for displaying proof details.
  -}
  
  module GUI.HTkProofDetails (doShowProofDetails) where
  
  import qualified Common.Doc as Pretty
  import qualified Common.OrderedMap as OMap
  import Common.AS_Annotation
  
  import qualified Data.Map as Map
  import Data.Maybe
  import Data.List
  import Data.IORef
  
  import GUI.Utils (fileSaveDialog)
  
  import System.Directory
  
  import GUI.HTkUtils
  
  import Proofs.AbstractState
  import Logic.Comorphism
  import Logic.Prover
  import Static.GTheory
  
  -- * record structures and basic functions for handling
  
  {- |
    Record structure containing proof details for a single proof.
  -}
  data GoalDescription = GoalDescription {
      proverInfo :: String, -- ^ standard proof details
      tacticScriptText :: OpenText, -- ^ more details for tactic script
      proofTreeText :: OpenText -- ^ more details for proof tree
      }
  
  {- |
    Current state of a text tag providing additional information. The text can be
    folded or unfolded.
  -}
  data OpenText = OpenText {
      additionalText :: String, -- ^ additional information
      textShown :: Bool, -- ^ if true, text is unfolded (default: false)
      textStartPosition :: Position -- ^ start position in editor widget
      }
  
  {- |
    Creates an initial 'GoalDescription' filled with just the standard prover
    info.
  -}
  emptyGoalDescription :: String -- ^ information about the used prover
                       -> GoalDescription -- ^ initiated GoalDescription
  emptyGoalDescription st =
      GoalDescription {
        proverInfo = st,
        tacticScriptText = emptyOpenText,
        proofTreeText = emptyOpenText }
  
  {- |
    Creates an empty 'OpenText' with start position (0,0).
  -}
  emptyOpenText :: OpenText
  emptyOpenText = OpenText {
        additionalText = "",
        textShown = False,
        textStartPosition = (Distance 0, Distance 0) }
  
  -- | Determines the kind of content of a 'HTk.TextTag'.
  data Content = TacticScriptText | ProofTreeText deriving Eq
  
  
  -- * GUI for show proof details
  
  -- ** help functions
  
  -- | Return number of new lines in a string.
  numberOfLines :: String
                -> Int
  numberOfLines =
      foldr (\ ch -> if ch == '\n' then (+ 1) else id) 0
  
  {- |
    Change the x-value of a 'Position' by a given arithmetical function and value.
  -}
  changePosition :: (Int -> Int -> Int)  -- ^ mostly add or subtract values
                 -> Int -- ^ (difference) value
                 -> Position -- ^ old position
                 -> Position -- ^ changed position with new x-value
  changePosition f diff (Distance posX, Distance posY) =
      (Distance $ f posX diff, Distance posY)
  
  {- |
    Indentation of a 'String' (also multiple lines) by a number of spaces.
  -}
  indent :: Int -- ^ number of spaces
         -> String -- ^ input String
         -> Pretty.Doc -- ^ output document
  indent numSp st =
    Pretty.text (replicate numSp ' ') <>
      (Pretty.vcat . map Pretty.text . lines) st
  
  {- |
    Standard indent width.
  -}
  stdIndent :: Int
  stdIndent = 4
  
  {- |
    An item of thmStatus will be put into 'GoalDescription' structure.
    Pretty printing of proof details, adding additional information
    for text tags.
  -}
  fillGoalDescription :: (AnyComorphism, BasicProof)
                      -> GoalDescription -- ^ contents in pretty format
  fillGoalDescription (cmo, basicProof) =
      let gd = indent stdIndent $ show $ printCmWStat (cmo, basicProof)
          stat str = Pretty.text "Status:" Pretty.<+> Pretty.text str
          printCmWStat (c, bp) =
              Pretty.text "Com:" Pretty.<+> Pretty.text (show c)
              Pretty.$+$ indent stdIndent (show $ printBP bp)
          printBP bp = case bp of
                       BasicProof _ ps ->
                        stat (show $ goalStatus ps) Pretty.$+$
                        (case goalStatus ps of
                         Proved _ -> Pretty.text "Used axioms:" Pretty.<+>
                             Pretty.fsep (Pretty.punctuate Pretty.comma
                               $ map (Pretty.text . show) $ usedAxioms ps)
                             Pretty.$+$ Pretty.text "Used time:" Pretty.<+>
                                   Pretty.text (show $ usedTime ps)
                         _ -> Pretty.empty)
                        Pretty.$+$ Pretty.text "Prover:" Pretty.<+>
                              Pretty.text (usedProver ps)
                       otherProof -> stat (show otherProof)
          printTS bp = case bp of
                       BasicProof _ ps ->
                         indent (2 * stdIndent) $ (\ (TacticScript xs) -> xs) $
                                                  tacticScript ps
                       _ -> Pretty.empty
          printPT bp = case bp of
                       BasicProof _ ps ->
                         indent (2 * stdIndent) $ show $ proofTree ps
                       _ -> Pretty.empty
      in (emptyGoalDescription $ show gd) {
             tacticScriptText = emptyOpenText {
               additionalText = show $ printTS basicProof },
             proofTreeText = emptyOpenText {
               additionalText = show $ printPT basicProof } }
  
  {- |
    Gets real 'EndOfText' index at the char position after (in x-direction)
    the last written text. This is because 'EndOfText' only gives a value where a
    text would be after an imaginary newline.
  -}
  getRealEndOfTextIndex :: Editor -- ^ the editor whose end index is determined
                        -> IO Position -- ^ position behind last char in widget
  getRealEndOfTextIndex ed = do
      (Distance eotX, _) <- getIndexPosition ed EndOfText
      lineBefore <- getTextLine ed $ IndexPos (Distance (eotX - 1), 0)
      return (Distance eotX - 1, Distance $ length lineBefore)
  
  {- |
    For a given Ordered Map containing all proof values, this function adapts the
    text positions lying behind after a given reference position. This is called
    when a position in the text is moved after clicking a text tag button.
  -}
  adaptTextPositions :: (Int -> Int -> Int)  -- ^ mostly add or subtract values
                     -> Int -- ^ (difference) value
                     -> Position -- ^ reference Position
                     -> OMap.OMap (String, Int) GoalDescription
                        -- ^ Map for all proofs
                     -> OMap.OMap (String, Int) GoalDescription -- ^ adapted Map
  adaptTextPositions f diff pos =
      OMap.map $ \ gDesc ->
        let tst = tacticScriptText gDesc
            ptt = proofTreeText gDesc
        in gDesc {
             tacticScriptText = if textStartPosition tst > pos
                 then tst { textStartPosition = changePosition f diff $
                                  textStartPosition tst }
                 else tst,
             proofTreeText = if textStartPosition ptt > pos
                 then ptt { textStartPosition = changePosition f diff $
                                  textStartPosition ptt }
                 else ptt }
  
  -- ** main GUI
  
  {- |
    Called whenever the button /Show proof details/ is clicked.
  -}
  doShowProofDetails :: ProofState -> IO ()
  doShowProofDetails prGUISt =
     do
      let thName = theoryName prGUISt
          winTitleStr = "Proof Details of Selected Goals from Theory " ++ thName
      win <- createToplevel [text winTitleStr]
      bFrame <- newFrame win [relief Groove, borderwidth (cm 0.05)]
      winTitle <- newLabel bFrame [text winTitleStr,
                                    font (Helvetica, Roman, 18 :: Int)]
      btnBox <- newHBox bFrame []
      tsBut <- newButton btnBox [text expand_tacticScripts, width 18]
      ptBut <- newButton btnBox [text expand_proofTrees, width 18]
      sBut <- newButton btnBox [text "Save", width 12]
      qBut <- newButton btnBox [text "Close", width 12]
      pack winTitle [Side AtTop, Expand Off, PadY 10]
  
      (sb, ed) <- newScrollBox bFrame
          (`newEditor` [state Normal, size (80, 40)]) []
      ed # state Disabled
      pack bFrame [Side AtTop, Expand On, Fill Both]
      pack sb [Side AtTop, Expand On, Fill Both]
      pack ed [Side AtTop, Expand On, Fill Both]
  
      pack btnBox [Side AtTop, Expand On, Fill X]
      pack tsBut [PadX 5, PadY 5]
      pack ptBut [PadX 5, PadY 5]
      pack sBut [PadX 5, PadY 5]
      pack qBut [PadX 8, PadY 5]
      G_theory _ _ _ _ sSens _ <- return $ selectedTheory prGUISt
      let sttDesc = "Tactic script"
          sptDesc = "Proof tree"
          sens = OMap.filter (not . isAxiom) sSens
          elementMap = foldr insertSenSt Map.empty (reverse $ OMap.toList sens)
          insertSenSt (gN, st) resOMap =
              foldl (flip $ \ (s2, ind) -> OMap.insert (gN, ind) $
                                                       fillGoalDescription s2)
                resOMap $
                 zip (sortBy (\ (_, a) (_, b) -> compare a b) $ thmStatus st)
                     [(0 :: Int) ..]
  
      stateRef <- newIORef elementMap
      ed # state Normal
      mapM_ (\ ((gName, ind), goalDesc) -> do
          when (ind == 0) $
            appendText ed $ replicate 75 '-' ++ "\n" ++ gName ++ "\n"
          appendText ed $ proverInfo goalDesc ++ "\n"
          opTextTS <- addTextTagButton sttDesc (tacticScriptText goalDesc)
                         TacticScriptText ed (gName, ind) stateRef
          opTextPT <- addTextTagButton sptDesc (proofTreeText goalDesc)
                         ProofTreeText ed (gName, ind) stateRef
          appendText ed "\n"
          let goalDesc' = goalDesc { tacticScriptText = opTextTS,
                                    proofTreeText = opTextPT }
          modifyIORef stateRef (OMap.update (\ _ -> Just goalDesc') (gName, ind))
        ) $ OMap.toList elementMap
  
      ed # state Disabled
  
      (editClicked, _) <- bindSimple ed (ButtonPress (Just 1))
      quit <- clicked qBut
      save <- clicked sBut
      toggleTacticScript <- clicked tsBut
      toggleProofTree <- clicked ptBut
      btnState <- newIORef (False, False)
      _ <- spawnEvent $ forever
          $ quit >>> destroy win
          +> save >>> do
            disable qBut
            disable sBut
            curDir <- getCurrentDirectory
            let f = curDir ++ '/' : thName ++ "-proof-details.txt"
            mfile <- fileSaveDialog f [ ("Text", ["*.txt"])
                                      , ("All Files", ["*"])] Nothing
            maybe done (writeTextToFile ed) mfile
            enable qBut
            enable sBut
            done
          +> toggleTacticScript >>> do
               (expTS, expPT) <- readIORef btnState
               tsBut # text (if expTS then expand_tacticScripts
                                      else hide_tacticScripts)
               toggleMultipleTags TacticScriptText expTS ed stateRef
               writeIORef btnState (not expTS, expPT)
          +> toggleProofTree >>> do
               (expTS, expPT) <- readIORef btnState
               ptBut # text (if expPT then expand_proofTrees
                                      else hide_proofTrees)
               toggleMultipleTags ProofTreeText expPT ed stateRef
               writeIORef btnState (expTS, not expPT)
          +> editClicked >>> forceFocus ed
      return ()
    where
      expand_tacticScripts = "Expand tactic scripts"
      expand_proofTrees = "Expand proof trees"
      hide_tacticScripts = "Hide tactic scripts"
      hide_proofTrees = "Hide proof trees"
  
  {- |
    Toggle all 'TextTag's of one kind to the same state (visible or invisible),
    either tactic script or proof tree.
  -}
  toggleMultipleTags :: Content -- ^ kind of text tag to toggle
                     -> Bool -- ^ current visibility state
                     -> Editor
                        -- ^ editor window to which button will be attached
                     -> IORef (OMap.OMap (String, Int) GoalDescription)
                        -- ^ current state of all proof descriptions
                     -> IO ()
  toggleMultipleTags content expanded ed stateRef = do
      s <- readIORef stateRef
      mapM_ (\ (dKey, goalDesc) -> do
          let openText = if content == TacticScriptText
                           then tacticScriptText goalDesc
                           else proofTreeText goalDesc
          when (textShown openText == expanded)
               (toggleTextTag content ed dKey stateRef)
        ) $ OMap.toList s
      done
  
  {- |
    This functions toggles the state from a given TextTag from visible to
    invisible or vice versa. This depends on the current state in the ordered map
    of goal descriptions. First parameter indicates whether the tactic script
    or the proof tree text from a goal description will be toggled.
  -}
  toggleTextTag :: Content -- ^ kind of text tag to toggle
                -> Editor -- ^ editor window to which button will be attached
                -> (String, Int) {- ^ key in single proof descriptions
                                 (goal name and index) -}
                -> IORef (OMap.OMap (String, Int) GoalDescription)
                   -- ^ current state of all proof descriptions
                -> IO ()
  toggleTextTag content ed (gName, ind) stateRef = do
      s <- readIORef stateRef
      let gd = fromMaybe (emptyGoalDescription gName)
               $ OMap.lookup (gName, ind) s
          openText = if content == TacticScriptText then tacticScriptText gd
                                                      else proofTreeText gd
          tsp = textStartPosition openText
          nol = numberOfLines (additionalText openText)
      if not $ textShown openText then do
          ed # state Normal
          insertText ed tsp $ additionalText openText
          ed # state Disabled
          done
        else do
          ed # state Normal
          deleteTextRange ed tsp $ changePosition (+) nol tsp
          ed # state Disabled
          done
      let openText' = openText { textShown = not $ textShown openText }
          s' = OMap.update
                   (\ _ -> Just $ if content == TacticScriptText
                            then gd { tacticScriptText = openText' }
                            else gd { proofTreeText = openText' } )
                   (gName, ind) s
      writeIORef stateRef $ adaptTextPositions
           (if textShown openText then (-) else (+))
           nol tsp s'
  
  {- |
    A button in form of a text tag will be added to the specified editor window.
    The events for clicking on a button are set up: adding or removing
    additional text lines by alternately clicking. All positions of text lying
    behind have to be adapted.
    The current state of text tags is stored and modified in 'IORef'.
    Initial call of this function returns an 'OpenText' containing the status of
    the added text tag button.
  -}
  addTextTagButton :: String -- ^ caption for button
                   -> OpenText -- ^ conatins text to be outfolded if clicked
                   -> Content -- ^ either text from tacticScript or proofTree
                   -> Editor -- ^ editor window to which button will be attached
                   -> (String, Int) {- ^ key in single proof descriptions
                                    (goal name and index) -}
                   -> IORef (OMap.OMap (String, Int) GoalDescription)
                      -- ^ current state of all proof descriptions
                   -> IO OpenText -- ^ information about OpenText status
  addTextTagButton cap addText content ed dKey stateRef = do
      appendText ed $ replicate (2 * stdIndent) ' '
      curPosStart <- getRealEndOfTextIndex ed
      appendText ed cap
      curPosEnd <- getRealEndOfTextIndex ed
      insertNewline ed
      ttag <- createTextTag ed curPosStart curPosEnd [underlined On]
  
      (selectTextTag, _) <- bindSimple ttag (ButtonPress (Just 1))
      (enterTT, _) <- bindSimple ttag Enter
      (leaveTT, _) <- bindSimple ttag Leave
      _ <- spawnEvent $ forever
                     $ selectTextTag >>> toggleTextTag content ed dKey stateRef
                     +> enterTT >>> do
                       ed # cursor hand2
                       done
                     +> leaveTT >>> do
                       ed # cursor xterm
                       done
      return OpenText {additionalText = "\n" ++ additionalText addText ++ "\n",
                       textShown = False,
                       textStartPosition = curPosEnd}
  