bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederDescription : GUI for showing and saving proof details.

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Rainer Grabbe 2006

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : rainer25@informatik.uni-bremen.de

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : needs POSIX

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederAdditional window used by 'GUI.ProofManagement' for displaying proof details.

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermodule GUI.HTkProofDetails (doShowProofDetails) where

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport qualified Common.Doc as Pretty

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport qualified Common.OrderedMap as OMap

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederimport qualified Data.Map as Map

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Data.Maybe

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Data.List

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Data.IORef

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport GUI.Utils (fileSaveDialog)

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport System.Directory

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport GUI.HTkUtils

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Proofs.AbstractState

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederimport Logic.Comorphism

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederimport Logic.Logic

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport Logic.Prover

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maederimport Static.GTheory

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski-- * record structures and basic functions for handling

ebcaad207cafc89eeb49d431f40de2ef4c48411cChristian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder{- |

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Record structure containing proof details for a single proof.

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-}

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskidata GoalDescription = GoalDescription {

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder proverInfo :: String, -- ^ standard proof details

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder tacticScriptText :: OpenText, -- ^ more details for tactic script

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder proofTreeText :: OpenText -- ^ more details for proof tree

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder }

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder{- |

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Current state of a text tag providing additional information. The text can be

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder folded or unfolded.

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-}

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata OpenText = OpenText {

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder additionalText :: String, -- ^ additional information

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder textShown :: Bool, -- ^ if true, text is unfolded (default: false)

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder textStartPosition :: Position -- ^ start position in editor widget

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski }

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder{- |

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Creates an initial 'GoalDescription' filled with just the standard prover

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski info.

dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder-}

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederemptyGoalDescription :: String -- ^ information about the used prover

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder -> GoalDescription -- ^ initiated GoalDescription

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederemptyGoalDescription st =

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder GoalDescription {

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder proverInfo = st,

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder tacticScriptText = emptyOpenText,

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder proofTreeText = emptyOpenText }

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder{- |

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Creates an empty 'OpenText' with start position (0,0).

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-}

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaederemptyOpenText :: OpenText

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederemptyOpenText = OpenText {

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder additionalText = "",

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski textShown = False,

3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maeder textStartPosition = (Distance 0, Distance 0) }

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski-- | Determines the kind of content of a 'HTk.TextTag'.

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata Content = TacticScriptText | ProofTreeText deriving Eq

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- * GUI for show proof details

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder-- ** help functions

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder{- | Return number of new lines in a string.

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder-}

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedernumberOfLines :: String

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder -> Int

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian MaedernumberOfLines =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder foldr (\ ch -> if ch == '\n' then (+ 1) else id) 0

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- |

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder Change the x-value of a 'Position' by a given arithmetical function and value.

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-}

836e72a3c413366ba9801726f3b249c7791cb9caChristian MaederchangePosition :: (Int -> Int -> Int) -- ^ mostly add or subtract values

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder -> Int -- ^ (difference) value

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> Position -- ^ old position

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> Position -- ^ changed position with new x-value

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian MaederchangePosition f diff (Distance posX, Distance posY) =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (Distance $ f posX diff, Distance posY)

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- |

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Indentation of a 'String' (also multiple lines) by a number of spaces.

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-}

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederindent :: Int -- ^ number of spaces

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> String -- ^ input String

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -> Pretty.Doc -- ^ output document

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederindent numSp st =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Pretty.text (replicate numSp ' ') Pretty.<>

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (Pretty.vcat . map Pretty.text . lines) st

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- |

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Standard indent width.

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder-}

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederstdIndent :: Int

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederstdIndent = 4

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- |

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder An item of thmStatus will be put into 'GoalDescription' structure.

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Pretty printing of proof details, adding additional information

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder for text tags.

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-}

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederfillGoalDescription :: (AnyComorphism, BasicProof)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> GoalDescription -- ^ contents in pretty format

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaederfillGoalDescription (cmo, basicProof) =

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder let gd = indent stdIndent $ show $ printCmWStat (cmo, basicProof)

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder stat str = Pretty.text "Status:" Pretty.<+> Pretty.text str

1738d16957389457347bee85075d3d33d002158fChristian Maeder printCmWStat (c, bp) =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Pretty.text "Com:" Pretty.<+> Pretty.text (show c)

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder Pretty.$+$ indent stdIndent (show $ printBP bp)

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder printBP bp = case bp of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder BasicProof _ ps ->

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder stat (show $ goalStatus ps) Pretty.$+$

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (case goalStatus ps of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Proved _ -> Pretty.text "Used axioms:" Pretty.<+>

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder Pretty.fsep (Pretty.punctuate Pretty.comma

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski $ map (Pretty.text . show) $ usedAxioms ps)

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder Pretty.$+$ Pretty.text "Used time:" Pretty.<+>

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Pretty.text (show $ usedTime ps)

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder _ -> Pretty.empty)

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder Pretty.$+$ Pretty.text "Prover:" Pretty.<+>

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Pretty.text (usedProver ps)

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder otherProof -> stat (show otherProof)

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder printTS bp = case bp of

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder BasicProof _ ps ->

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder indent (2 * stdIndent) $ (\(TacticScript xs) -> xs) $

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder tacticScript ps

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder _ -> Pretty.empty

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder printPT bp = case bp of

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder BasicProof _ ps ->

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder indent (2 * stdIndent) $ show $ proofTree ps

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder _ -> Pretty.empty

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder in (emptyGoalDescription $ show gd) {

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder tacticScriptText = emptyOpenText {

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder additionalText = show $ printTS basicProof },

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder proofTreeText = emptyOpenText {

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder additionalText = show $ printPT basicProof } }

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder{- |

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Gets real 'EndOfText' index at the char position after (in x-direction)

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder the last written text. This is because 'EndOfText' only gives a value where a

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder text would be after an imaginary newline.

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-}

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetRealEndOfTextIndex :: Editor -- ^ the editor whose end index is determined

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder -> IO Position -- ^ position behind last char in widget

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetRealEndOfTextIndex ed = do

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (Distance eotX, _) <- getIndexPosition ed EndOfText

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder lineBefore <- getTextLine ed $ IndexPos (Distance (eotX - 1), 0)

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder return (Distance eotX - 1, Distance $ length lineBefore)

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder{- |

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder For a given Ordered Map containing all proof values, this function adapts the

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder 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 ::

(Logic lid

sublogics1

basic_spec1

sentence

symb_items1

symb_map_items1

sign1

morphism1

symbol1

raw_symbol1

proof_tree1) =>

ProofState lid sentence

-> 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

(flip 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]

let sttDesc = "Tactic script"

sptDesc = "Proof tree"

sens = selectedGoalMap prGUISt

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}