
  0 | module Protocol.IDE.Highlight
  1 | 
  2 | import Protocol.SExp
  3 | 
  4 | import Protocol.IDE.FileContext
  5 | import Protocol.IDE.Decoration
  6 | 
  7 | %default total
  8 | 
  9 | public export
 10 | record Highlight where
 11 |   constructor MkHighlight
 12 |   location : FileContext
 13 |   name : String
 14 |   isImplicit : Bool
 15 |   key : String
 16 |   decor : Decoration
 17 |   docOverview : String
 18 |   typ : String
 19 |   ns : String
 20 | 
 21 | public export
 22 | record LwHighlight where
 23 |   constructor MkLwHighlight
 24 |   location : FileContext
 25 |   decor : Decoration
 26 | 
 27 | export
 28 | SExpable Highlight where
 29 |   toSExp (MkHighlight fc nam impl k dec doc t ns)
 30 |     = SExpList [ toSExp fc
 31 |                , SExpList [ SExpList [ SymbolAtom "name", StringAtom nam ]
 32 |                           , SExpList [ SymbolAtom "namespace", StringAtom ns ]
 33 |                           , toSExp dec
 34 |                           , SExpList [ SymbolAtom "implicit", toSExp impl ]
 35 |                           , SExpList [ SymbolAtom "key", StringAtom k ]
 36 |                           , SExpList [ SymbolAtom "doc-overview", StringAtom doc ]
 37 |                           , SExpList [ SymbolAtom "type", StringAtom t ]
 38 |                           ]
 39 |                ]
 40 | 
 41 | export
 42 | FromSExpable Highlight where
 43 |   fromSExp (SExpList [ fc
 44 |                , SExpList [ SExpList [ SymbolAtom "name", StringAtom nam ]
 45 |                           , SExpList [ SymbolAtom "namespace", StringAtom ns ]
 46 |                           , dec
 47 |                           , SExpList [ SymbolAtom "implicit", impl ]
 48 |                           , SExpList [ SymbolAtom "key", StringAtom key ]
 49 |                           , SExpList [ SymbolAtom "doc-overview", StringAtom doc ]
 50 |                           , SExpList [ SymbolAtom "type", StringAtom typ ]
 51 |                           ]
 52 |                ]) = do
 53 |                  pure $ MkHighlight
 54 |                    { location = !(fromSExp fc)
 55 |                    , name = nam
 56 |                    , ns
 57 |                    , isImplicit = !(fromSExp impl)
 58 |                    , decor = !(fromSExp dec)
 59 |                    , docOverview = doc
 60 |                    , key, typ}
 61 |   fromSExp _ = Nothing
 62 | 
 63 | export
 64 | SExpable LwHighlight where
 65 |   toSExp lwhl = SExpList
 66 |                  [ toSExp lwhl.location
 67 |                  , SExpList [ toSExp lwhl.decor]
 68 |                  ]
 69 | 
 70 | export
 71 | FromSExpable LwHighlight where
 72 |   fromSExp (SExpList
 73 |             [ location
 74 |             , SExpList [ decor ]
 75 |             ]) = do pure $ MkLwHighlight
 76 |                       { location = !(fromSExp location)
 77 |                       , decor    = !(fromSExp decor)}
 78 |   fromSExp _ = Nothing
 79 | 
 80 | public export
 81 | data SourceHighlight =
 82 |     Full Highlight
 83 |   | Lw LwHighlight
 84 | 
 85 | export
 86 | SExpable SourceHighlight where
 87 |   toSExp (Full hl) = toSExp hl
 88 |   toSExp (Lw   hl) = toSExp hl
 89 | 
 90 | export
 91 | FromSExpable SourceHighlight where
 92 |   fromSExp shl = do
 93 |     let Nothing = fromSExp shl
 94 |       | Just hl => Just (Full hl)
 95 |     hl <- fromSExp shl
 96 |     pure $ Lw hl
 97 |