9 val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source -> |
9 val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source -> |
10 (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a) |
10 (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a) |
11 Source.source) Source.source) Source.source) Source.source |
11 Source.source) Source.source) Source.source) Source.source |
12 val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list |
12 val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list |
13 val present_token: Token.T -> Output.output |
13 val present_token: Token.T -> Output.output |
14 val report_token: Token.T -> unit |
14 val reports_of_token: Token.T -> Position.report list |
15 datatype span_kind = Command of string | Ignored | Malformed |
15 datatype span_kind = Command of string | Ignored | Malformed |
16 type span |
16 type span |
17 val span_kind: span -> span_kind |
17 val span_kind: span -> span_kind |
18 val span_content: span -> Token.T list |
18 val span_content: span -> Token.T list |
19 val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source |
19 val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source |
72 if kind = Token.Command |
72 if kind = Token.Command |
73 then Markup.properties [(Markup.nameN, Token.content_of tok)] |
73 then Markup.properties [(Markup.nameN, Token.content_of tok)] |
74 else I; |
74 else I; |
75 in props (token_kind_markup kind) end; |
75 in props (token_kind_markup kind) end; |
76 |
76 |
77 fun report_symbol (sym, pos) = |
77 fun reports_of_symbol (sym, pos) = |
78 if Symbol.is_malformed sym then Position.report pos Markup.malformed else (); |
78 if Symbol.is_malformed sym then [(pos, Markup.malformed)] else []; |
79 |
79 |
80 in |
80 in |
81 |
81 |
82 fun present_token tok = |
82 fun present_token tok = |
83 Markup.enclose (token_markup tok) (Output.output (Token.unparse tok)); |
83 Markup.enclose (token_markup tok) (Output.output (Token.unparse tok)); |
84 |
84 |
85 fun report_token tok = |
85 fun reports_of_token tok = |
86 (Position.report (Token.position_of tok) (token_markup tok); |
86 (Token.position_of tok, token_markup tok) :: |
87 List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok))); |
87 maps reports_of_symbol (Symbol_Pos.explode (Token.source_position_of tok)); |
88 |
88 |
89 end; |
89 end; |
90 |
90 |
91 |
91 |
92 |
92 |