--- a/src/Pure/General/input.ML Sat Dec 16 14:40:21 2017 +0100
+++ b/src/Pure/General/input.ML Sat Dec 16 15:11:19 2017 +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 empty: source
val string: string -> source
val reset_pos: source -> source
val source_explode: source -> Symbol_Pos.T list
@@ -36,6 +37,8 @@
fun source delimited text range =
Source {delimited = delimited, text = text, range = range};
+val empty = source false "" Position.no_range;
+
fun string text = source true text Position.no_range;
fun reset_pos (Source {delimited, text, ...}) = source delimited text Position.no_range;