72 |
72 |
73 (** split up a string into a list of characters (with positions) **) |
73 (** split up a string into a list of characters (with positions) **) |
74 |
74 |
75 type chars = (string * Position.T) list; |
75 type chars = (string * Position.T) list; |
76 |
76 |
77 (* a variant of Position.advance (see Pure/General/position.ML) *) |
|
78 fun advance x pos = |
|
79 let |
|
80 fun incr i = i+1; |
|
81 fun change_prop s f props = case Properties.get_int props s of |
|
82 NONE => props |
|
83 | SOME i => Properties.put (s, Int.toString (f i)) props; |
|
84 in |
|
85 pos |> |
|
86 Position.properties_of |> |
|
87 change_prop "offset" incr |> |
|
88 (case x of |
|
89 "\n" => |
|
90 change_prop "line" incr #> |
|
91 change_prop "column" (K 1) |
|
92 | _ => change_prop "column" incr) |> |
|
93 Position.of_properties |
|
94 end; |
|
95 |
|
96 fun is_char_eof ("", _) = true |
77 fun is_char_eof ("", _) = true |
97 | is_char_eof _ = false; |
78 | is_char_eof _ = false; |
98 |
79 |
99 val char_stopper = Scan.stopper (K ("", Position.none)) is_char_eof; |
80 val char_stopper = Scan.stopper (K ("", Position.none)) is_char_eof; |
100 |
81 |
101 fun symbol (x : string, _ : Position.T) = x; |
82 fun symbol (x : string, _ : Position.T) = x; |
102 |
83 |
103 fun explode_pos s pos = fst (fold_map (fn x => fn pos => |
84 fun explode_pos s pos = fst (fold_map (fn x => fn pos => |
104 ((x, pos), advance x pos)) (raw_explode s) pos); |
85 ((x, pos), Position.advance x pos)) (raw_explode s) pos); |
105 |
86 |
106 |
87 |
107 (** scanners **) |
88 (** scanners **) |
108 |
89 |
109 val any = Scan.one (not o Scan.is_stopper char_stopper); |
90 val any = Scan.one (not o Scan.is_stopper char_stopper); |