0 | module Protocol.IDE.Formatting
 1 |
 2 | import Protocol.SExp
 3 | import Protocol.IDE.Decoration
 4 |
 5 | import Data.List
 6 |
 7 | %default total
 8 |
 9 | public export
10 | data Formatting : Type where
11 |   Bold      : Formatting
12 |   Italic    : Formatting
13 |   Underline : Formatting
14 |
15 | export
16 | Show Formatting where
17 |   show Bold      = "bold"
18 |   show Italic    = "italic"
19 |   show Underline = "underline"
20 |
21 | export
22 | SExpable Formatting where
23 |   toSExp format = SExpList [ SymbolAtom "text-formatting"
24 |                            , SymbolAtom (show format)
25 |                            ]
26 |   where
27 |     {- This definition looks like it repeats `Show`, but `display` is part
28 |        of the IDE protocol, whereas the `Show` instance doesn't have to be.
29 |     -}
30 |     display : Formatting -> String
31 |     display Bold      = "bold"
32 |     display Italic    = "italic"
33 |     display Underline = "underline"
34 |
35 |
36 | export
37 | FromSExpable Formatting where
38 |   fromSExp (SExpList [ SymbolAtom "text-formatting"
39 |                            , SymbolAtom format
40 |                      ]) =
41 |     case format of
42 |        "bold"      => Just Bold
43 |        "italic"    => Just Italic
44 |        "underline" => Just Underline
45 |        _           => Nothing
46 |   fromSExp _ = Nothing
47 |
48 | -- At most one decoration & one formatting
49 | -- (We could use `These` to guarantee non-emptiness but I am not
50 | -- convinced this will stay being just 2 fields e.g. the emacs mode
51 | -- has support for tagging things as errors, adding links, etc.)
52 | public export
53 | record Properties where
54 |   constructor MkProperties
55 |   decor  : Maybe Decoration
56 |   format : Maybe Formatting
57 |
58 | export
59 | mkDecor : Decoration -> Properties
60 | mkDecor dec = MkProperties (Just dec) Nothing
61 |
62 | export
63 | mkFormat : Formatting -> Properties
64 | mkFormat = MkProperties Nothing . Just
65 |
66 | export
67 | SExpable Properties where
68 |   toSExp (MkProperties dec form)  = SExpList $ catMaybes
69 |     [ toSExp <$> form
70 |     , toSExp <$> dec
71 |     ]
72 |
73 | export
74 | FromSExpable Properties where
75 |   fromSExp (SExpList props) =
76 |     case props of
77 |       []  => Just $ MkProperties {decor = Nothing, format = Nothing}
78 |       [prop] => do
79 |         let Nothing = fromSExp prop
80 |           | Just decor => Just $ mkDecor decor
81 |         format <- fromSExp prop
82 |         pure $ mkFormat format
83 |       [prop1, prop2] => -- assume the same order as in toSExp
84 |                         -- not part of the protocol though
85 |         do let format = Just !(fromSExp prop1)
86 |            let decor  = Just !(fromSExp prop2)
87 |            pure $ MkProperties {format, decor}
88 |       _ => Nothing
89 |   fromSExp _ = Nothing
90 |