equal
deleted
inserted
replaced
112 |
112 |
113 (** basic scanners **) |
113 (** basic scanners **) |
114 |
114 |
115 open Basic_Symbol_Pos; |
115 open Basic_Symbol_Pos; |
116 |
116 |
117 fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg); |
117 fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg); |
118 |
118 |
119 val scan_id = |
119 val scan_id = |
120 Scan.one (Symbol.is_letter o Symbol_Pos.symbol) ::: |
120 Scan.one (Symbol.is_letter o Symbol_Pos.symbol) ::: |
121 Scan.many (Symbol.is_letdig o Symbol_Pos.symbol); |
121 Scan.many (Symbol.is_letdig o Symbol_Pos.symbol); |
122 |
122 |