Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
[ new ] semantic highlighting via the IDE mode (#1868)
  • Loading branch information
gallais committed Aug 27, 2021
1 parent 70ac0f4 commit e2addcf
Show file tree
Hide file tree
Showing 27 changed files with 375 additions and 88 deletions.
2 changes: 1 addition & 1 deletion src/Core/Binary.idr
Expand Up @@ -31,7 +31,7 @@ import public Libraries.Utils.Binary
||| (Increment this when changing anything in the data format)
export
ttcVersion : Int
ttcVersion = 60
ttcVersion = 61

export
checkTTCVersion : String -> Int -> Int -> Core ()
Expand Down
62 changes: 40 additions & 22 deletions src/Core/Metadata.idr
Expand Up @@ -21,11 +21,14 @@ import Libraries.Utils.Binary

public export
data Decoration : Type where
Typ : Decoration
Function : Decoration
Data : Decoration
Keyword : Decoration
Bound : Decoration
Typ : Decoration
Function : Decoration
Data : Decoration
Keyword : Decoration
Bound : Decoration
Namespace : Decoration
Postulate : Decoration
Module : Decoration

export
nameTypeDecoration : NameType -> Decoration
Expand All @@ -44,34 +47,49 @@ SemanticDecorations = List ASemanticDecoration

public export
Eq Decoration where
Typ == Typ = True
Function == Function = True
Data == Data = True
Keyword == Keyword = True
Bound == Bound = True
_ == _ = False

Typ == Typ = True
Function == Function = True
Data == Data = True
Keyword == Keyword = True
Bound == Bound = True
Namespace == Namespace = True
Postulate == Postulate = True
Module == Module = True
_ == _ = False

-- CAREFUL: this instance is used in SExpable Decoration. If you change
-- it then you need to fix the SExpable implementation in order not to
-- break the IDE mode.
public export
Show Decoration where
show Typ = "type"
show Function = "function"
show Data = "data"
show Keyword = "keyword"
show Bound = "bound"
show Typ = "type"
show Function = "function"
show Data = "data"
show Keyword = "keyword"
show Bound = "bound"
show Namespace = "namespace"
show Postulate = "postulate"
show Module = "module"

TTC Decoration where
toBuf b Typ = tag 0
toBuf b Function = tag 1
toBuf b Data = tag 2
toBuf b Keyword = tag 3
toBuf b Bound = tag 4
toBuf b Typ = tag 0
toBuf b Function = tag 1
toBuf b Data = tag 2
toBuf b Keyword = tag 3
toBuf b Bound = tag 4
toBuf b Namespace = tag 5
toBuf b Postulate = tag 6
toBuf b Module = tag 7
fromBuf b
= case !getTag of
0 => pure Typ
1 => pure Function
2 => pure Data
3 => pure Keyword
4 => pure Bound
5 => pure Namespace
6 => pure Postulate
7 => pure Module
_ => corrupt "Decoration"

public export
Expand Down
55 changes: 41 additions & 14 deletions src/Idris/Doc/String.idr
Expand Up @@ -44,6 +44,12 @@ data IdrisDocAnn
| DocStringBody
| Syntax IdrisSyntax

export
-- TODO: how can we deal with bold & so on?
docToDecoration : IdrisDocAnn -> Maybe Decoration
docToDecoration (Syntax syn) = syntaxToDecoration syn
docToDecoration _ = Nothing

export
styleAnn : IdrisDocAnn -> AnsiStyle
styleAnn Header = underline
Expand Down Expand Up @@ -377,18 +383,39 @@ export
getDocsForPTerm : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
PTerm -> Core (List String)
getDocsForPTerm (PRef fc name) = pure $ [!(render styleAnn !(getDocsForName fc name MkConfig))]
getDocsForPTerm (PPrimVal _ constant)
= pure [!(render styleAnn !(getDocsForPrimitive constant))]
getDocsForPTerm (PType _) = pure ["Type : Type\n\tThe type of all types is Type. The type of Type is Type."]
getDocsForPTerm (PString _ _) = pure ["String Literal\n\tDesugars to a fromString call"]
getDocsForPTerm (PList _ _ _) = pure ["List Literal\n\tDesugars to (::) and Nil"]
getDocsForPTerm (PSnocList _ _ _) = pure ["SnocList Literal\n\tDesugars to (:<) and Empty"]
getDocsForPTerm (PPair _ _ _) = pure ["Pair Literal\n\tDesugars to MkPair or Pair"]
getDocsForPTerm (PDPair _ _ _ _ _) = pure ["Dependant Pair Literal\n\tDesugars to MkDPair or DPair"]
getDocsForPTerm (PUnit _) = pure ["Unit Literal\n\tDesugars to MkUnit or Unit"]
getDocsForPTerm pterm = pure ["Docs not implemented for " ++ show pterm ++ " yet"]
PTerm -> Core (Doc IdrisDocAnn)
getDocsForPTerm (PRef fc name) = getDocsForName fc name MkConfig
getDocsForPTerm (PPrimVal _ c) = getDocsForPrimitive c
getDocsForPTerm (PType _) = pure $ vcat
[ "Type : Type"
, indent 2 "The type of all types is Type. The type of Type is Type."
]
getDocsForPTerm (PString _ _) = pure $ vcat
[ "String Literal"
, indent 2 "Desugars to a fromString call"
]
getDocsForPTerm (PList _ _ _) = pure $ vcat
[ "List Literal"
, indent 2 "Desugars to (::) and Nil"
]
getDocsForPTerm (PSnocList _ _ _) = pure $ vcat
[ "SnocList Literal"
, indent 2 "Desugars to (:<) and Empty"
]
getDocsForPTerm (PPair _ _ _) = pure $ vcat
[ "Pair Literal"
, indent 2 "Desugars to MkPair or Pair"
]
getDocsForPTerm (PDPair _ _ _ _ _) = pure $ vcat
[ "Dependant Pair Literal"
, indent 2 "Desugars to MkDPair or DPair"
]
getDocsForPTerm (PUnit _) = pure $ vcat
[ "Unit Literal"
, indent 2 "Desugars to MkUnit or Unit"
]
getDocsForPTerm pterm = pure $
"Docs not implemented for" <++> pretty (show pterm) <++> "yet"

summarise : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Expand All @@ -407,15 +434,15 @@ export
getContents : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Namespace -> Core (List String)
Namespace -> Core (Doc IdrisDocAnn)
getContents ns
= -- Get all the names, filter by any that match the given namespace
-- and are visible, then display with their type
do defs <- get Ctxt
ns <- allNames (gamma defs)
let allNs = filter inNS ns
allNs <- filterM (visible defs) allNs
traverse (\ ns => render styleAnn !(summarise ns)) (sort allNs)
vsep <$> traverse summarise (sort allNs)
where
visible : Defs -> Name -> Core Bool
visible defs n
Expand Down
60 changes: 48 additions & 12 deletions src/Idris/IDEMode/REPL.idr
Expand Up @@ -17,7 +17,6 @@ import Core.TT
import Core.Unify

import Data.List
import Data.List1
import Data.So
import Data.String

Expand All @@ -32,6 +31,7 @@ import Idris.REPL
import Idris.Syntax
import Idris.Version
import Idris.Pretty
import Idris.Doc.String

import Idris.IDEMode.Commands
import Idris.IDEMode.Holes
Expand Down Expand Up @@ -274,12 +274,31 @@ returnFromIDE outf i msg
= do send outf (SExpList [SymbolAtom "return", msg, toSExp i])

printIDEResult : {auto c : Ref Ctxt Defs} -> File -> Integer -> SExp -> Core ()
printIDEResult outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "ok", toSExp msg])
printIDEResult outf i msg
= returnFromIDE outf i
$ SExpList [ SymbolAtom "ok"
, toSExp msg
]

printIDEResultWithHighlight : {auto c : Ref Ctxt Defs} -> File -> Integer -> SExp -> Core ()
printIDEResultWithHighlight outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "ok", toSExp msg
-- TODO return syntax highlighted result
, SExpList []])
export
SExpable a => SExpable (Span a) where
toSExp (MkSpan start width ann)
= SExpList [ IntegerAtom (cast start)
, IntegerAtom (cast width)
, toSExp ann
]

printIDEResultWithHighlight :
{auto c : Ref Ctxt Defs} ->
File -> Integer -> (SExp, List (Span Properties)) ->
Core ()
printIDEResultWithHighlight outf i (msg, spans) = do
-- log "ide-mode.highlight" 10 $ show spans
returnFromIDE outf i
$ SExpList [ SymbolAtom "ok"
, msg
, toSExp spans
]

printIDEError : Ref ROpts REPLOpts => {auto c : Ref Ctxt Defs} -> File -> Integer -> Doc IdrisAnn -> Core ()
printIDEError outf i msg = returnFromIDE outf i (SExpList [SymbolAtom "error", toSExp !(renderWithoutColor msg) ])
Expand Down Expand Up @@ -312,16 +331,26 @@ displayIDEResult outf i (REPL RequestedHelp )
$ StringAtom $ displayHelp
displayIDEResult outf i (REPL $ Evaluated x Nothing)
= printIDEResultWithHighlight outf i
$ StringAtom $ show x
$ mapFst StringAtom
!(renderWithDecorations syntaxToProperties $ prettyTerm x)
displayIDEResult outf i (REPL $ Evaluated x (Just y))
= printIDEResultWithHighlight outf i
$ StringAtom $ show x ++ " : " ++ show y
$ mapFst StringAtom
!(renderWithDecorations syntaxToProperties
$ prettyTerm x <++> ":" <++> prettyTerm y)
displayIDEResult outf i (REPL $ Printed xs)
= printIDEResultWithHighlight outf i
$ StringAtom $ !(renderWithoutColor xs)
$ mapFst StringAtom
$ !(renderWithDecorations annToProperties xs)
displayIDEResult outf i (REPL (PrintedDoc xs))
= printIDEResultWithHighlight outf i
$ mapFst StringAtom
$ !(renderWithDecorations docToProperties xs)
displayIDEResult outf i (REPL $ TermChecked x y)
= printIDEResultWithHighlight outf i
$ StringAtom $ show x ++ " : " ++ show y
$ mapFst StringAtom
!(renderWithDecorations syntaxToProperties
$ prettyTerm x <++> ":" <++> prettyTerm y)
displayIDEResult outf i (REPL $ FileLoaded x)
= printIDEResult outf i $ SExpList []
displayIDEResult outf i (REPL $ ErrorLoadingFile x err)
Expand Down Expand Up @@ -436,8 +465,15 @@ displayIDEResult outf i (NameLocList dat)
, IntegerAtom $ cast $ endLine
, IntegerAtom $ cast $ endCol
]

displayIDEResult outf i _ = pure ()
-- do not use a catchall so that we are warned about missing cases when adding a
-- new construtor to the enumeration.
displayIDEResult _ _ (REPL Done) = pure ()
displayIDEResult _ _ (REPL (Executed _)) = pure ()
displayIDEResult _ _ (REPL (ModuleLoaded _)) = pure ()
displayIDEResult _ _ (REPL (ErrorLoadingModule _ _)) = pure ()
displayIDEResult _ _ (REPL (ColorSet _)) = pure ()
displayIDEResult _ _ (REPL DefDeclared) = pure ()
displayIDEResult _ _ (REPL Exited) = pure ()


handleIDEResult : {auto c : Ref Ctxt Defs} ->
Expand Down
79 changes: 74 additions & 5 deletions src/Idris/IDEMode/SyntaxHighlight.idr
Expand Up @@ -9,6 +9,7 @@ import Core.TT

import Idris.REPL
import Idris.Syntax
import Idris.Pretty
import Idris.Doc.String
import Idris.IDEMode.Commands

Expand All @@ -19,12 +20,80 @@ import Libraries.Data.PosMap

%default total

------------------------------------------------------------------------
-- Text properties supported by the IDE mode
------------------------------------------------------------------------

data Formatting : Type where
Bold : Formatting
Italic : Formatting
Underline : Formatting

-- CAREFUL: this instance is used in SExpable Formatting. If you change
-- it then you need to fix the SExpable implementation in order not to
-- break the IDE mode.
Show Formatting where
show Bold = "bold"
show Italic = "italic"
show Underline = "underline"

-- At most one decoration & one formatting
-- (We could use `These` to guarantee non-emptiness but I am not
-- convinced this will stay being just 2 fields e.g. the emacs mode
-- has support for tagging things as errors, adding links, etc.)
public export
record Properties where
constructor MkProperties
decor : Maybe Decoration
format : Maybe Formatting

export
mkDecor : Decoration -> Properties
mkDecor dec = MkProperties (Just dec) Nothing

export
mkFormat : Formatting -> Properties
mkFormat = MkProperties Nothing . Just

export
syntaxToProperties : IdrisSyntax -> Maybe Properties
syntaxToProperties syn = mkDecor <$> syntaxToDecoration syn

export
annToProperties : IdrisAnn -> Maybe Properties
annToProperties Warning = Nothing
annToProperties Error = Nothing
annToProperties ErrorDesc = Nothing
annToProperties FileCtxt = Nothing
annToProperties Code = Nothing
annToProperties Meta = Nothing
annToProperties (Syntax syn) = syntaxToProperties syn

export
docToProperties : IdrisDocAnn -> Maybe Properties
docToProperties Header = pure $ mkFormat Underline
docToProperties Declarations = Nothing
docToProperties (Decl _) = Nothing
docToProperties DocStringBody = Nothing
docToProperties (Syntax syn) = syntaxToProperties syn

SExpable Decoration where
toSExp Typ = SExpList [ SymbolAtom "decor", SymbolAtom "type"]
toSExp Function = SExpList [ SymbolAtom "decor", SymbolAtom "function"]
toSExp Data = SExpList [ SymbolAtom "decor", SymbolAtom "data"]
toSExp Keyword = SExpList [ SymbolAtom "decor", SymbolAtom "keyword"]
toSExp Bound = SExpList [ SymbolAtom "decor", SymbolAtom "bound"]
toSExp decor = SExpList [ SymbolAtom "decor"
, SymbolAtom (show decor)
]

SExpable Formatting where
toSExp format = SExpList [ SymbolAtom "text-formatting"
, SymbolAtom (show format)
]

export
SExpable Properties where
toSExp (MkProperties dec form) = SExpList $ catMaybes
[ toSExp <$> form
, toSExp <$> dec
]


record Highlight where
constructor MkHighlight
Expand Down

0 comments on commit e2addcf

Please sign in to comment.