{- |
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 {
    GoalDescription -> String
proverInfo :: String, -- ^ standard proof details
    GoalDescription -> OpenText
tacticScriptText :: OpenText, -- ^ more details for tactic script
    GoalDescription -> OpenText
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 {
    OpenText -> String
additionalText :: String, -- ^ additional information
    OpenText -> Bool
textShown :: Bool, -- ^ if true, text is unfolded (default: false)
    OpenText -> Position
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 :: String -> GoalDescription
emptyGoalDescription st :: String
st =
    GoalDescription :: String -> OpenText -> OpenText -> GoalDescription
GoalDescription {
      proverInfo :: String
proverInfo = String
st,
      tacticScriptText :: OpenText
tacticScriptText = OpenText
emptyOpenText,
      proofTreeText :: OpenText
proofTreeText = OpenText
emptyOpenText }

{- |
  Creates an empty 'OpenText' with start position (0,0).
-}
emptyOpenText :: OpenText
emptyOpenText :: OpenText
emptyOpenText = OpenText :: String -> Bool -> Position -> OpenText
OpenText {
      additionalText :: String
additionalText = "",
      textShown :: Bool
textShown = Bool
False,
      textStartPosition :: Position
textStartPosition = (Int -> Distance
Distance 0, Int -> Distance
Distance 0) }

-- | Determines the kind of content of a 'HTk.TextTag'.
data Content = TacticScriptText | ProofTreeText deriving Content -> Content -> Bool
(Content -> Content -> Bool)
-> (Content -> Content -> Bool) -> Eq Content
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Content -> Content -> Bool
$c/= :: Content -> Content -> Bool
== :: Content -> Content -> Bool
$c== :: Content -> Content -> Bool
Eq


-- * GUI for show proof details

-- ** help functions

-- | Return number of new lines in a string.
numberOfLines :: String
              -> Int
numberOfLines :: String -> Int
numberOfLines =
    (Char -> Int -> Int) -> Int -> String -> Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ch :: Char
ch -> if Char
ch Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '\n' then (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) else Int -> Int
forall a. a -> a
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 :: (Int -> Int -> Int) -> Int -> Position -> Position
changePosition f :: Int -> Int -> Int
f diff :: Int
diff (Distance posX :: Int
posX, Distance posY :: Int
posY) =
    (Int -> Distance
Distance (Int -> Distance) -> Int -> Distance
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int
f Int
posX Int
diff, Int -> Distance
Distance Int
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 :: Int -> String -> Doc
indent numSp :: Int
numSp st :: String
st =
  String -> Doc
Pretty.text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
numSp ' ') Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
    ([Doc] -> Doc
Pretty.vcat ([Doc] -> Doc) -> (String -> [Doc]) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
Pretty.text ([String] -> [Doc]) -> (String -> [String]) -> String -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines) String
st

{- |
  Standard indent width.
-}
stdIndent :: Int
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 :: (AnyComorphism, BasicProof) -> GoalDescription
fillGoalDescription (cmo :: AnyComorphism
cmo, basicProof :: BasicProof
basicProof) =
    let gd :: Doc
gd = Int -> String -> Doc
indent Int
stdIndent (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ (AnyComorphism, BasicProof) -> Doc
forall a. Show a => (a, BasicProof) -> Doc
printCmWStat (AnyComorphism
cmo, BasicProof
basicProof)
        stat :: String -> Doc
stat str :: String
str = String -> Doc
Pretty.text "Status:" Doc -> Doc -> Doc
Pretty.<+> String -> Doc
Pretty.text String
str
        printCmWStat :: (a, BasicProof) -> Doc
printCmWStat (c :: a
c, bp :: BasicProof
bp) =
            String -> Doc
Pretty.text "Com:" Doc -> Doc -> Doc
Pretty.<+> String -> Doc
Pretty.text (a -> String
forall a. Show a => a -> String
show a
c)
            Doc -> Doc -> Doc
Pretty.$+$ Int -> String -> Doc
indent Int
stdIndent (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ BasicProof -> Doc
printBP BasicProof
bp)
        printBP :: BasicProof -> Doc
printBP bp :: BasicProof
bp = case BasicProof
bp of
                     BasicProof _ ps :: ProofStatus proof_tree
ps ->
                      String -> Doc
stat (GoalStatus -> String
forall a. Show a => a -> String
show (GoalStatus -> String) -> GoalStatus -> String
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus proof_tree
ps) Doc -> Doc -> Doc
Pretty.$+$
                      (case ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus proof_tree
ps of
                       Proved _ -> String -> Doc
Pretty.text "Used axioms:" Doc -> Doc -> Doc
Pretty.<+>
                           [Doc] -> Doc
Pretty.fsep (Doc -> [Doc] -> [Doc]
Pretty.punctuate Doc
Pretty.comma
                             ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
Pretty.text (String -> Doc) -> (String -> String) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. Show a => a -> String
show) ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
usedAxioms ProofStatus proof_tree
ps)
                           Doc -> Doc -> Doc
Pretty.$+$ String -> Doc
Pretty.text "Used time:" Doc -> Doc -> Doc
Pretty.<+>
                                 String -> Doc
Pretty.text (TimeOfDay -> String
forall a. Show a => a -> String
show (TimeOfDay -> String) -> TimeOfDay -> String
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> TimeOfDay
forall proof_tree. ProofStatus proof_tree -> TimeOfDay
usedTime ProofStatus proof_tree
ps)
                       _ -> Doc
Pretty.empty)
                      Doc -> Doc -> Doc
Pretty.$+$ String -> Doc
Pretty.text "Prover:" Doc -> Doc -> Doc
Pretty.<+>
                            String -> Doc
Pretty.text (ProofStatus proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
usedProver ProofStatus proof_tree
ps)
                     otherProof :: BasicProof
otherProof -> String -> Doc
stat (BasicProof -> String
forall a. Show a => a -> String
show BasicProof
otherProof)
        printTS :: BasicProof -> Doc
printTS bp :: BasicProof
bp = case BasicProof
bp of
                     BasicProof _ ps :: ProofStatus proof_tree
ps ->
                       Int -> String -> Doc
indent (2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
stdIndent) (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ (\ (TacticScript xs :: String
xs) -> String
xs) (TacticScript -> String) -> TacticScript -> String
forall a b. (a -> b) -> a -> b
$
                                                ProofStatus proof_tree -> TacticScript
forall proof_tree. ProofStatus proof_tree -> TacticScript
tacticScript ProofStatus proof_tree
ps
                     _ -> Doc
Pretty.empty
        printPT :: BasicProof -> Doc
printPT bp :: BasicProof
bp = case BasicProof
bp of
                     BasicProof _ ps :: ProofStatus proof_tree
ps ->
                       Int -> String -> Doc
indent (2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
stdIndent) (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ proof_tree -> String
forall a. Show a => a -> String
show (proof_tree -> String) -> proof_tree -> String
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> proof_tree
forall proof_tree. ProofStatus proof_tree -> proof_tree
proofTree ProofStatus proof_tree
ps
                     _ -> Doc
Pretty.empty
    in (String -> GoalDescription
emptyGoalDescription (String -> GoalDescription) -> String -> GoalDescription
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
gd) {
           tacticScriptText :: OpenText
tacticScriptText = OpenText
emptyOpenText {
             additionalText :: String
additionalText = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ BasicProof -> Doc
printTS BasicProof
basicProof },
           proofTreeText :: OpenText
proofTreeText = OpenText
emptyOpenText {
             additionalText :: String
additionalText = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ BasicProof -> Doc
printPT BasicProof
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 :: Editor -> IO Position
getRealEndOfTextIndex ed :: Editor
ed = do
    (Distance eotX :: Int
eotX, _) <- Editor -> EndOfText -> IO Position
forall i. HasIndex Editor i BaseIndex => Editor -> i -> IO Position
getIndexPosition Editor
ed EndOfText
EndOfText
    String
lineBefore <- Editor -> BaseIndex -> IO String
forall i. HasIndex Editor i BaseIndex => Editor -> i -> IO String
getTextLine Editor
ed (BaseIndex -> IO String) -> BaseIndex -> IO String
forall a b. (a -> b) -> a -> b
$ Position -> BaseIndex
IndexPos (Int -> Distance
Distance (Int
eotX Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1), 0)
    Position -> IO Position
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Distance
Distance Int
eotX Distance -> Distance -> Distance
forall a. Num a => a -> a -> a
- 1, Int -> Distance
Distance (Int -> Distance) -> Int -> Distance
forall a b. (a -> b) -> a -> b
$ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
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 :: (Int -> Int -> Int)
-> Int
-> Position
-> OMap (String, Int) GoalDescription
-> OMap (String, Int) GoalDescription
adaptTextPositions f :: Int -> Int -> Int
f diff :: Int
diff pos :: Position
pos =
    (GoalDescription -> GoalDescription)
-> OMap (String, Int) GoalDescription
-> OMap (String, Int) GoalDescription
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map ((GoalDescription -> GoalDescription)
 -> OMap (String, Int) GoalDescription
 -> OMap (String, Int) GoalDescription)
-> (GoalDescription -> GoalDescription)
-> OMap (String, Int) GoalDescription
-> OMap (String, Int) GoalDescription
forall a b. (a -> b) -> a -> b
$ \ gDesc :: GoalDescription
gDesc ->
      let tst :: OpenText
tst = GoalDescription -> OpenText
tacticScriptText GoalDescription
gDesc
          ptt :: OpenText
ptt = GoalDescription -> OpenText
proofTreeText GoalDescription
gDesc
      in GoalDescription
gDesc {
           tacticScriptText :: OpenText
tacticScriptText = if OpenText -> Position
textStartPosition OpenText
tst Position -> Position -> Bool
forall a. Ord a => a -> a -> Bool
> Position
pos
               then OpenText
tst { textStartPosition :: Position
textStartPosition = (Int -> Int -> Int) -> Int -> Position -> Position
changePosition Int -> Int -> Int
f Int
diff (Position -> Position) -> Position -> Position
forall a b. (a -> b) -> a -> b
$
                                OpenText -> Position
textStartPosition OpenText
tst }
               else OpenText
tst,
           proofTreeText :: OpenText
proofTreeText = if OpenText -> Position
textStartPosition OpenText
ptt Position -> Position -> Bool
forall a. Ord a => a -> a -> Bool
> Position
pos
               then OpenText
ptt { textStartPosition :: Position
textStartPosition = (Int -> Int -> Int) -> Int -> Position -> Position
changePosition Int -> Int -> Int
f Int
diff (Position -> Position) -> Position -> Position
forall a b. (a -> b) -> a -> b
$
                                OpenText -> Position
textStartPosition OpenText
ptt }
               else OpenText
ptt }

-- ** main GUI

{- |
  Called whenever the button /Show proof details/ is clicked.
-}
doShowProofDetails :: ProofState -> IO ()
doShowProofDetails :: ProofState -> IO ()
doShowProofDetails prGUISt :: ProofState
prGUISt =
   do
    let thName :: String
thName = ProofState -> String
theoryName ProofState
prGUISt
        winTitleStr :: String
winTitleStr = "Proof Details of Selected Goals from Theory " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thName
    Toplevel
win <- [Config Toplevel] -> IO Toplevel
createToplevel [String -> Config Toplevel
forall w v. HasText w v => v -> Config w
text String
winTitleStr]
    Frame
bFrame <- Toplevel -> [Config Frame] -> IO Frame
forall par. Container par => par -> [Config Frame] -> IO Frame
newFrame Toplevel
win [Relief -> Config Frame
forall w. HasBorder w => Relief -> Config w
relief Relief
Groove, Distance -> Config Frame
forall w. HasBorder w => Distance -> Config w
borderwidth (Double -> Distance
cm 0.05)]
    Label
winTitle <- Frame -> [Config Label] -> IO Label
forall par. Container par => par -> [Config Label] -> IO Label
newLabel Frame
bFrame [String -> Config Label
forall w v. HasText w v => v -> Config w
text String
winTitleStr,
                                  (FontFamily, FontSlant, Int) -> Config Label
forall w f. (HasFont w, FontDesignator f) => f -> Config w
font (FontFamily
Helvetica, FontSlant
Roman, 18 :: Int)]
    Box
btnBox <- Frame -> [Config Box] -> IO Box
forall par. Container par => par -> [Config Box] -> IO Box
newHBox Frame
bFrame []
    Button
tsBut <- Box -> [Config Button] -> IO Button
forall par. Container par => par -> [Config Button] -> IO Button
newButton Box
btnBox [String -> Config Button
forall w v. HasText w v => v -> Config w
text String
expand_tacticScripts, Distance -> Config Button
forall w. HasSize w => Distance -> Config w
width 18]
    Button
ptBut <- Box -> [Config Button] -> IO Button
forall par. Container par => par -> [Config Button] -> IO Button
newButton Box
btnBox [String -> Config Button
forall w v. HasText w v => v -> Config w
text String
expand_proofTrees, Distance -> Config Button
forall w. HasSize w => Distance -> Config w
width 18]
    Button
sBut <- Box -> [Config Button] -> IO Button
forall par. Container par => par -> [Config Button] -> IO Button
newButton Box
btnBox [String -> Config Button
forall w v. HasText w v => v -> Config w
text "Save", Distance -> Config Button
forall w. HasSize w => Distance -> Config w
width 12]
    Button
qBut <- Box -> [Config Button] -> IO Button
forall par. Container par => par -> [Config Button] -> IO Button
newButton Box
btnBox [String -> Config Button
forall w v. HasText w v => v -> Config w
text "Close", Distance -> Config Button
forall w. HasSize w => Distance -> Config w
width 12]
    Label -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Label
winTitle [SideSpec -> PackOption
Side SideSpec
AtTop, Toggle -> PackOption
Expand Toggle
Off, Distance -> PackOption
PadY 10]

    (sb :: ScrollBox Editor
sb, ed :: Editor
ed) <- Frame
-> (Frame -> IO Editor)
-> [Config (ScrollBox Editor)]
-> IO (ScrollBox Editor, Editor)
forall wid par.
(Widget wid, HasScroller wid, Container par) =>
par
-> (Frame -> IO wid)
-> [Config (ScrollBox wid)]
-> IO (ScrollBox wid, wid)
newScrollBox Frame
bFrame
        (Frame -> [Config Editor] -> IO Editor
forall par. Container par => par -> [Config Editor] -> IO Editor
`newEditor` [State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Normal, Position -> Config Editor
forall w. HasSize w => Position -> Config w
size (80, 40)]) []
    Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Disabled
    Frame -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Frame
bFrame [SideSpec -> PackOption
Side SideSpec
AtTop, Toggle -> PackOption
Expand Toggle
On, FillSpec -> PackOption
Fill FillSpec
Both]
    ScrollBox Editor -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack ScrollBox Editor
sb [SideSpec -> PackOption
Side SideSpec
AtTop, Toggle -> PackOption
Expand Toggle
On, FillSpec -> PackOption
Fill FillSpec
Both]
    Editor -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Editor
ed [SideSpec -> PackOption
Side SideSpec
AtTop, Toggle -> PackOption
Expand Toggle
On, FillSpec -> PackOption
Fill FillSpec
Both]

    Box -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Box
btnBox [SideSpec -> PackOption
Side SideSpec
AtTop, Toggle -> PackOption
Expand Toggle
On, FillSpec -> PackOption
Fill FillSpec
X]
    Button -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Button
tsBut [Distance -> PackOption
PadX 5, Distance -> PackOption
PadY 5]
    Button -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Button
ptBut [Distance -> PackOption
PadX 5, Distance -> PackOption
PadY 5]
    Button -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Button
sBut [Distance -> PackOption
PadX 5, Distance -> PackOption
PadY 5]
    Button -> [PackOption] -> IO ()
forall w. Widget w => w -> [PackOption] -> IO ()
pack Button
qBut [Distance -> PackOption
PadX 8, Distance -> PackOption
PadY 5]
    G_theory _ _ _ _ sSens :: ThSens sentence (AnyComorphism, BasicProof)
sSens _ <- G_theory -> IO G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> IO G_theory) -> G_theory -> IO G_theory
forall a b. (a -> b) -> a -> b
$ ProofState -> G_theory
selectedTheory ProofState
prGUISt
    let sttDesc :: String
sttDesc = "Tactic script"
        sptDesc :: String
sptDesc = "Proof tree"
        sens :: ThSens sentence (AnyComorphism, BasicProof)
sens = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter (Bool -> Bool
not (Bool -> Bool)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> Bool)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom) ThSens sentence (AnyComorphism, BasicProof)
sSens
        elementMap :: OMap (String, Int) GoalDescription
elementMap = ((String, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> OMap (String, Int) GoalDescription
 -> OMap (String, Int) GoalDescription)
-> OMap (String, Int) GoalDescription
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> OMap (String, Int) GoalDescription
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> OMap (String, Int) GoalDescription
-> OMap (String, Int) GoalDescription
forall a a.
Ord a =>
(a, SenStatus a (AnyComorphism, BasicProof))
-> OMap (a, Int) GoalDescription -> OMap (a, Int) GoalDescription
insertSenSt OMap (String, Int) GoalDescription
forall k a. Map k a
Map.empty ([(String,
  SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall a. [a] -> [a]
reverse ([(String,
   SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
 -> [(String,
      SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))])
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens sentence (AnyComorphism, BasicProof)
sens)
        insertSenSt :: (a, SenStatus a (AnyComorphism, BasicProof))
-> OMap (a, Int) GoalDescription -> OMap (a, Int) GoalDescription
insertSenSt (gN :: a
gN, st :: SenStatus a (AnyComorphism, BasicProof)
st) resOMap :: OMap (a, Int) GoalDescription
resOMap =
            (OMap (a, Int) GoalDescription
 -> ((AnyComorphism, BasicProof), Int)
 -> OMap (a, Int) GoalDescription)
-> OMap (a, Int) GoalDescription
-> [((AnyComorphism, BasicProof), Int)]
-> OMap (a, Int) GoalDescription
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((((AnyComorphism, BasicProof), Int)
 -> OMap (a, Int) GoalDescription -> OMap (a, Int) GoalDescription)
-> OMap (a, Int) GoalDescription
-> ((AnyComorphism, BasicProof), Int)
-> OMap (a, Int) GoalDescription
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((((AnyComorphism, BasicProof), Int)
  -> OMap (a, Int) GoalDescription -> OMap (a, Int) GoalDescription)
 -> OMap (a, Int) GoalDescription
 -> ((AnyComorphism, BasicProof), Int)
 -> OMap (a, Int) GoalDescription)
-> (((AnyComorphism, BasicProof), Int)
    -> OMap (a, Int) GoalDescription -> OMap (a, Int) GoalDescription)
-> OMap (a, Int) GoalDescription
-> ((AnyComorphism, BasicProof), Int)
-> OMap (a, Int) GoalDescription
forall a b. (a -> b) -> a -> b
$ \ (s2 :: (AnyComorphism, BasicProof)
s2, ind :: Int
ind) -> (a, Int)
-> GoalDescription
-> OMap (a, Int) GoalDescription
-> OMap (a, Int) GoalDescription
forall k a. Ord k => k -> a -> OMap k a -> OMap k a
OMap.insert (a
gN, Int
ind) (GoalDescription
 -> OMap (a, Int) GoalDescription -> OMap (a, Int) GoalDescription)
-> GoalDescription
-> OMap (a, Int) GoalDescription
-> OMap (a, Int) GoalDescription
forall a b. (a -> b) -> a -> b
$
                                                     (AnyComorphism, BasicProof) -> GoalDescription
fillGoalDescription (AnyComorphism, BasicProof)
s2)
              OMap (a, Int) GoalDescription
resOMap ([((AnyComorphism, BasicProof), Int)]
 -> OMap (a, Int) GoalDescription)
-> [((AnyComorphism, BasicProof), Int)]
-> OMap (a, Int) GoalDescription
forall a b. (a -> b) -> a -> b
$
               [(AnyComorphism, BasicProof)]
-> [Int] -> [((AnyComorphism, BasicProof), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((AnyComorphism, BasicProof)
 -> (AnyComorphism, BasicProof) -> Ordering)
-> [(AnyComorphism, BasicProof)] -> [(AnyComorphism, BasicProof)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\ (_, a :: BasicProof
a) (_, b :: BasicProof
b) -> BasicProof -> BasicProof -> Ordering
forall a. Ord a => a -> a -> Ordering
compare BasicProof
a BasicProof
b) ([(AnyComorphism, BasicProof)] -> [(AnyComorphism, BasicProof)])
-> [(AnyComorphism, BasicProof)] -> [(AnyComorphism, BasicProof)]
forall a b. (a -> b) -> a -> b
$ SenStatus a (AnyComorphism, BasicProof)
-> [(AnyComorphism, BasicProof)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenStatus a (AnyComorphism, BasicProof)
st)
                   [(0 :: Int) ..]

    IORef (OMap (String, Int) GoalDescription)
stateRef <- OMap (String, Int) GoalDescription
-> IO (IORef (OMap (String, Int) GoalDescription))
forall a. a -> IO (IORef a)
newIORef OMap (String, Int) GoalDescription
elementMap
    Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Normal
    (((String, Int), GoalDescription) -> IO ())
-> [((String, Int), GoalDescription)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ ((gName :: String
gName, ind :: Int
ind), goalDesc :: GoalDescription
goalDesc) -> do
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
ind Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
          Editor -> String -> IO ()
appendText Editor
ed (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
replicate 75 '-' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
gName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
        Editor -> String -> IO ()
appendText Editor
ed (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ GoalDescription -> String
proverInfo GoalDescription
goalDesc String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
        OpenText
opTextTS <- String
-> OpenText
-> Content
-> Editor
-> (String, Int)
-> IORef (OMap (String, Int) GoalDescription)
-> IO OpenText
addTextTagButton String
sttDesc (GoalDescription -> OpenText
tacticScriptText GoalDescription
goalDesc)
                       Content
TacticScriptText Editor
ed (String
gName, Int
ind) IORef (OMap (String, Int) GoalDescription)
stateRef
        OpenText
opTextPT <- String
-> OpenText
-> Content
-> Editor
-> (String, Int)
-> IORef (OMap (String, Int) GoalDescription)
-> IO OpenText
addTextTagButton String
sptDesc (GoalDescription -> OpenText
proofTreeText GoalDescription
goalDesc)
                       Content
ProofTreeText Editor
ed (String
gName, Int
ind) IORef (OMap (String, Int) GoalDescription)
stateRef
        Editor -> String -> IO ()
appendText Editor
ed "\n"
        let goalDesc' :: GoalDescription
goalDesc' = GoalDescription
goalDesc { tacticScriptText :: OpenText
tacticScriptText = OpenText
opTextTS,
                                  proofTreeText :: OpenText
proofTreeText = OpenText
opTextPT }
        IORef (OMap (String, Int) GoalDescription)
-> (OMap (String, Int) GoalDescription
    -> OMap (String, Int) GoalDescription)
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (OMap (String, Int) GoalDescription)
stateRef ((GoalDescription -> Maybe GoalDescription)
-> (String, Int)
-> OMap (String, Int) GoalDescription
-> OMap (String, Int) GoalDescription
forall k a. Ord k => (a -> Maybe a) -> k -> OMap k a -> OMap k a
OMap.update (\ _ -> GoalDescription -> Maybe GoalDescription
forall a. a -> Maybe a
Just GoalDescription
goalDesc') (String
gName, Int
ind))
      ) ([((String, Int), GoalDescription)] -> IO ())
-> [((String, Int), GoalDescription)] -> IO ()
forall a b. (a -> b) -> a -> b
$ OMap (String, Int) GoalDescription
-> [((String, Int), GoalDescription)]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList OMap (String, Int) GoalDescription
elementMap

    Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Disabled

    (editClicked :: Event ()
editClicked, _) <- Editor -> WishEventType -> IO (Event (), IO ())
forall wid.
GUIObject wid =>
wid -> WishEventType -> IO (Event (), IO ())
bindSimple Editor
ed (Maybe Int -> WishEventType
ButtonPress (Int -> Maybe Int
forall a. a -> Maybe a
Just 1))
    Event ()
quit <- Button -> IO (Event ())
forall w. HasCommand w => w -> IO (Event ())
clicked Button
qBut
    Event ()
save <- Button -> IO (Event ())
forall w. HasCommand w => w -> IO (Event ())
clicked Button
sBut
    Event ()
toggleTacticScript <- Button -> IO (Event ())
forall w. HasCommand w => w -> IO (Event ())
clicked Button
tsBut
    Event ()
toggleProofTree <- Button -> IO (Event ())
forall w. HasCommand w => w -> IO (Event ())
clicked Button
ptBut
    IORef (Bool, Bool)
btnState <- (Bool, Bool) -> IO (IORef (Bool, Bool))
forall a. a -> IO (IORef a)
newIORef (Bool
False, Bool
False)
    IO ()
_ <- Event () -> IO (IO ())
spawnEvent (Event () -> IO (IO ())) -> Event () -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ Event () -> Event ()
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever
        (Event () -> Event ()) -> Event () -> Event ()
forall a b. (a -> b) -> a -> b
$ Event ()
quit Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> Toplevel -> IO ()
forall o. Destroyable o => o -> IO ()
destroy Toplevel
win
        Event () -> Event () -> Event ()
forall a. Event a -> Event a -> Event a
+> Event ()
save Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> do
          Config Button
forall w. HasEnable w => Config w
disable Button
qBut
          Config Button
forall w. HasEnable w => Config w
disable Button
sBut
          String
curDir <- IO String
getCurrentDirectory
          let f :: String
f = String
curDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ '/' Char -> String -> String
forall a. a -> [a] -> [a]
: String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-proof-details.txt"
          Maybe String
mfile <- String
-> [(String, [String])]
-> Maybe (String -> IO ())
-> IO (Maybe String)
fileSaveDialog String
f [ ("Text", ["*.txt"])
                                    , ("All Files", ["*"])] Maybe (String -> IO ())
forall a. Maybe a
Nothing
          IO () -> (String -> IO ()) -> Maybe String -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall (m :: * -> *). Monad m => m ()
done (Editor -> String -> IO ()
writeTextToFile Editor
ed) Maybe String
mfile
          Config Button
forall w. HasEnable w => Config w
enable Button
qBut
          Config Button
forall w. HasEnable w => Config w
enable Button
sBut
          IO ()
forall (m :: * -> *). Monad m => m ()
done
        Event () -> Event () -> Event ()
forall a. Event a -> Event a -> Event a
+> Event ()
toggleTacticScript Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> do
             (expTS :: Bool
expTS, expPT :: Bool
expPT) <- IORef (Bool, Bool) -> IO (Bool, Bool)
forall a. IORef a -> IO a
readIORef IORef (Bool, Bool)
btnState
             Button
tsBut Button -> Config Button -> IO Button
forall a b. a -> (a -> b) -> b
# String -> Config Button
forall w v. HasText w v => v -> Config w
text (if Bool
expTS then String
expand_tacticScripts
                                    else String
hide_tacticScripts)
             Content
-> Bool
-> Editor
-> IORef (OMap (String, Int) GoalDescription)
-> IO ()
toggleMultipleTags Content
TacticScriptText Bool
expTS Editor
ed IORef (OMap (String, Int) GoalDescription)
stateRef
             IORef (Bool, Bool) -> (Bool, Bool) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Bool, Bool)
btnState (Bool -> Bool
not Bool
expTS, Bool
expPT)
        Event () -> Event () -> Event ()
forall a. Event a -> Event a -> Event a
+> Event ()
toggleProofTree Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> do
             (expTS :: Bool
expTS, expPT :: Bool
expPT) <- IORef (Bool, Bool) -> IO (Bool, Bool)
forall a. IORef a -> IO a
readIORef IORef (Bool, Bool)
btnState
             Button
ptBut Button -> Config Button -> IO Button
forall a b. a -> (a -> b) -> b
# String -> Config Button
forall w v. HasText w v => v -> Config w
text (if Bool
expPT then String
expand_proofTrees
                                    else String
hide_proofTrees)
             Content
-> Bool
-> Editor
-> IORef (OMap (String, Int) GoalDescription)
-> IO ()
toggleMultipleTags Content
ProofTreeText Bool
expPT Editor
ed IORef (OMap (String, Int) GoalDescription)
stateRef
             IORef (Bool, Bool) -> (Bool, Bool) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Bool, Bool)
btnState (Bool
expTS, Bool -> Bool
not Bool
expPT)
        Event () -> Event () -> Event ()
forall a. Event a -> Event a -> Event a
+> Event ()
editClicked Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> Editor -> IO ()
forall w. Widget w => w -> IO ()
forceFocus Editor
ed
    () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    expand_tacticScripts :: String
expand_tacticScripts = "Expand tactic scripts"
    expand_proofTrees :: String
expand_proofTrees = "Expand proof trees"
    hide_tacticScripts :: String
hide_tacticScripts = "Hide tactic scripts"
    hide_proofTrees :: String
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
-> Bool
-> Editor
-> IORef (OMap (String, Int) GoalDescription)
-> IO ()
toggleMultipleTags content :: Content
content expanded :: Bool
expanded ed :: Editor
ed stateRef :: IORef (OMap (String, Int) GoalDescription)
stateRef = do
    OMap (String, Int) GoalDescription
s <- IORef (OMap (String, Int) GoalDescription)
-> IO (OMap (String, Int) GoalDescription)
forall a. IORef a -> IO a
readIORef IORef (OMap (String, Int) GoalDescription)
stateRef
    (((String, Int), GoalDescription) -> IO ())
-> [((String, Int), GoalDescription)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (dKey :: (String, Int)
dKey, goalDesc :: GoalDescription
goalDesc) -> do
        let openText :: OpenText
openText = if Content
content Content -> Content -> Bool
forall a. Eq a => a -> a -> Bool
== Content
TacticScriptText
                         then GoalDescription -> OpenText
tacticScriptText GoalDescription
goalDesc
                         else GoalDescription -> OpenText
proofTreeText GoalDescription
goalDesc
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (OpenText -> Bool
textShown OpenText
openText Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
expanded)
             (Content
-> Editor
-> (String, Int)
-> IORef (OMap (String, Int) GoalDescription)
-> IO ()
toggleTextTag Content
content Editor
ed (String, Int)
dKey IORef (OMap (String, Int) GoalDescription)
stateRef)
      ) ([((String, Int), GoalDescription)] -> IO ())
-> [((String, Int), GoalDescription)] -> IO ()
forall a b. (a -> b) -> a -> b
$ OMap (String, Int) GoalDescription
-> [((String, Int), GoalDescription)]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList OMap (String, Int) GoalDescription
s
    IO ()
forall (m :: * -> *). Monad m => m ()
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
-> Editor
-> (String, Int)
-> IORef (OMap (String, Int) GoalDescription)
-> IO ()
toggleTextTag content :: Content
content ed :: Editor
ed (gName :: String
gName, ind :: Int
ind) stateRef :: IORef (OMap (String, Int) GoalDescription)
stateRef = do
    OMap (String, Int) GoalDescription
s <- IORef (OMap (String, Int) GoalDescription)
-> IO (OMap (String, Int) GoalDescription)
forall a. IORef a -> IO a
readIORef IORef (OMap (String, Int) GoalDescription)
stateRef
    let gd :: GoalDescription
gd = GoalDescription -> Maybe GoalDescription -> GoalDescription
forall a. a -> Maybe a -> a
fromMaybe (String -> GoalDescription
emptyGoalDescription String
gName)
             (Maybe GoalDescription -> GoalDescription)
-> Maybe GoalDescription -> GoalDescription
forall a b. (a -> b) -> a -> b
$ (String, Int)
-> OMap (String, Int) GoalDescription -> Maybe GoalDescription
forall (m :: * -> *) k a.
(MonadFail m, Ord k) =>
k -> OMap k a -> m a
OMap.lookup (String
gName, Int
ind) OMap (String, Int) GoalDescription
s
        openText :: OpenText
openText = if Content
content Content -> Content -> Bool
forall a. Eq a => a -> a -> Bool
== Content
TacticScriptText then GoalDescription -> OpenText
tacticScriptText GoalDescription
gd
                                                    else GoalDescription -> OpenText
proofTreeText GoalDescription
gd
        tsp :: Position
tsp = OpenText -> Position
textStartPosition OpenText
openText
        nol :: Int
nol = String -> Int
numberOfLines (OpenText -> String
additionalText OpenText
openText)
    if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ OpenText -> Bool
textShown OpenText
openText then do
        Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Normal
        Editor -> Position -> String -> IO ()
forall i a.
(HasIndex Editor i BaseIndex, GUIValue a) =>
Editor -> i -> a -> IO ()
insertText Editor
ed Position
tsp (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ OpenText -> String
additionalText OpenText
openText
        Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Disabled
        IO ()
forall (m :: * -> *). Monad m => m ()
done
      else do
        Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Normal
        Editor -> Position -> Position -> IO ()
forall i1 i2.
(HasIndex Editor i1 BaseIndex, HasIndex Editor i2 BaseIndex) =>
Editor -> i1 -> i2 -> IO ()
deleteTextRange Editor
ed Position
tsp (Position -> IO ()) -> Position -> IO ()
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int) -> Int -> Position -> Position
changePosition Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Int
nol Position
tsp
        Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# State -> Config Editor
forall w. HasEnable w => State -> Config w
state State
Disabled
        IO ()
forall (m :: * -> *). Monad m => m ()
done
    let openText' :: OpenText
openText' = OpenText
openText { textShown :: Bool
textShown = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ OpenText -> Bool
textShown OpenText
openText }
        s' :: OMap (String, Int) GoalDescription
s' = (GoalDescription -> Maybe GoalDescription)
-> (String, Int)
-> OMap (String, Int) GoalDescription
-> OMap (String, Int) GoalDescription
forall k a. Ord k => (a -> Maybe a) -> k -> OMap k a -> OMap k a
OMap.update
                 (\ _ -> GoalDescription -> Maybe GoalDescription
forall a. a -> Maybe a
Just (GoalDescription -> Maybe GoalDescription)
-> GoalDescription -> Maybe GoalDescription
forall a b. (a -> b) -> a -> b
$ if Content
content Content -> Content -> Bool
forall a. Eq a => a -> a -> Bool
== Content
TacticScriptText
                          then GoalDescription
gd { tacticScriptText :: OpenText
tacticScriptText = OpenText
openText' }
                          else GoalDescription
gd { proofTreeText :: OpenText
proofTreeText = OpenText
openText' } )
                 (String
gName, Int
ind) OMap (String, Int) GoalDescription
s
    IORef (OMap (String, Int) GoalDescription)
-> OMap (String, Int) GoalDescription -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (OMap (String, Int) GoalDescription)
stateRef (OMap (String, Int) GoalDescription -> IO ())
-> OMap (String, Int) GoalDescription -> IO ()
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int)
-> Int
-> Position
-> OMap (String, Int) GoalDescription
-> OMap (String, Int) GoalDescription
adaptTextPositions
         (if OpenText -> Bool
textShown OpenText
openText then (-) else Int -> Int -> Int
forall a. Num a => a -> a -> a
(+))
         Int
nol Position
tsp OMap (String, Int) GoalDescription
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 :: String
-> OpenText
-> Content
-> Editor
-> (String, Int)
-> IORef (OMap (String, Int) GoalDescription)
-> IO OpenText
addTextTagButton cap :: String
cap addText :: OpenText
addText content :: Content
content ed :: Editor
ed dKey :: (String, Int)
dKey stateRef :: IORef (OMap (String, Int) GoalDescription)
stateRef = do
    Editor -> String -> IO ()
appendText Editor
ed (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
stdIndent) ' '
    Position
curPosStart <- Editor -> IO Position
getRealEndOfTextIndex Editor
ed
    Editor -> String -> IO ()
appendText Editor
ed String
cap
    Position
curPosEnd <- Editor -> IO Position
getRealEndOfTextIndex Editor
ed
    Editor -> IO ()
insertNewline Editor
ed
    TextTag
ttag <- Editor -> Position -> Position -> [Config TextTag] -> IO TextTag
forall i1 i2.
(HasIndex Editor i1 BaseIndex, HasIndex Editor i2 BaseIndex) =>
Editor -> i1 -> i2 -> [Config TextTag] -> IO TextTag
createTextTag Editor
ed Position
curPosStart Position
curPosEnd [Toggle -> Config TextTag
underlined Toggle
On]

    (selectTextTag :: Event ()
selectTextTag, _) <- TextTag -> WishEventType -> IO (Event (), IO ())
forall wid.
GUIObject wid =>
wid -> WishEventType -> IO (Event (), IO ())
bindSimple TextTag
ttag (Maybe Int -> WishEventType
ButtonPress (Int -> Maybe Int
forall a. a -> Maybe a
Just 1))
    (enterTT :: Event ()
enterTT, _) <- TextTag -> WishEventType -> IO (Event (), IO ())
forall wid.
GUIObject wid =>
wid -> WishEventType -> IO (Event (), IO ())
bindSimple TextTag
ttag WishEventType
Enter
    (leaveTT :: Event ()
leaveTT, _) <- TextTag -> WishEventType -> IO (Event (), IO ())
forall wid.
GUIObject wid =>
wid -> WishEventType -> IO (Event (), IO ())
bindSimple TextTag
ttag WishEventType
Leave
    IO ()
_ <- Event () -> IO (IO ())
spawnEvent (Event () -> IO (IO ())) -> Event () -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ Event () -> Event ()
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever
                   (Event () -> Event ()) -> Event () -> Event ()
forall a b. (a -> b) -> a -> b
$ Event ()
selectTextTag Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> Content
-> Editor
-> (String, Int)
-> IORef (OMap (String, Int) GoalDescription)
-> IO ()
toggleTextTag Content
content Editor
ed (String, Int)
dKey IORef (OMap (String, Int) GoalDescription)
stateRef
                   Event () -> Event () -> Event ()
forall a. Event a -> Event a -> Event a
+> Event ()
enterTT Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> do
                     Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# Cursor -> Config Editor
forall w ch. (Widget w, CursorDesignator ch) => ch -> Config w
cursor Cursor
hand2
                     IO ()
forall (m :: * -> *). Monad m => m ()
done
                   Event () -> Event () -> Event ()
forall a. Event a -> Event a -> Event a
+> Event ()
leaveTT Event () -> IO () -> Event ()
forall a b. Event a -> IO b -> Event b
>>> do
                     Editor
ed Editor -> Config Editor -> IO Editor
forall a b. a -> (a -> b) -> b
# Cursor -> Config Editor
forall w ch. (Widget w, CursorDesignator ch) => ch -> Config w
cursor Cursor
xterm
                     IO ()
forall (m :: * -> *). Monad m => m ()
done
    OpenText -> IO OpenText
forall (m :: * -> *) a. Monad m => a -> m a
return OpenText :: String -> Bool -> Position -> OpenText
OpenText {additionalText :: String
additionalText = "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OpenText -> String
additionalText OpenText
addText String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n",
                     textShown :: Bool
textShown = Bool
False,
                     textStartPosition :: Position
textStartPosition = Position
curPosEnd}