src/Pure/General/input.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/input.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -0,0 +1,43 @@
+(*  Title:      Pure/General/input.ML
+    Author:     Makarius
+
+Generic input with position information.
+*)
+
+signature INPUT =
+sig
+  type source
+  val is_delimited: source -> bool
+  val text_of: source -> Symbol_Pos.text
+  val pos_of: source -> Position.T
+  val range_of: source -> Position.range
+  val source: bool -> Symbol_Pos.text -> Position.range -> source
+  val source_explode: source -> Symbol_Pos.T list
+  val source_content: source -> string * Position.T
+end;
+
+structure Input: INPUT =
+struct
+
+abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}
+with
+
+fun is_delimited (Source {delimited, ...}) = delimited;
+fun text_of (Source {text, ...}) = text;
+fun pos_of (Source {range = (pos, _), ...}) = pos;
+fun range_of (Source {range, ...}) = range;
+
+fun source delimited text range =
+  Source {delimited = delimited, text = text, range = range};
+
+fun source_explode (Source {text, range = (pos, _), ...}) =
+  Symbol_Pos.explode (text, pos);
+
+fun source_content (Source {text, range = (pos, _), ...}) =
+  let val syms = Symbol_Pos.explode (text, pos)
+  in (Symbol_Pos.content syms, pos) end;
+
+end;
+
+end;
+