| Copyright | (c) Uni Bremen 2002-2008 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | r.pascanu@gmail.com |
| Stability | provisional |
| Portability | non-portable (imports Logic) |
| Safe Haskell | None |
Interfaces.DataTypes
Description
Different data structures that are (or should be) shared by all interfaces of Hets
- data IntState = IntState {}
- getMaybeLib :: IntState -> Maybe (LibName, LibEnv)
- data IntHistory = IntHistory {
- undoList :: [CmdHistory]
- redoList :: [CmdHistory]
- data CmdHistory = CmdHistory {
- command :: Command
- cmdHistory :: [UndoRedoElem]
- data IntIState = IntIState {}
- data Int_NodeInfo = Element ProofState Int
- data UndoRedoElem
- = UseThmChange Bool
- | Save2FileChange Bool
- | ProverChange (Maybe G_prover)
- | ConsCheckerChange (Maybe G_cons_checker)
- | ScriptChange ATPTacticScript
- | LoadScriptChange Bool
- | CComorphismChange (Maybe AnyComorphism)
- | ListChange [ListChange]
- | IStateChange (Maybe IntIState)
- | DgCommandChange LibName
- | ChShowOutput Bool
- data ListChange
- = AxiomsChange [String] Int
- | GoalsChange [String] Int
- | NodesChange [Int_NodeInfo]
Documentation
data IntState
Internal state of the interface, it contains the development graph and a full history. While this in most cases describes the state of development graph at a given time for GUI it is not the same for the PGIP ( it does not describe selected nodes). If one switches from one interface to the other passing this informations should be sufficient with minimal loss of information ( like selected nodes, unfinished script .. and so on)
Constructors
| IntState | |
getMaybeLib :: IntState -> Maybe (LibName, LibEnv)
data IntHistory
Contains the detailed global history as two list, a list of actions for undo, and a list of action for redo commands
Constructors
| IntHistory | |
Fields
| |
Instances
data CmdHistory
Contains command description needed for undo/redo actions and for displaying commands in the history
Constructors
| CmdHistory | |
Fields
| |
Instances
data IntIState
full description of the internal state required by all interfaces
Constructors
| IntIState | |
Fields
| |
data UndoRedoElem
History elements for the proof state, only LibName would be used by GUI because it keeps track only to changes to the development graph, the other are for PGIP but in order to integrate both they should use same structure
Constructors
Instances
data ListChange
Constructors
| AxiomsChange [String] Int | |
| GoalsChange [String] Int | |
| NodesChange [Int_NodeInfo] |
Instances