||| Tokenise a source line for easier processingmodule Idris.IDEMode.TokenLine import Parser.Lexerimport Text.Lexer public exportdata SourcePart  = Whitespace String  | Name String  | HoleName String  | LBrace  | RBrace  | Equal  | Other String holeIdent : LexerholeIdent = is '?' <+> identStrict srcTokens : TokenMap SourcePartsrcTokens =    [(identStrict, Name),     (holeIdent, \x => HoleName (assert_total (strTail x))),     (space, Whitespace),     (is '{', const LBrace),     (is '}', const RBrace),     (is '=', const Equal),     (any, Other)] exporttokens : String -> List SourceParttokens str    = case lex srcTokens str of           -- Add the EndInput token so that we'll have a line and column           -- number to read when storing spans in the file           (srctoks, (l, c, rest)) =>              map tok srctoks ++ (if rest == "" then [] else [Other rest])