equal
deleted
inserted
replaced
1 (* Title: Pure/RAW/ml_positions.ML |
|
2 Author: Makarius |
|
3 |
|
4 Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap. |
|
5 *) |
|
6 |
|
7 fun ml_positions start_line name txt = |
|
8 let |
|
9 fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res = |
|
10 let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")" |
|
11 in positions line cs (s :: res) end |
|
12 | positions line (c :: cs) res = |
|
13 positions (if c = #"\n" then line + 1 else line) cs (str c :: res) |
|
14 | positions _ [] res = rev res; |
|
15 in String.concat (positions start_line (String.explode txt) []) end; |
|
16 |
|