
  0 | module Protocol.IDE.Decoration
  1 | 
  2 | import Protocol.SExp
  3 | 
  4 | %default total
  5 | 
  6 | public export
  7 | data Decoration : Type where
  8 |   Comment   : Decoration
  9 |   Typ       : Decoration
 10 |   Function  : Decoration
 11 |   Data      : Decoration
 12 |   Keyword   : Decoration
 13 |   Bound     : Decoration
 14 |   Namespace : Decoration
 15 |   Postulate : Decoration
 16 |   Module    : Decoration
 17 | 
 18 | public export
 19 | Eq Decoration where
 20 |   Comment   == Comment   = True
 21 |   Typ       == Typ       = True
 22 |   Function  == Function  = True
 23 |   Data      == Data      = True
 24 |   Keyword   == Keyword   = True
 25 |   Bound     == Bound     = True
 26 |   Namespace == Namespace = True
 27 |   Postulate == Postulate = True
 28 |   Module    == Module    = True
 29 |   _         == _         = False
 30 | 
 31 | public export
 32 | Show Decoration where
 33 |   show Comment   = "comment"
 34 |   show Typ       = "type"
 35 |   show Function  = "function"
 36 |   show Data      = "data"
 37 |   show Keyword   = "keyword"
 38 |   show Bound     = "bound"
 39 |   show Namespace = "namespace"
 40 |   show Postulate = "postulate"
 41 |   show Module    = "module"
 42 | 
 43 | 
 44 | export
 45 | SExpable Decoration where
 46 |   toSExp decor = SExpList [ SymbolAtom "decor"
 47 |                           , SymbolAtom (show decor)
 48 |                           ]
 49 |   where
 50 |     {- This definition looks like it repeats `Show`, but `display` is part
 51 |        of the IDE protocol, whereas the `Show` instance doesn't have to be.
 52 |     -}
 53 |     display : Decoration -> String
 54 |     display Comment   = "comment"
 55 |     display Typ       = "type"
 56 |     display Function  = "function"
 57 |     display Data      = "data"
 58 |     display Keyword   = "keyword"
 59 |     display Bound     = "bound"
 60 |     display Namespace = "namespace"
 61 |     display Postulate = "postulate"
 62 |     display Module    = "module"
 63 | 
 64 | export
 65 | FromSExpable Decoration where
 66 |   fromSExp (SExpList [SymbolAtom "decor", SymbolAtom decor]) =
 67 |     case decor of
 68 |       "comment"   => Just Comment
 69 |       "type"      => Just Typ
 70 |       "function"  => Just Function
 71 |       "data"      => Just Data
 72 |       "keyword"   => Just Keyword
 73 |       "bound"     => Just Bound
 74 |       "namespace" => Just Namespace
 75 |       "postulate" => Just Postulate
 76 |       "module"    => Just Module
 77 |       _ => Nothing
 78 |   fromSExp _ = Nothing
 79 |