implementation module htmlDatabase import StdClass, StdInt, StdString import htmlExceptions, htmlFormlib // editor for persistent information: universalDB :: !(!Init,!Lifespan,!a,!String) !(String a -> Judgement) !*HSt -> (a,!*HSt) | iData a universalDB (init,lifespan,value,filename) invariant hst # (dbf,hst) = myDatabase Init (0,value) hst // create / read out database file # (dbversion,dbvalue) = dbf.value // version number and value stored in database # (versionf,hst) = myVersion Init dbversion hst // create / read out version number expected by this application # version = versionf.value // current version number assumed in this application | init == Init // we only want to read, no version conflict # (_,hst) = myVersion Set dbversion hst // synchronize version number and = (dbvalue,hst) // return current value stored in database | dbversion <> version // we want to write and have a version conflict # (_,hst) = myVersion Set dbversion hst // synchronize with new version # (_,hst) = ExceptionStore ((+) (Just (filename,"Your screen data is out of date; I have retrieved the latest data."))) hst // Raise exception = (dbvalue,hst) // return current version stored in database # exception = invariant filename value // no version conflict, check invariants // check invariants | isJust exception // we want to write, but invariants don't hold # (_,hst) = ExceptionStore ((+) exception) hst // report them = (value,hst) // return disapproved value such that it can be improved # (versionf,hst) = myVersion Set (dbversion + 1) hst // increment version number # (_,hst) = myDatabase Set (versionf.value,value) hst // update database file = (value,hst) where myDatabase init cntvalue hst // read the database = mkEditForm (init,if (lifespan == TxtFile) pFormId dbFormId filename cntvalue <@ NoForm) hst myVersion init cnt hst = mkEditForm (init,xtFormId ("vrs_db_" +++ filename) cnt) hst // to remember version number