equal
deleted
inserted
replaced
213 (**** PARSING OF TSTP FORMAT ****) |
213 (**** PARSING OF TSTP FORMAT ****) |
214 |
214 |
215 (* Strings enclosed in single quotes (e.g., file names) *) |
215 (* Strings enclosed in single quotes (e.g., file names) *) |
216 val scan_general_id = |
216 val scan_general_id = |
217 $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode |
217 $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode |
218 || Scan.repeat ($$ "$") -- Scan.many1 (fn s => Symbol.is_letdig s orelse s="-") |
218 || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig |
219 >> (fn (ss1, ss2) => implode ss1 ^ implode ss2) |
219 >> (fn (ss1, ss2) => implode ss1 ^ implode ss2) |
220 |
220 |
221 val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode |
221 val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode |
222 |
222 |
223 val skip_term = |
223 val skip_term = |