# HG changeset patch
# User wenzelm
# Date 1513433479 -3600
# Node ID 01576aebc398d0e20ca04e82f69336c510d94123
# Parent  f5d44a01030c7632d85b12bf78094bdb5628f703
more operations;

diff -r f5d44a01030c -r 01576aebc398 src/Pure/General/input.ML
--- 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;