0 | module Idris.IDEMode.SyntaxHighlight
 1 |
 2 | import Core.Directory
 3 | import Core.Metadata
 4 |
 5 | import Idris.REPL
 6 | import Idris.Syntax
 7 | import Idris.IDEMode.Commands
 8 |
 9 | import Libraries.Data.PosMap
10 |
11 | %default total
12 |
13 | ||| Output some data using current dialog index
14 | export
15 | printOutput : {auto c : Ref Ctxt Defs} ->
16 |               {auto o : Ref ROpts REPLOpts} ->
17 |               SourceHighlight -> Core ()
18 | printOutput highlight
19 |   =  do opts <- get ROpts
20 |         case idemode opts of
21 |           REPL _ => pure ()
22 |           IDEMode i _ f =>
23 |             send f (Intermediate (HighlightSource [highlight]) i)
24 |
25 | outputHighlight : {auto c : Ref Ctxt Defs} ->
26 |                   {auto opts : Ref ROpts REPLOpts} ->
27 |                   Highlight -> Core ()
28 | outputHighlight hl =
29 |   printOutput $ Full hl
30 |
31 | lwOutputHighlight :
32 |   {auto c : Ref Ctxt Defs} ->
33 |   {auto opts : Ref ROpts REPLOpts} ->
34 |   (FileName, NonEmptyFC, Decoration) -> Core ()
35 | lwOutputHighlight (fname, nfc, decor) =
36 |   printOutput $ Lw $ MkLwHighlight {location = cast (fname, nfc), decor}
37 |
38 | outputNameSyntax : {auto c : Ref Ctxt Defs} ->
39 |                    {auto s : Ref Syn SyntaxInfo} ->
40 |                    {auto opts : Ref ROpts REPLOpts} ->
41 |                    (FileName, NonEmptyFC, Decoration, Name) -> Core ()
42 | outputNameSyntax (fname, nfc, decor, nm) = do
43 |       defs <- get Ctxt
44 |       log "ide-mode.highlight" 20 $ "highlighting at " ++ show nfc
45 |                                  ++ ": " ++ show nm
46 |                                  ++ "\nAs: " ++ show decor
47 |       let fc = justFC nfc
48 |       let (mns, name) = displayName nm
49 |       outputHighlight $ MkHighlight
50 |          { location = cast (fname, nfc)
51 |          , name
52 |          , isImplicit = False
53 |          , key = ""
54 |          , decor
55 |          , docOverview = "" --!(getDocsForName fc nm)
56 |          , typ = "" -- TODO: extract type maybe "" show !(lookupTyExact nm (gamma defs))
57 |          , ns = maybe "" show mns
58 |          }
59 |
60 | export
61 | outputSyntaxHighlighting : {auto c : Ref Ctxt Defs} ->
62 |                            {auto m : Ref MD Metadata} ->
63 |                            {auto s : Ref Syn SyntaxInfo} ->
64 |                            {auto opts : Ref ROpts REPLOpts} ->
65 |                            String ->
66 |                            REPLResult ->
67 |                            Core REPLResult
68 | outputSyntaxHighlighting fname loadResult = do
69 |   opts <- get ROpts
70 |   when (opts.synHighlightOn) $ do
71 |     meta <- get MD
72 |     modIdent <- ctxtPathToNS fname
73 |
74 |     let allNames = filter ((PhysicalIdrSrc modIdent ==) . fst . fst)
75 |                      $ toList meta.nameLocMap
76 |     --decls <- filter (inFile fname) . tydecls <$> get MD
77 |     --_ <- traverse outputNameSyntax allNames -- ++ decls)
78 |
79 |     decors <- allSemanticHighlighting meta
80 |
81 |     traverse_ {b = Unit}
82 |          (\(nfc, decor, mn) =>
83 |            case mn of
84 |              Nothing => lwOutputHighlight (fname, nfc, decor)
85 |              Just n  => outputNameSyntax  (fname, nfc, decor, n))
86 |          (toList decors)
87 |
88 |   pure loadResult
89 |