--- a/src/Pure/General/input.ML Tue Dec 09 17:40:42 2014 +0100
+++ b/src/Pure/General/input.ML Tue Dec 09 18:29:45 2014 +0100
@@ -12,6 +12,7 @@
val pos_of: source -> Position.T
val range_of: source -> Position.range
val source: bool -> Symbol_Pos.text -> Position.range -> source
+ val string: string -> source
val source_explode: source -> Symbol_Pos.T list
val source_content: source -> string
end;
@@ -30,6 +31,8 @@
fun source delimited text range =
Source {delimited = delimited, text = text, range = range};
+fun string text = source true text Position.no_range;
+
fun source_explode (Source {text, range = (pos, _), ...}) =
Symbol_Pos.explode (text, pos);