29 |
29 |
30 fun drop_newline s = |
30 fun drop_newline s = |
31 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
31 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
32 else s; |
32 else s; |
33 |
33 |
34 fun ml_positions start_line name txt = |
34 fun ml_input start_line name txt = |
35 let |
35 let |
36 fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res = |
36 fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res = |
37 let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")" |
37 let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")" |
38 in positions line cs (s :: res) end |
38 in positions line cs (s :: res) end |
39 | positions line (c :: cs) res = |
39 | positions line (#"\\" :: #"<" :: cs) res = positions line cs ("\\\\<" :: res) |
40 positions (if c = #"\n" then line + 1 else line) cs (str c :: res) |
40 | positions line (#"\n" :: cs) res = positions (line + 1) cs ("\n" :: res) |
|
41 | positions line (c :: cs) res = positions line cs (str c :: res) |
41 | positions _ [] res = rev res; |
42 | positions _ [] res = rev res; |
42 in String.concat (positions start_line (String.explode txt) []) end; |
43 in String.concat (positions start_line (String.explode txt) []) end; |
43 |
44 |
44 fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text = |
45 fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text = |
45 let |
46 let |
46 val _ = Secure.deny_ml (); |
47 val _ = Secure.deny_ml (); |
47 |
48 |
48 val current_line = Unsynchronized.ref line; |
49 val current_line = Unsynchronized.ref line; |
49 val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text)); |
50 val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text)); |
50 val out_buffer = Unsynchronized.ref ([]: string list); |
51 val out_buffer = Unsynchronized.ref ([]: string list); |
51 fun output () = drop_newline (implode (rev (! out_buffer))); |
52 fun output () = drop_newline (implode (rev (! out_buffer))); |
52 |
53 |
53 fun get () = |
54 fun get () = |
54 (case ! in_buffer of |
55 (case ! in_buffer of |