equal
deleted
inserted
replaced
125 |
125 |
126 fun token_source pos str = |
126 fun token_source pos str = |
127 str |
127 str |
128 |> Source.of_string_limited 8000 |
128 |> Source.of_string_limited 8000 |
129 |> Symbol.source |
129 |> Symbol.source |
130 |> Token.source {do_recover = NONE} (K header_lexicons) pos; |
130 |> Token.source {do_recover = false} (K header_lexicons) pos; |
131 |
131 |
132 fun read_source pos source = |
132 fun read_source pos source = |
133 let val res = |
133 let val res = |
134 source |
134 source |
135 |> Token.source_proper |
135 |> Token.source_proper |