more operations;
authorwenzelm
Sat Dec 16 15:11:19 2017 +0100 (19 months ago)
changeset 6721301576aebc398
parent 67212 f5d44a01030c
child 67214 87038a574d09
more operations;
src/Pure/General/input.ML
     1.1 --- a/src/Pure/General/input.ML	Sat Dec 16 14:40:21 2017 +0100
     1.2 +++ b/src/Pure/General/input.ML	Sat Dec 16 15:11:19 2017 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    val pos_of: source -> Position.T
     1.5    val range_of: source -> Position.range
     1.6    val source: bool -> Symbol_Pos.text -> Position.range -> source
     1.7 +  val empty: source
     1.8    val string: string -> source
     1.9    val reset_pos: source -> source
    1.10    val source_explode: source -> Symbol_Pos.T list
    1.11 @@ -36,6 +37,8 @@
    1.12  fun source delimited text range =
    1.13    Source {delimited = delimited, text = text, range = range};
    1.14  
    1.15 +val empty = source false "" Position.no_range;
    1.16 +
    1.17  fun string text = source true text Position.no_range;
    1.18  
    1.19  fun reset_pos (Source {delimited, text, ...}) = source delimited text Position.no_range;