author | wenzelm |
Mon, 15 Jun 2015 13:29:57 +0200 | |
changeset 60483 | 9a566f4ac20a |
parent 56437 | b14bd153a753 |
permissions | -rw-r--r-- |
56435
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/ml_positions.ML |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
3 |
|
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
4 |
Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap. |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
5 |
*) |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
6 |
|
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
7 |
fun ml_positions start_line name txt = |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
8 |
let |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
9 |
fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res = |
56437 | 10 |
let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")" |
56435
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
11 |
in positions line cs (s :: res) end |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
12 |
| positions line (c :: cs) res = |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
13 |
positions (if c = #"\n" then line + 1 else line) cs (str c :: res) |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
14 |
| positions _ [] res = rev res; |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
15 |
in String.concat (positions start_line (String.explode txt) []) end; |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
diff
changeset
|
16 |