module PfeBrowserF(mainF) where import Prelude hiding (putStr,putStrLn,print,readFile,writeFile,ioError,catch,readIO) import Monad(unless,mplus,when,filterM) import Maybe(fromMaybe,mapMaybe,isJust) import List(find,(\\),nub) import AllFudgets as Fud hiding (getModificationTime) import ContribFudgets hiding (lift) import FudgetIOMonad1 import PfePlumbing import PfeBrowserMonad import IdInfo import PfeBrowserGUI import CertAttrsEditorF import PfeBrowserMenu as M import PfeBrowserCerts import CertServerF import CertCmd import AuxWindowsF import ImageGraphics(gifFile) import FudExtras(longTextPopupF) import HsModule(ModuleName(..),hsModName,{-,HsModuleI-}) import HsTokens as T import PropPosSyntax(getHSName,SrcLoc(..)) import TiDecorate(no_use) import TI(Typing(..),envFrom,topName,HsIdentI(..)) import PNT(PNT(..)) import TypedIds(namespace,isClassOrType) import UniqueNames as UN(OptSrcLoc(N),optOrigModule) import HasBaseName(getBaseName) import PFE0(getModuleInfixes,setBatchMode,checkProject,ppFlags, withProjectDir,epput, updateModuleGraph,findNode,projectDir,getCurrentModuleGraph) import PFE2(getModuleExports) import PFE3(parseSourceFile'') import ScopeModule(checkRefs) import PFE4(exTypeCheck) import Pfe2Cmds(ppExports) import Pfe4Cmds(ppIface,moduleInterface) import PFE_Certs import CertServers(printAttrs) import PPU(pp,ppi,ppu,withPPEnv,($$),(<>),(<+>),vcat) import DrawDoc(drawDoc) import DrawError import DrawLex(origLabel,certIcon) import FudDraw(ulinkD) import MT(lift) import MUtils import AbstractIO hiding (getEnv) import FileUtils(updateFile) import SimpleGraphs(reverseGraph,neighbours) import StatusIndicator(statusF,Status(..)) -- Debuging --import IOExts(trace) --- Plumbing ------------------------------------------------------------------- mainF opts pdir servers = loopOnlyF $ titleShellF' (setSizing Static) myversion pfeBrowserF where pfeBrowserF = pfeF opts >==< guiF -- @ guiF : the graphical user interface fudget of the PFE browser guiF :: F Out In TagF guiF dispatch tags = mapTF vBoxF $ (mapTF hBoxF (pfeMenuBarTF>&<statusTF) >&< infoWindowsTF) >&< compTagF (hSplitF' aLeft) graphDispTF moduleDispTF >&< (popupsTF >&< certServerTF) toTitle = Left (_toMenuBar:&:toStatus:&:_toInfoWindows):&:(toGraph:&:toModuleDisp) :&:(toPopups:&:toCertServer)= extend Right tags toMessagePopup:&:toNewCertPopup:&:(toCertAttrsEditors:&:toTextEditor) = toPopups pfeMenuBarTF = tagF fromMenuBar (pfeMenuBarF types) where types = [serverName s|s<-servers, lookup "has_sequent" (serverAttrs s)/=Just "no"] statusTF = tagF (const done) (spacer1F centerS $ {-"Status:" `labLeftOfF`-} statusF) popupsTF = messagePopupTF >&< newCertPopupTF >&< (certAttrsEditorsTF >&< textEditorPopupTF) where messagePopupTF = tagF fromMessagePopup (snd>^=<longTextPopupF) newCertPopupTF = tagF fromNewCertPopup newCertPopupF certAttrsEditorsTF = tagF fromCertAttrsEditor dynCertAttrsEditorPopupsF textEditorPopupTF = tagF fromTextEditor textEditorPopupF graphDispTF = tagF fromGraph graphDispF certServerTF = tagF fromCertServer certServerF -- actually not a GUI part... toNodeInfo:&:(_toSource:&:_toRefs) = toModuleDisp moduleDispTF = mapTF vBoxF $ tagF fromNodeInfo nodeInfoF >&< compTagF (vSplitF' aBottom) (tagF fromSource sourceDispF) (tagF fromRefs refDispF) infoWindowsTF = tagF fromInfoWindows $ spacer1F (noStretchS False True `compS` rightS) $ auxGfxWindowsF myname fromGraph = newNode fromNodeInfo = either newModuleLbl newFile fromRefs = infoPick Nothing fromMessagePopup _ = done fromInfoWindows = either popupInfoWindow infoPick' where infoPick' (w,infolbl) = infoPick (Just w) infolbl infoPick optw infolbl = case infolbl of CertLbl cert -> clearRefs >> changeHilite [] >> updCertInfo cert DefLbl (HsCon (PNT pn sp _)) -> goto (HsCon pn,sp) DefLbl (HsVar (PNT pn sp _)) -> goto (HsVar pn,sp) SrcLocLbl (path,pos) -> newFile path >> gotoLabel (posLabel pos) where gotoLabel lbl = do pfePut . toSource . mkvis $ lbl changeHilite [lbl] ModuleLbl m -> newModuleLbl (m,Nothing) CertCmd cmd@(ValidateCert qcert) -> do putCertServer cmd vcert <- certDisplay # getStBr when (vcert==Just qcert) $ showQCertInfo qcert CertCmd cmd -> do maybe done close optw putCertServer cmd where close w = popupInfoWindow (w,False) CreateCert ca -> newCertPopup ca CertEdit e -> pfePut (toCertAttrsEditors (Right e)) CertShowText txt -> pfePut . toMessagePopup . map backspace . lines $ txt ShowErrorMsg gfx -> popupErrorMsg gfx newCertPopup ca = do cicons <- certIcons # getStBr clearRefs pfePut (toNewCertPopup (cicons,ca)) putCertServer cmd = do cmds <- certInProgress # getStBr setInProgress (cmds++[cmd]) if null cmds then doCertServer shellcmd else notnow where shellcmd = shellCmd cmd notnow = certCmdMsg "Command added to queue" shellcmd -- pre: no command in progress doCertServer shellcmd = do certCmdMsg "Sent certificate server command" shellcmd pfePut (toCertServer shellcmd) certCmdMsg msg cmd = do cnt <- length . certInProgress # getStBr pfePut $ toRefs $ linesD $ [g $ msg++":", g cmd] ++(if cnt>0 then [g $ "Number of commands in queue: "++show cnt] else []) fromNewCertPopup (ty,(cert,concl)) = if null cert || null concl then popupMsg "Fill in both a certificate name and a conclusion when creating a new certificate!" else do m <- modname # getStBr let qcert = QCertName m cert cmd = CertCmd.NewCert ty qcert concl putCertServer cmd dcert <- certDisplay # getStBr when (dcert==Just qcert) $ showQCertInfo qcert fromCertAttrsEditor (ctype,(cname,userattrs)) = do Just dir <- projectDir m <- modname # getStBr (_,(Just oldattrs,_)) <- certInfo m cname let newattrs = updateAttrs oldattrs userattrs updateFile (certAttrsPath m cname dir) (printAttrs newattrs) infoPick Nothing (CertLbl cname) -- hmm where updateAttrs oldattrs newattrs = map replace oldattrs++addedattrs -- preserve the order! where addedattrs = filter added newattrs added (n,_) = n `notElem` map fst oldattrs replace (name,old) = (name,fromMaybe old (lookup name newattrs)) fromTextEditor ((_,Just src),src') = if src'/=src then do srcpath <- fst . modnode # getStBr -- This assumes that the editor window is modal, so that -- the current node still is the same!! writeFile srcpath src' reloadModule else done fromMenuBar msg = case msg of File fcmd -> fileCmd fcmd View vcmd -> viewCmd vcmd Windows wcmd -> windowCmd wcmd Cert ccmd -> certCmd ccmd _ -> done -- !! where fileCmd Quit = pfeQuit fileCmd ReloadModule = reloadProject fileCmd EditModule = editModule viewCmd vcmd = do updStBr $ \ st->st{viewMode=vcmd} optGetTypes windowCmd (WindowCmd w up) = pfePut (toInfoWindows (w,Left up)) --up is False or True certCmd certcmd = case certcmd of M.NewCert -> whenInModuleM $ newCertPopup ("","") M.NewAll certtype -> whenInModuleM $ newAll certtype M.TodoCert -> putCertServer CertCmd.TodoCert RevalidateAllQuick -> revalidateAll >> reloadModule ValidateAll -> validateAll _ -> done -- !! newAll ty = do m <- modname # getStBr putCertServer $ CertCmd.NewCertAll ty (pp m) validateAll = do m <- modname # getStBr let qcert = QCertName m validateOne = putCertServer . ValidateCert . qcert . fst mapM_ validateOne. certs =<< getStBr editModule = do n <- modnode # getStBr unless (isNoModule n) $ do let srcpath = fst n mname = fst (snd n) prompt = "Edit "++pp mname++" in "++srcpath src <- readFile srcpath pfePut (toTextEditor (Just prompt,Just src)) fromCertServer (ok,output) = do cmds <- certInProgress # getStBr let cmds' = drop 1 cmds setInProgress cmds' if null cmds' then do clearRefs changeHilite [] {-when ok-} reloadModule else doCertServer (shellCmd (head cmds')) unless (null output) (route cmds . map stripEither $ output) where route (ValidateCert qcert:_) msg = certCmdMsg (ppqcert qcert) (last msg) route _ msg = if ok && length msg <= 3 then pfePut . toRefs . linesD . map g $ msg else pfePut $ toMessagePopup msg --- Initialization and main loop ------------------------------------------- --pfeF o = nullF pfeF :: Opts -> PfeF pfeF = runFIOM . runPfeFM pfeFM pfeFM :: PfeFM () pfeFM = do g <- getCurrentModuleGraph icons <- getCertIcons servers sadicon <- getIcon (gifFile (badCertIconPath pdir)) setStBr St{modnode=noModuleNode,viewMode=view0,mrefs=[], hilbls=[], types=Nothing,certs=[],revgraph=reverseGraph (map snd g), certDisplay=Nothing,certInProgress=[], certServers=servers,certIcons=icons,sadIcon=sadicon} pfePut (toGraph g) putInfoWindow (CertTypes,drawCertTypes (zip servers icons)) pfePut (toCertAttrsEditors (Left servers)) setBatchMode False pfeloop where pfeloop :: PfeFM () pfeloop = do (dispatch =<< pfeGet) `catch` stdHandler pfeloop getCertIcons :: CertServers -> PfeFM CertIcons getCertIcons servers = mapM getCertIcon servers getCertIcon certServer = do let dir = serverDir certServer certtype = serverName certServer iconsrc status = gifFile (dir++"/"++status++".gif") valid <- getIcon (iconsrc "valid") invalid <- getIcon (iconsrc "invalid") unknown <- getIcon (iconsrc "unknown") return (certtype,(valid,invalid,unknown)) getIcon = lift . xrequestFIOM . convToPixmapK drawCertTypes = htableD hdrs . concatMap certD where hdrs = ["Icon","Type","Description"] certD (server,(ty,(icon,_,_))) = [g icon,g ty,g descr] where descr = fromMaybe "(Descrption missing)" $ lookup "description" (serverAttrs server) typeErrorHandler err = do --setNoTypes pfePut $ toRefs $ fgD "red" $ g "Type error!" setStatus (Typing,InError) --o <- ppFlags m <- modname # getStBr popupErrorMsg (fontD ppfont (drawTypeError m err)) epput err
{-
setNoTypes = do updStBr $ \ st->st{viewMode=Hyper}
putStrLn "Switching off type info"
pfePut (toMenuBar (View Hyper))
-}
stdHandler err = do epput msg -- popupMsg msg unless (null msg) $ popupErrorMsg (msgGfx msg) where msg = ioeGetErrorString err popupErrorMsg gfx = do putInfoWindow (ErrorMsg,gfx) popupInfoWindow (ErrorMsg,True) clearErrorMsg = putInfoWindow (ErrorMsg,blankD 10) setStatus = pfePut . toStatus resetStatus = sequence_ [setStatus (l,Unknown)|l<-[minBound..maxBound]] whenInModuleM = unlessM (isNoModule.modnode # getStBr) --- Reactions and auxiliary functions -------------------------------------- reloadProject = -- skip reload if there is no project, or no module is selected whenInModuleM $ reloadGraph >> reloadModule where reloadGraph = do updateModuleGraph -- should also check for added/removed files and update graphDispF updModNode . modname =<< getStBr updModNode m = do g <- getCurrentModuleGraph node <- findNode m updStBr $ \st->st{revgraph=reverseGraph (map snd g),modnode=node} return node reloadModule = whenInModuleM $ do maybe done showQCertInfo . certDisplay =<< getStBr newNode . modnode =<< getStBr
newNode: load and display a new module, after the user has entered or clicked on a module name or a file name.
newNode node@(path,_) =
withWaitCursor $
do resetStatus
clearErrorMsg
setStatus (Syntax,InProgress)
dir <- checkProject
--pfePut (toSource (Left ("","",[]))) -- empty window to scroll to top
r <- try (parseSourceFile'' path)
case r of
Left err -> badNode dir err
Right (ts,((wm,ast),refs)) ->
do node@(_,(m,_)) <- updModNode (getBaseName (hsModName ast)) --updates revgraph
let --refs =simplifyRefsTypes' rs
asserts = assertions ast -- :: [(PNT,AssertionI PNT)]
certs_annot = mapMaybe isCertToken ts -- :: [CertName]
isCert cert = doesFileExist (certAttrsPath m cert dir)
certs_existing <- filterM isCert . fromMaybe [] =<<
maybeM (getDirectoryContents (certModuleDir m dir))
let certs_noannot = certs_existing \\ certs_annot
certs = certs_annot++certs_noannot
certsStatus <- zip certs # quickCertsStatus m certs dir
certsInfo <-
let replace = zipWith replace1 certsStatus
replace1 (_,s) (c,(a,s0)) = (c,(a,s))
in replace # mapM (certInfo m) certs
let conccert (cert,(attrs,_)) =
flip (,) cert # (lookup "conc" =<< attrs)
na = collectByFst .
mapMaybe conccert .
filter ((`elem` certs_noannot).fst) $
certsInfo
updStBr $ \st->st{mrefs=refs,hilbls=[],types=Nothing,certs=certsInfo}
e <- getModuleExports m
-- To keep the displays consistent with the internal state,
-- output operations should come after all operations that can fail!
setStatus (Syntax,Good)
setStatus (Scoping,InProgress)
scope_ok <- showScopeErrors refs
setStatus (Scoping,if scope_ok then Good else InError)
importedby <- flip neighbours m . revgraph # getStBr
pfePut (toNodeInfo (Left (node,importedby)))
cicons <- icons # getStBr
pfePut (toSource (Left (dir,cicons,node,ts,refs,certsStatus,na)))
o <- ppFlags
putInfoWindow (Exports,ppo o (ppExports m e))
putInfoWindow (Interface,ppMsgGfx o clickToActivate)
putInfoWindow (Pretty,ppo o ast)
putInfoWindow (Evidence,evidenceGfx m dir cicons certsInfo asserts)
pfePut (toTitle (myname++": "++pp m))
when scope_ok optGetTypes
where
Rather than aborting newNode (and potentially leaving the history buttons in an incosistent state) on errors, display an empty window and continue...
badNode dir err =
do o <- ppFlags
s <- fromMaybe [] # maybeM (readFile path)
updStBr $ \st->st{modnode=node}
pfePut (toRefs (ppMsgGfx o (ioeGetErrorString err)))
pfePut (toNodeInfo (Left (node,[])))
pfePut (toSource (showsrctext s))
setStatus (Syntax,InError)
putInfoWindow (Exports,blankD 10)
putInfoWindow (Interface,blankD 10)
putInfoWindow (Pretty,blankD 10)
putInfoWindow (Evidence,blankD 10)
pfePut (toTitle (myname++": "++path))
showScopeErrors refs =
do if ok
then clearRefs
else do o <- ppFlags
pfePut (toRefs (gfx o))
return ok
where
ok = null errs
errs = checkRefs refs
errcnt = length errs
gfx o =
labelD (ShowErrorMsg (fontD ppfont (drawScopeErrors errs)))
(ulinkD (g msg))
msg = if errcnt==1
then "One scoping error"
else show errcnt++" scoping errors"
newModule: load and display a new module after the user has entered or clicked on a module name.
newModule :: ModuleName ->PfeFM ()
newModule m = newNode =<< findNode m
newModuleLbl (m',optlbl) =
do n@(_,(m,_)) <- modnode # getStBr
when (isNoModule n || m'/=m) $ newModule m'
maybe done gotoLabel optlbl
where
gotoLabel lbl = do pfePut . toSource . mkvis $ lbl
showInfo lbl
newFile: load and display a new module after the user has entered or clicked on a file name.
newFile :: FilePath ->PfeFM ()
newFile path =
do (oldpath,_) <- modnode # getStBr
when (path/=oldpath) $
do updateModuleGraph
g <- getCurrentModuleGraph
case [node|node@(path',_)<-g,path'==path] of
[node] -> newNode node
_ -> fail ("File not part of this project:"++path)
{-
goto o@(_,r) =
case r of
Left (s,n) ->
do let m' = Module s
m <- modname # getStBr
unless (m'==m) $ newModule m'
gotoLocal o
_ -> gotoLocal o
-}
goto o@(r,_) =
do let optm' = optOrigModule r
m <- modname # getStBr
case optm' of
Just m'| m'/=m -> newModule m'
_ -> done
gotoLocal o
gotoLocal (o,sp) =
do st <- getStBr
case [r|r@((d,_),_,[(o',sp')])<-mrefs st,
isDef d,o'==o,namespace sp'==namespace sp]
of orig:_ -> do let lbl = origLabel orig
pfePut (toSource (mkvis lbl))
rememberLbl lbl
showInfo lbl
_ -> putStrLn $ "Didn't find def of "++show o
rememberLbl lbl =
do m <- modname # getStBr
pfePut (toNodeInfo (Right (m,lbl)))
followLink lbl def = rememberLbl lbl >> goto def
changeHilite new =
do old <- hilbls # getStBr
pfePut (toSource (hilite (old\\new) (new\\old)))
updStBr $ \st->st{hilbls=new}
getIdInfo lbl@(Lbl token) =
do refs <- mrefs # getStBr
infixes <- getModuleInfixes
path <- fst . modnode # getStBr
let p = (path,lblPos lbl)
(occurences,optdef,refinfo) = idInfo refs infixes token
return ((occurences,optdef,concatMap msglines refinfo),p)
fromSource (Just (Button 1),lbl@(Lbl ((ModuleName,(_,mn)),_))) =
newModule (PlainModule mn) -- !!!
fromSource (Just button,lbl@(Lbl token)) =
case button of
Button 1 -> case isCertTokenRef token of
Just cert -> changeHilite [lbl] >> updCertInfo cert
_ -> do info@((_,optdef,_),_) <- getIdInfo lbl
case optdef of
Nothing -> done
Just def ->
if isDefLbl lbl
then showInfo' lbl info
else followLink lbl def
Button 2 -> showInfo lbl
Button 3 -> do ((occurences,_,refinfo),_) <- getIdInfo lbl
let cnt=length occurences
msg=if cnt>0
then ["Highlighted all "++show cnt++
" occurences in this module"]
else []
changeHilite (map posLabel occurences)
pfePut (toRefs (linesD (map g (refinfo++msg))))
_ -> done
fromSource (Nothing,lbl) =
ifM (isLink lbl)
(pfePut (toSource setlinkcursor))
(pfePut (toSource setnormalcursor))
where
isLink (Lbl ((ModuleName,(_,mn)),_)) = return True
isLink lbl =
if isDefLbl lbl
then return False
else do info@((_,optdef,_),_) <- getIdInfo lbl
return (isJust optdef)
updCertInfo cert = showCertInfo cert >> updCertIcons cert
updCertIcons cert = whenM (statusChange cert) reloadModule
-- TODO: efficient icon updates in the source display and evidence window
showInfo lbl = showInfo' lbl =<< getIdInfo lbl
showInfo' lbl ((_,def,refinfo),p) =
do --optGetTypes
tinfo <- maybeD (optGetType p) def
ainfo <- maybeD getAssertionInfo def
pfePut (toRefs (linesD (map g refinfo++ainfo++tinfo)))
changeHilite (if isJust def then [lbl] else [])
where
maybeD = maybe (return [])
optGetType p o = maybe (return []) (getType p o) . types =<< getStBr
getType p (qn,k) types =
do --print (k,qn)
m <- modname # getStBr
let env = modtypes m types
o <- ppFlags
--print (let xs:>:_ = unzipTyped mt in xs)
return [typeInfo o env k p qn]
typeInfo ppopts (mt,env) k p qn =
if isClassOrType k
then kinfo qn (fst env)
else tinfo (snd (no_use env)) mt p qn
where
kinfo qn = optpp . lookup qn . convTEnv (ppi.fst)
optpp = maybe (Fud.g "No type/kind info available") (ppo ppopts)
tinfo env mt (path,lexpos) qn =
optpp (find' mt `mplus` lookup qn env')
where env' = convTEnv (ppi.fst) (env++mt)
qn' = getHSName qn
find' = fmap pp_use . find (pos.name)
name (i:>:_) = getHSName i
pos (PNT pn _ (N (Just (SrcLoc f _ lin col)))) =
pn==qn' && f==path && col==column lexpos && lin==line lexpos
pos i = False
pp_use (_:>:(gen,opti)) =
case opti of
Just inst -> "Generally:"<+>gen<>","$$"Here:"<+>inst
_ -> ppi gen
pntpos (PNT _ _ (N p)) = p
convTEnv f env = [(bn i,f info)|i:>:info<-env]
where
bn = fmap orig -- . getHSName
orig (PNT n _ _) = n
modtypes m pfe4info = (snd (envFrom tm),(concat kenvs,concat tenvs))
where
Just (_,((_,tm):_,_)) = lookup m (pfe4info::TInfo)
(kenvs,tenvs) = unzip [env|(_,(_,(_,(_,env))))<-pfe4info]
optGetTypes =
do st <- getStBr
when (viewMode st==Typed &&
not (isNoModule (modnode st) || haveTypes st))
(retypeCheck (modname st))
where
retypeCheck m =
withWaitMsg (g "Type checking...") $
do setStatus (Typing,InProgress)
opttypes <- exTypeCheck (Just [m])
case opttypes of
Left err -> typeErrorHandler err
Right types ->
do mIface <- moduleInterface m -- calls typeCheck again ==> slow!!
setStatus (Typing,Good)
o <- ppFlags
putInfoWindow (Interface,ppo o (ppIface mIface))
updStBr $ \st->st{types=Just types}
clearRefs = pfePut (toRefs (blankD 10))
popupMsg = pfePut . toMessagePopup . msglines
withWaitMsg msg cmd =
do pfePut (toRefs msg)
tryThen (withWaitCursor cmd) $ clearRefs
setInProgress cmds =
do updStBr $ \ st -> st{certInProgress=cmds}
o <- ppFlags
putInfoWindow (PendingCmds,ppo o (vcat cmds))
ppMsgGfx o = msgGfx . ppu o
msgGfx = linesD . map g . msglines
--msgGfx = vboxlD' 0 . map (atomicD . expandTabs 8)
ppo ppopts = ppo' ppopts
ppo' (_,ppopts) = fontD ppfont . drawDoc . withPPEnv ppopts . ppi
msglines = map (expandTabs 8) . lines
clickToActivate =
-- "(To activate type checker: click with the middle mouse button on an identifier)"
"(To activate type checker: select Type Info from the View menu)"
---
{- instance CatchIO e m => CatchIO e (WithState s m) where stm `catch` h = do s <- getSt r <- lift $ try (withStS s stm) case r of Left err -> h err Right (ans,s') -> setSt_ s' >> return ans ioError = lift . ioError -} --
ppfont = argKey "ppfont" refFont