| changeset 44818 | 9b00f09f7721 |
| parent 41750 | 967cbbc77abd |
| child 45583 | fe319b45315c |
| 44817:ba88bb44c192 | 44818:9b00f09f7721 |
|---|---|
134 |
134 |
135 (** scanners **) |
135 (** scanners **) |
136 |
136 |
137 open Basic_Symbol_Pos; |
137 open Basic_Symbol_Pos; |
138 |
138 |
139 fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg); |
139 fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg); |
140 |
140 |
141 |
141 |
142 (* blanks *) |
142 (* blanks *) |
143 |
143 |
144 val scan_blank = Scan.one (Symbol.is_ascii_blank o Symbol_Pos.symbol); |
144 val scan_blank = Scan.one (Symbol.is_ascii_blank o Symbol_Pos.symbol); |