# HG changeset patch
# User wenzelm
# Date 1418146185 -3600
# Node ID caddfa6ca534a279776cbf9047c3d0c8f3566af1
# Parent  77351f2051f5de04fb2f035d8ca17ac765519a20
tuned signature;

diff -r 77351f2051f5 -r caddfa6ca534 src/Pure/General/input.ML
--- 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);