equal
deleted
inserted
replaced
66 fun input line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res = |
66 fun input line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res = |
67 let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")" |
67 let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")" |
68 in input line cs (s :: res) end |
68 in input line cs (s :: res) end |
69 | input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" :: |
69 | input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" :: |
70 #"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res = |
70 #"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res = |
71 input line cs (ML_Pretty.make_string_global :: res) |
71 input line cs (ML_Pretty.make_string_fn :: res) |
72 | input line (#"\\" :: #"<" :: cs) res = input line cs ("\092\092<" :: res) |
72 | input line (#"\\" :: #"<" :: cs) res = input line cs ("\092\092<" :: res) |
73 | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res) |
73 | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res) |
74 | input line (c :: cs) res = input line cs (str c :: res) |
74 | input line (c :: cs) res = input line cs (str c :: res) |
75 | input _ [] res = rev res; |
75 | input _ [] res = rev res; |
76 in String.concat (input start_line (String.explode txt) []) end; |
76 in String.concat (input start_line (String.explode txt) []) end; |