equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 fun ml_positions start_line name txt = |
7 fun ml_positions start_line name txt = |
8 let |
8 let |
9 fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res = |
9 fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res = |
10 let val s = "(Position.line_file " ^ Int.toString line ^ " \"" ^ name ^ "\")" |
10 let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")" |
11 in positions line cs (s :: res) end |
11 in positions line cs (s :: res) end |
12 | positions line (c :: cs) res = |
12 | positions line (c :: cs) res = |
13 positions (if c = #"\n" then line + 1 else line) cs (str c :: res) |
13 positions (if c = #"\n" then line + 1 else line) cs (str c :: res) |
14 | positions _ [] res = rev res; |
14 | positions _ [] res = rev res; |
15 in String.concat (positions start_line (String.explode txt) []) end; |
15 in String.concat (positions start_line (String.explode txt) []) end; |