
  0 | ||| Tokenise a source line for easier processing
  1 | module Idris.IDEMode.TokenLine
  2 | 
  3 | import Parser.Lexer.Source
  4 | import Libraries.Text.Lexer
  5 | 
  6 | %default total
  7 | 
  8 | public export
  9 | RawName : Type
 10 | RawName = String
 11 | 
 12 | public export
 13 | data SourcePart
 14 |   = Whitespace String
 15 |   | Name RawName
 16 |   | HoleName String
 17 |   | LBrace
 18 |   | RBrace
 19 |   | Equal
 20 |   | AsPattern
 21 |   | Other String
 22 | 
 23 | ------------------------------------------------------------------------
 24 | -- Printer
 25 | ------------------------------------------------------------------------
 26 | 
 27 | export
 28 | toString : SourcePart -> String
 29 | toString (Whitespace str) = str
 30 | toString (Name n) = n
 31 | toString (HoleName n) = "?" ++ n
 32 | toString LBrace = "{"
 33 | toString RBrace = "}"
 34 | toString Equal = "="
 35 | toString AsPattern = "@"
 36 | toString (Other str) = str
 37 | 
 38 | ------------------------------------------------------------------------
 39 | -- Parser
 40 | ------------------------------------------------------------------------
 41 | 
 42 | holeIdent : Lexer
 43 | holeIdent = is '?' <+> identNormal
 44 | 
 45 | srcTokens : TokenMap SourcePart
 46 | srcTokens =
 47 |     [(identNormal, Name),
 48 |      (holeIdent, \x => HoleName (assert_total (prim__strTail x))),
 49 |      (space, Whitespace),
 50 |      (is '{', const LBrace),
 51 |      (is '}', const RBrace),
 52 |      (is '=', const Equal),
 53 |      (is '@', const AsPattern),
 54 |      (any, Other)]
 55 | 
 56 | export
 57 | tokens : String -> List SourcePart
 58 | tokens str
 59 |     = case lex srcTokens str of
 60 |            -- Add the EndInput token so that we'll have a line and column
 61 |            -- number to read when storing spans in the file
 62 |            (srctoks, (l, c, rest)) =>
 63 |               map val srctoks ++ (if rest == "" then [] else [Other rest])
 64 |