src/Pure/General/symbol_pos.ML
changeset 55829 b7bdea5336dd
parent 55828 42ac3cfb89f6
child 58047 9f3826352b52
     1.1 --- a/src/Pure/General/symbol_pos.ML	Sat Mar 01 22:46:31 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Mar 01 23:17:37 2014 +0100
     1.3 @@ -37,10 +37,11 @@
     1.4    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     1.5      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
     1.6    type text = string
     1.7 -  type source = {delimited: bool, text: text, pos: Position.T}
     1.8    val implode: T list -> text
     1.9    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
    1.10    val explode: text * Position.T -> T list
    1.11 +  type source = {delimited: bool, text: text, pos: Position.T}
    1.12 +  val source_content: source -> string * Position.T
    1.13    val scan_ident: T list -> T list * T list
    1.14    val is_identifier: string -> bool
    1.15  end;
    1.16 @@ -233,7 +234,6 @@
    1.17  (* compact representation -- with Symbol.DEL padding *)
    1.18  
    1.19  type text = string;
    1.20 -type source = {delimited: bool, text: text, pos: Position.T}
    1.21  
    1.22  fun pad [] = []
    1.23    | pad [(s, _)] = [s]
    1.24 @@ -257,6 +257,14 @@
    1.25    in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
    1.26  
    1.27  
    1.28 +(* full source information *)
    1.29 +
    1.30 +type source = {delimited: bool, text: text, pos: Position.T};
    1.31 +
    1.32 +fun source_content {delimited = _, text, pos} =
    1.33 +  let val syms = explode (text, pos) in (content syms, pos) end;
    1.34 +
    1.35 +
    1.36  (* identifiers *)
    1.37  
    1.38  local