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