--- a/src/Pure/General/symbol_pos.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Sun Nov 30 12:24:56 2014 +0100
@@ -39,9 +39,6 @@
val implode: T list -> text
val implode_range: Position.T -> Position.T -> T list -> text * Position.range
val explode: text * Position.T -> T list
- type source = {delimited: bool, text: text, range: Position.range}
- val source_explode: source -> T list
- val source_content: source -> string * Position.T
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
end;
@@ -253,16 +250,6 @@
in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
-(* full source information *)
-
-type source = {delimited: bool, text: text, range: Position.range};
-
-fun source_explode {delimited = _, text, range = (pos, _)} = explode (text, pos);
-
-fun source_content {delimited = _, text, range = (pos, _)} =
- let val syms = explode (text, pos) in (content syms, pos) end;
-
-
(* identifiers *)
local