module Idris.IDEMode.SyntaxHighlight import Prelude.Functor as F import Core.Context import Core.InitPrimitives import Core.Metadata import Core.TT import Idris.REPL import Idris.IDEMode.Commands data Decoration : Type where Typ : Decoration Function : Decoration Data : Decoration Keyword : Decoration Bound : Decoration SExpable Decoration where toSExp Typ = SymbolAtom "type" toSExp Function = SymbolAtom "function" toSExp Data = SymbolAtom "data" toSExp Keyword = SymbolAtom "keyword" toSExp Bound = SymbolAtom "bound" record Highlight where constructor MkHighlight location : FC name : Name isImplicit : Bool key : String decor : Decoration docOverview : String typ : String ns : String SExpable FC where toSExp (MkFC fname (startLine, startCol) (endLine, endCol)) = SExpList [ SExpList [ SymbolAtom "filename", StringAtom fname ] , SExpList [ SymbolAtom "start", IntegerAtom (cast startLine + 1), IntegerAtom (cast startCol + 1) ] , SExpList [ SymbolAtom "end", IntegerAtom (cast endLine + 1), IntegerAtom (cast endCol + 1) ] ] toSExp EmptyFC = SExpList [] SExpable Highlight where toSExp (MkHighlight loc nam impl k dec doc t ns) = SExpList [ toSExp loc , SExpList [ SExpList [ SymbolAtom "name", StringAtom (show nam) ] , SExpList [ SymbolAtom "namespace", StringAtom ns ] , SExpList [ SymbolAtom "decor", toSExp dec ] , SExpList [ SymbolAtom "implicit", toSExp impl ] , SExpList [ SymbolAtom "key", StringAtom k ] , SExpList [ SymbolAtom "doc-overview", StringAtom doc ] , SExpList [ SymbolAtom "type", StringAtom t ] ] ] inFile : String -> (FC, (Name, Nat, ClosedTerm)) -> Bool inFile fname (MkFC file _ _, _) = file == fname ||| Output some data using current dialog index export printOutput : {auto o : Ref ROpts REPLOpts} -> SExp -> Core () printOutput msg = do opts <- get ROpts case idemode opts of REPL _ => pure () IDEMode i _ f => send f (SExpList [SymbolAtom "output", msg, toSExp i]) outputHighlight : {auto opts : Ref ROpts REPLOpts} -> Highlight -> Core () outputHighlight h = printOutput $ SExpList [ SymbolAtom "ok" , SExpList [ SymbolAtom "highlight-source" , toSExp hlt ] ] where hlt : List Highlight hlt = [h] outputNameSyntax : {auto opts : Ref ROpts REPLOpts} -> (FC, (Name, Nat, ClosedTerm)) -> Core () outputNameSyntax (fc, (name, _, term)) = let dec = case term of (Local fc x idx y) => Just Bound -- See definition of NameType in Core.TT for possible values of Ref's nametype field -- data NameType : Type where -- Bound : NameType -- Func : NameType -- DataCon : (tag : Int) -> (arity : Nat) -> NameType -- TyCon : (tag : Int) -> (arity : Nat) -> NameType (Ref fc Bound name) => Just Bound (Ref fc Func name) => Just Function (Ref fc (DataCon tag arity) name) => Just Data (Ref fc (TyCon tag arity) name) => Just Typ (Meta fc x y xs) => Just Bound (Bind fc x b scope) => Just Bound (App fc fn arg) => Just Bound (As fc x as pat) => Just Bound (TDelayed fc x y) => Nothing (TDelay fc x ty arg) => Nothing (TForce fc x y) => Nothing (PrimVal fc c) => Just Typ (Erased fc imp) => Just Bound (TType fc) => Just Typ hilite = F.map (\ d => MkHighlight fc name False "" d "" (show term) "") dec in maybe (pure ()) outputHighlight hilite export outputSyntaxHighlighting : {auto m : Ref MD Metadata} -> {auto opts : Ref ROpts REPLOpts} -> String -> REPLResult -> Core REPLResult outputSyntaxHighlighting fname loadResult = do allNames <- filter (inFile fname) . names <$> get MD -- decls <- filter (inFile fname) . tydecls <$> get MD _ <- traverse outputNameSyntax allNames -- ++ decls) pure loadResult