equal
deleted
inserted
replaced
293 | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs; |
293 | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs; |
294 |
294 |
295 fun idxname cs ds = (implode (rev cs), nat 0 ds); |
295 fun idxname cs ds = (implode (rev cs), nat 0 ds); |
296 fun chop_idx [] ds = idxname [] ds |
296 fun chop_idx [] ds = idxname [] ds |
297 | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds |
297 | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds |
298 | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds |
298 | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds (*legacy*) |
|
299 | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds (*legacy*) |
299 | chop_idx (c :: cs) ds = |
300 | chop_idx (c :: cs) ds = |
300 if Symbol.is_digit c then chop_idx cs (c :: ds) |
301 if Symbol.is_digit c then chop_idx cs (c :: ds) |
301 else idxname (c :: cs) ds; |
302 else idxname (c :: cs) ds; |
302 |
303 |
303 val scan = |
304 val scan = |