0 | module Protocol.IDE.FileContext
 1 |
 2 | import Protocol.SExp
 3 |
 4 | import public Libraries.Text.Bounded
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | record FileContext where
10 |   constructor MkFileContext
11 |   file : String
12 |   range : Bounds
13 |
14 | export
15 | SExpable FileContext where
16 |   toSExp fc =
17 |     SExpList [ SExpList
18 |                [ SymbolAtom "filename", toSExp fc.file ]
19 |              , SExpList [ SymbolAtom "start"
20 |                         , IntegerAtom (cast fc.range.startLine)
21 |                         , IntegerAtom (cast fc.range.startCol)
22 |                         ]
23 |              , SExpList [ SymbolAtom "end"
24 |                         , IntegerAtom (cast fc.range.endLine)
25 |                         , IntegerAtom (cast fc.range.endCol)
26 |                         ]
27 |              ]
28 |
29 | export
30 | FromSExpable FileContext where
31 |   fromSExp (SExpList [ SExpList
32 |                [ SymbolAtom "filename", filenameSExp ]
33 |              , SExpList [ SymbolAtom "start"
34 |                         , IntegerAtom startLine
35 |                         , IntegerAtom startCol
36 |                         ]
37 |              , SExpList [ SymbolAtom "end"
38 |                         , IntegerAtom endLine
39 |                         , IntegerAtom endCol
40 |                         ]
41 |              ]) = do file <- fromSExp filenameSExp
42 |                      pure $ MkFileContext {file, range = MkBounds
43 |                        { startLine = cast startLine
44 |                        , startCol  = cast startCol
45 |                        , endLine   = cast endLine
46 |                        , endCol    = cast endCol
47 |                        }}
48 |   fromSExp _ = Nothing
49 |