src/Pure/General/input.ML

clarified overall range: include delimiters;

(*  Title:      Pure/General/input.ML
    Author:     Makarius

Generic input with position information.
*)

signature INPUT =
sig
  type source
  val is_delimited: source -> bool
  val text_of: source -> Symbol_Pos.text
  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 cartouche_content: Symbol_Pos.T list -> source
  val reset_pos: source -> source
  val source_explode: source -> Symbol_Pos.T list
  val source_content: source -> string
  val equal_content: source * source -> bool
end;

structure Input: INPUT =
struct

abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}
with


(* source *)

fun is_delimited (Source {delimited, ...}) = delimited;
fun text_of (Source {text, ...}) = text;
fun pos_of (Source {range = (pos, _), ...}) = pos;
fun range_of (Source {range, ...}) = range;

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 cartouche_content syms =
  let
    val range = Symbol_Pos.range syms;
    val (text, _) = Symbol_Pos.implode_range range (Symbol_Pos.cartouche_content syms);
  in source true text range end;

fun reset_pos (Source {delimited, text, ...}) = source delimited text Position.no_range;


(* content *)

fun source_explode (Source {text, range = (pos, _), ...}) =
  Symbol_Pos.explode (text, pos);

val source_content = source_explode #> Symbol_Pos.content;

val equal_content = (op =) o apply2 source_content;

end;

end;