d0be1e954bd4674fc27f2616c72adb37cf3525a2David Lawrence{- |

dafcb997e390efa4423883dafd100c975c4095d6Mark AndrewsModule :$Header$

499b34cea04a46823d003d4c0520c8b03e8513cbBrian WellingtonDescription : history management functions

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David LawrenceCopyright : uni-bremen and DFKI

ec5347e2c775f027573ce5648b910361aa926c01Automatic UpdaterLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

d0be1e954bd4674fc27f2616c72adb37cf3525a2David LawrenceMaintainer : r.pascanu@jacobs-university.de

d0be1e954bd4674fc27f2616c72adb37cf3525a2David LawrenceStability : provisional

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David LawrencePortability : portable

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews

dafcb997e390efa4423883dafd100c975c4095d6Mark AndrewsInterfaces.History contains different functions that deal

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrewswith history

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews-}

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews

dafcb997e390efa4423883dafd100c975c4095d6Mark Andrewsmodule Interfaces.History

d0be1e954bd4674fc27f2616c72adb37cf3525a2David Lawrence ( undoOneStep

d0be1e954bd4674fc27f2616c72adb37cf3525a2David Lawrence , redoOneStep

ec5347e2c775f027573ce5648b910361aa926c01Automatic Updater , undoOneStepWithUpdate

9c3531d72aeaad6c5f01efe6a1c82023e1379e4dDavid Lawrence , redoOneStepWithUpdate

51f90e94e4dcea187628175b50217bc525570b55James Brister , add2history

51f90e94e4dcea187628175b50217bc525570b55James Brister ) where

51f90e94e4dcea187628175b50217bc525570b55James Brister

51f90e94e4dcea187628175b50217bc525570b55James Bristerimport Interfaces.DataTypes

51f90e94e4dcea187628175b50217bc525570b55James Bristerimport Interfaces.Command

51f90e94e4dcea187628175b50217bc525570b55James Bristerimport Common.LibName

51f90e94e4dcea187628175b50217bc525570b55James Brister

51f90e94e4dcea187628175b50217bc525570b55James Bristerimport Proofs.AbstractState

51f90e94e4dcea187628175b50217bc525570b55James Brister

51f90e94e4dcea187628175b50217bc525570b55James Bristerimport Static.DevGraph

51f90e94e4dcea187628175b50217bc525570b55James Bristerimport Static.History

51f90e94e4dcea187628175b50217bc525570b55James Brister

51f90e94e4dcea187628175b50217bc525570b55James Bristerimport qualified Data.Map as Map

51f90e94e4dcea187628175b50217bc525570b55James Brister

51f90e94e4dcea187628175b50217bc525570b55James Brister-- | Datatype used to differentiate between the two actions (so that code does

51f90e94e4dcea187628175b50217bc525570b55James Brister-- not get duplicated

51f90e94e4dcea187628175b50217bc525570b55James Bristerdata UndoOrRedo =

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David Lawrence DoUndo

51f90e94e4dcea187628175b50217bc525570b55James Brister | DoRedo

51f90e94e4dcea187628175b50217bc525570b55James Brister

51f90e94e4dcea187628175b50217bc525570b55James Bristeradd2history :: Command -> IntState -> [UndoRedoElem] -> IntState

51f90e94e4dcea187628175b50217bc525570b55James Bristeradd2history nm st descr = let

51f90e94e4dcea187628175b50217bc525570b55James Brister hst = i_hist st

51f90e94e4dcea187628175b50217bc525570b55James Brister ul = undoList hst

51f90e94e4dcea187628175b50217bc525570b55James Brister nwEl = CmdHistory

51f90e94e4dcea187628175b50217bc525570b55James Brister { command = nm

51f90e94e4dcea187628175b50217bc525570b55James Brister , cmdHistory = descr }

51f90e94e4dcea187628175b50217bc525570b55James Brister in st { i_hist = hst { undoList = nwEl : ul } }

51f90e94e4dcea187628175b50217bc525570b55James Brister

51f90e94e4dcea187628175b50217bc525570b55James Brister-- | Undo or redo a command that modified the development graph

51f90e94e4dcea187628175b50217bc525570b55James BristerundoRedoDgCmd :: UndoOrRedo -> IntState -> LibName

51f90e94e4dcea187628175b50217bc525570b55James Brister -> ([DGChange] -> DGraph -> IO ()) -> IO IntState

51f90e94e4dcea187628175b50217bc525570b55James BristerundoRedoDgCmd actionType state ln update =

51f90e94e4dcea187628175b50217bc525570b55James Brister case i_state state of

51f90e94e4dcea187628175b50217bc525570b55James Brister -- should I return an error message??

51f90e94e4dcea187628175b50217bc525570b55James Brister Nothing -> return state

51f90e94e4dcea187628175b50217bc525570b55James Brister Just dgS -> do

51f90e94e4dcea187628175b50217bc525570b55James Brister let

51f90e94e4dcea187628175b50217bc525570b55James Brister -- take ln from the history storage ??

-- in contrast to GUI here you operate with only one ln at a time

dg = lookupDGraph ln (i_libEnv dgS)

(dg',changes) = ( case actionType of

DoUndo -> undoHistStep

DoRedo -> redoHistStep) dg

newEnv = Map.insert ln dg' (i_libEnv dgS)

newst = state { i_state = Just $ dgS { i_libEnv = newEnv } }

update changes dg'

return newst

-- | Analyze changes to the selected nodes, return new nodes plus a list

-- of changes that would undo last changes

processList :: [ListChange]-> [Int_NodeInfo]

-> [ListChange] -> ([Int_NodeInfo],[ListChange])

processList ls elems acc

= case ls of

-- if nothing to process return elements and changes

[] -> (elems, acc)

x:l->

-- else check what type of change we are dealing with

case x of

-- if it is a change in axioms

AxiomsChange nwaxms nb ->

-- apply change and store the undo action

let nwls = map (\y ->

case y of

Element ps nb' ->

case nb' == nb of

True ->((Element ps{includedAxioms = nwaxms} nb)

,[AxiomsChange (includedAxioms ps) nb])

False -> (y,[]) ) elems

nwelems = map (\y -> fst y) nwls

changesLs = concatMap (\y-> snd y) nwls

in processList l nwelems (changesLs ++ acc)

-- if it is a change in goals

GoalsChange nwgls nb ->

-- apply change and store the undo action

let nwls = map (\y ->

case y of

Element ps nb' ->

case nb' == nb of

True ->((Element ps{selectedGoals = nwgls} nb)

,[GoalsChange (selectedGoals ps) nb])

False ->(y,[])) elems

nwelems = map (\y -> fst y) nwls

changeLs = concatMap (\y ->snd y) nwls

in processList l nwelems (changeLs ++ acc)

-- if selected nodes change

NodesChange nwelems ->

processList l nwelems ((NodesChange elems):acc)

-- | Process one step of undo or redo

processAny :: UndoOrRedo -> IntState

-> (LibName -> [DGChange] -> DGraph -> IO ()) -> IO IntState

processAny actype state update = do

let hst = case actype of

-- find out the list of actions according to the action

-- (undo/redo)

DoUndo -> undoList $ i_hist state

DoRedo -> redoList $ i_hist state

case hst of

[] -> return state

x:l-> do

(nwst,ch) <- processUndoRedoElems actype (cmdHistory x) state [] update

let

x' = x { cmdHistory = ch }

i_hist_state = i_hist state

nwstate = case actype of

DoUndo -> nwst {

i_hist = IntHistory {

undoList = l,

redoList = x' : redoList i_hist_state

}

}

DoRedo -> nwst {

i_hist = IntHistory {

redoList = l,

undoList = x' : undoList i_hist_state

}

}

return nwstate

-- | Process a list of undo or redo changes

processUndoRedoElems :: UndoOrRedo -> [UndoRedoElem] -> IntState

-> [UndoRedoElem]

-> (LibName -> [DGChange] -> DGraph -> IO ())

-> IO (IntState,[UndoRedoElem])

processUndoRedoElems actype ls state acc update

= case i_state state of

Nothing -> return (state,[])

Just ist ->

case ls of

[] -> return (state,acc)

(UseThmChange sw):l -> do

let nwst = state { i_state = Just $ ist { useTheorems = sw } }

ch = UseThmChange $ useTheorems ist

processUndoRedoElems actype l nwst (ch:acc) update

(Save2FileChange sw):l -> do

let nwst = state { i_state = Just $ ist { save2file = sw } }

ch = Save2FileChange $ save2file ist

processUndoRedoElems actype l nwst (ch:acc) update

(ProverChange nwp):l -> do

let nwst = state { i_state = Just $ ist { prover = nwp } }

ch = ProverChange $ prover ist

processUndoRedoElems actype l nwst (ch:acc) update

(ConsCheckerChange nwc):l -> do

let nwst = state { i_state = Just $ ist { consChecker = nwc} }

ch = ConsCheckerChange $ consChecker ist

processUndoRedoElems actype l nwst (ch:acc) update

(ScriptChange nws):l -> do

let nwst = state { i_state = Just $ ist { script = nws } }

ch = ScriptChange $ script ist

processUndoRedoElems actype l nwst (ch:acc) update

(LoadScriptChange sw):l -> do

let nwst = state { i_state = Just $ ist { loadScript = sw } }

ch = LoadScriptChange $ loadScript ist

processUndoRedoElems actype l nwst (ch:acc) update

(CComorphismChange nwc):l -> do

let nwst = state { i_state = Just $ ist { cComorphism = nwc} }

ch = CComorphismChange $ cComorphism ist

processUndoRedoElems actype l nwst (ch:acc) update

(DgCommandChange nln):l -> do

nwst <- undoRedoDgCmd actype state nln $ update nln

let ch = DgCommandChange nln

processUndoRedoElems actype l nwst (ch:acc) update

(ListChange nls):l -> do

let (nwels,lc) = processList nls (elements ist) []

nwst = state { i_state = Just $ ist { elements = nwels } }

ch = ListChange lc

processUndoRedoElems actype l nwst (ch:acc) update

(IStateChange nist):l -> do

let nwst = state { i_state = nist }

ch = IStateChange $ Just ist

processUndoRedoElems actype l nwst (ch:acc) update

undoOneStep :: IntState -> IO IntState

undoOneStep ist = processAny DoUndo ist (\ _ _ _ -> return ())

redoOneStep :: IntState -> IO IntState

redoOneStep ist = processAny DoRedo ist (\ _ _ _ -> return ())

undoOneStepWithUpdate :: IntState -> (LibName -> [DGChange] -> DGraph -> IO ())

-> IO IntState

undoOneStepWithUpdate = processAny DoUndo

redoOneStepWithUpdate :: IntState -> (LibName -> [DGChange] -> DGraph -> IO ())

-> IO IntState

redoOneStepWithUpdate = processAny DoRedo