equal
deleted
inserted
replaced
30 val float_number: string parser |
30 val float_number: string parser |
31 val string: string parser |
31 val string: string parser |
32 val alt_string: string parser |
32 val alt_string: string parser |
33 val verbatim: string parser |
33 val verbatim: string parser |
34 val cartouche: string parser |
34 val cartouche: string parser |
35 val sync: string parser |
|
36 val eof: string parser |
35 val eof: string parser |
37 val command_name: string -> string parser |
36 val command_name: string -> string parser |
38 val keyword_with: (string -> bool) -> string parser |
37 val keyword_with: (string -> bool) -> string parser |
39 val keyword_markup: bool * Markup.T -> string -> string parser |
38 val keyword_markup: bool * Markup.T -> string -> string parser |
40 val keyword_improper: string -> string parser |
39 val keyword_improper: string -> string parser |
194 val float_number = kind Token.Float; |
193 val float_number = kind Token.Float; |
195 val string = kind Token.String; |
194 val string = kind Token.String; |
196 val alt_string = kind Token.AltString; |
195 val alt_string = kind Token.AltString; |
197 val verbatim = kind Token.Verbatim; |
196 val verbatim = kind Token.Verbatim; |
198 val cartouche = kind Token.Cartouche; |
197 val cartouche = kind Token.Cartouche; |
199 val sync = kind Token.Sync; |
|
200 val eof = kind Token.EOF; |
198 val eof = kind Token.EOF; |
201 |
199 |
202 fun command_name x = |
200 fun command_name x = |
203 group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x) |
201 group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x) |
204 (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x))) |
202 (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x))) |