@@ -342,34 +342,62 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
342 do ist <- getIState
342 do ist <- getIState
343 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
343 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
344 let ppo = ppOptionIst ist
344 let ppo = ppOptionIst ist
345− let mvarTys = map (delabTy ist) mvs
345+ -- splitMvs is a list of pairs of names and their split types
346− let res = (IdeSlave.SymbolAtom "ok",
346+ let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)
347− zipWith (\ n (prems, concl) -> (n, prems, concl))
347+ -- mvOutput is the pretty-printed version ready for conversion to SExpr
348− (map (IdeSlave.StringAtom . show) mvs)
348+ let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
349− (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
349+ mapPair show
351+ let bnd = [ n | (n,_,_) <- hs ] in
352+ let bnds = inits bnd in
353+ (map (\(bnd, h) -> processPremise ist bnd h)
355+ render ist bnd c pc))
350− runIO . putStrLn $ IdeSlave.convSExp "return" res id
358+ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id
351− where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
359+ where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
352− getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
360+ mapSnd f xs = zip (map fst xs) (map (f . snd) xs)
353− in ((n, t):prems, conc)
361+
354− getGoal tm = ([], tm)
362+ -- | Split a function type into a pair of premises, conclusion.
355− sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
363+ -- Each maintains both the original and delaborated versions.
356− -> ([(String, String, SpanList OutputAnnotation)],
364+ splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
357− (String, SpanList OutputAnnotation))
365+ splitPi ist (Bind n (Pi t) rest) =
358− sexpGoal ist cols ppo ns ([], concl) =
366+ let (hs, c, pc) = splitPi ist rest in
359− let infixes = idris_infixes ist
367+ ((n, t, delabTy' ist [] t False False):hs,
360− concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
368+ c, delabTy' ist [] c False False)
361− pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
369+ splitPi ist tm = ([], tm, delabTy' ist [] tm False False)
363− sexpGoal ist cols ppo ns ((n, t):ps, concl) =
371+ -- | Get the types of a list of metavariable names
364− let n' = case n of
372+ mvTys :: IState -> [Name] -> [(Name, Type)]
365− NS (UN nm) ns -> str nm
373+ mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))
366− UN nm | ('_':'_':_) <- str nm -> "_"
374+
367− | otherwise -> str nm
375+ -- | Show a type and its corresponding PTerm in a format suitable
368− _ -> "_"
376+ -- for the IDE - that is, pretty-printed and annotated.
377+ render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)
378+ render ist bnd t pt =
379+ let prettyT = pprintPTerm (ppOptionIst ist)
380+ (zip bnd (repeat False))
386+ renderPretty 0.9 cols .
369− (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
387+ fmap (fancifyAnnots ist) .
370− pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
388+ annotate (AnnTerm t) $ prettyT
371− rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
389+
372− in ((n', t', spans) : fst rest, snd rest)
390+ -- | Juggle the bits of a premise to prepare for output.
391+ processPremise :: IState
392+ -> [Name] -- ^ the names to highlight as bound
393+ -> (Name, Type, PTerm)
396+ SpanList OutputAnnotation)
397+ processPremise ist bnd (n, t, pt) =
398+ let (out, spans) = render ist bnd t pt in
399+ (show n , out, spans)
373runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
401runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
374 case splitName n of
402 case splitName n of
375 Left err -> iPrintError err
403 Left err -> iPrintError err