Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: input.ML Sprache: SML

Original von: Isabelle^©

(*  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_range: source -> string * Position.range
  val source_content: source -> string * Position.T
  val string_of: 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);

fun source_content_range source =
  let val syms = source_explode source
  in (Symbol_Pos.content syms, Symbol_Pos.range syms) end;

val source_content = source_content_range #> apsnd #1;

val string_of = source_explode #> Symbol_Pos.content;

val equal_content = (op =) o apply2 string_of;

end;

end;

¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.