git.iko.soy/Idris-dev
on master help sign in
Support semantic highlighting in IDEslave mode

Now, semantic information from the pretty-printer is sent as a list of spans associating regions of output with metadata.

commit4d2185b4a998f8a984eae88ed9398775f81497c8 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 27 Jan 2014, 16:56 (13 years ago) parent13c6eff
5 files changed+61−13
compare with master
unifiedsplit
idris.cabal+1−1 src/Idris/AbsSyntax.hs+27−1 src/Idris/Delaborate.hs+5−5 src/Idris/IdeSlave.hs+17 src/Idris/REPL.hs+11−6
idris.cabal+1−1
@@ -434,7 +434,7 @@ Library
434434
435435 Build-depends: base >=4 && <5
436436 , Cabal
437− , annotated-wl-pprint
437+ , annotated-wl-pprint >= 0.5.3
438438 , ansi-terminal
439439 , ansi-wl-pprint
440440 , binary
src/Idris/AbsSyntax.hs+27−1
@@ -397,6 +397,31 @@ ihPrintResult h s = do i <- getIState
397397 let good = SexpList [SymbolAtom "ok", toSExp s] in
398398 runIO $ hPutStrLn h $ convSExp "return" good n
399399
400+ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
401+ihPrintTermWithType h tm ty = do ist <- getIState
402+ let output = tm <+> colon <+> ty
403+ case idris_outputmode ist of
404+ RawOutput -> runIO .
405+ hPutStrLn h .
406+ displayDecorated (consoleDecorate ist) .
407+ renderCompact $ output
408+ IdeSlave n -> let (str, spans) = displaySpans (fmap (fancifyAnnots ist) (renderCompact output))
409+ good = [SymbolAtom "ok", toSExp str, toSExp spans]
410+ in runIO . hPutStrLn h $ convSExp "return" good n
411+
412+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
413+fancifyAnnots ist annot@(AnnName n _ _) =
414+ do let ctxt = tt_ctxt ist
415+ case () of
416+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
417+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
418+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
419+ _ | otherwise -> annot
420+fancifyAnnots _ annot = annot
421+
422+type1Doc :: Doc OutputAnnotation
423+type1Doc = (annotate AnnConstType $ text "Type 1")
424+
400425ihPrintError :: Handle -> String -> Idris ()
401426ihPrintError h s = do i <- getIState
402427 case idris_outputmode i of
@@ -429,7 +454,8 @@ iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
429454iputGoal g = do i <- getIState
430455 case idris_outputmode i of
431456 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
432− IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" (displayS g "") n
457+ IdeSlave n -> runIO . putStrLn $
458+ convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
433459
434460isetPrompt :: String -> Idris ()
435461isetPrompt p = do i <- getIState
src/Idris/Delaborate.hs+5−5
@@ -50,8 +50,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
5050 | Just n' <- lookup n env = PRef un n'
5151 | otherwise
5252 = case lookup n (idris_metavars ist) of
53− Just (Just _, mi, _) -> mkMVApp (dens n) []
54− _ -> PRef un (dens n)
53+ Just (Just _, mi, _) -> mkMVApp n []
54+ _ -> PRef un n
5555 de env _ (Bind n (Lam ty) sc)
5656 = PLam n (de env [] ty) (de ((n,n):env) [] sc)
5757 de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)
@@ -96,9 +96,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
9696 deFn env (P _ n _) args | not mvs
9797 = case lookup n (idris_metavars ist) of
9898 Just (Just _, mi, _) ->
99− mkMVApp (dens n) (drop mi (map (de env []) args))
100− _ -> mkPApp (dens n) (map (de env []) args)
101− | otherwise = mkPApp (dens n) (map (de env []) args)
99+ mkMVApp n (drop mi (map (de env []) args))
100+ _ -> mkPApp n (map (de env []) args)
101+ | otherwise = mkPApp n (map (de env []) args)
102102 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))
103103
104104 mkMVApp n []
src/Idris/IdeSlave.hs+17
@@ -69,6 +69,23 @@ instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
6969instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where
7070 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]
7171
72+instance SExpable NameOutput where
73+ toSExp TypeOutput = SymbolAtom "type"
74+ toSExp FunOutput = SymbolAtom "function"
75+ toSExp DataOutput = SymbolAtom "data"
76+
77+instance SExpable OutputAnnotation where
78+ toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),
79+ (SymbolAtom "implicit", BoolAtom False)]
80+ toSExp (AnnName n (Just ty) _) = toSExp [(SymbolAtom "name", StringAtom (show n)),
81+ (SymbolAtom "decor", toSExp ty),
82+ (SymbolAtom "implicit", BoolAtom False)]
83+ toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),
84+ (SymbolAtom "decor", SymbolAtom "bound"),
85+ (SymbolAtom "implicit", BoolAtom imp)]
86+ toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]
87+ toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]
88+
7289escape :: String -> String
7390escape = concatMap escapeChar
7491 where
src/Idris/REPL.hs+11−6
@@ -448,8 +448,11 @@ process h fn (Eval t)
448448 ist <- getIState
449449 logLvl 3 $ "Raw: " ++ show (tm', ty')
450450 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
451− ihPrintResult h (showTm ist (delab ist tm') ++ " : " ++
452− showTm ist (delab ist ty'))
451+ let imp = opt_showimp (idris_options ist)
452+ tmDoc = prettyImp imp (delab ist tm')
453+ tyDoc = prettyImp imp (delab ist ty')
454+ ihPrintTermWithType h tmDoc tyDoc
455+
453456process h fn (ExecVal t)
454457 = do ctxt <- getContext
455458 ist <- getIState
@@ -497,11 +500,13 @@ process h fn (Check t)
497500 = do (tm, ty) <- elabVal toplevel False t
498501 ctxt <- getContext
499502 ist <- getIState
500− let ty' = normaliseC ctxt [] ty
503+ let imp = opt_showimp (idris_options ist)
504+ ty' = normaliseC ctxt [] ty
501505 case tm of
502− TType _ -> ihPrintResult h ("Type : Type 1")
503− _ -> ihPrintResult h (showTm ist (delab ist tm) ++ " : " ++
504− showTm ist (delab ist ty))
506+ TType _ ->
507+ ihPrintTermWithType h (prettyImp imp PType) type1Doc
508+ _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))
509+ (prettyImp imp (delab ist ty))
505510
506511process h fn (DocStr n)
507512 = do i <- getIState