src/Pure/General/symbol_pos.ML
changeset 27778 3ec7a4d9ef18
parent 27763 f49f6275cefa
child 27797 9861b39a2fd5
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Aug 07 19:21:39 2008 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Aug 07 19:21:40 2008 +0200
     1.3 @@ -19,15 +19,17 @@
     1.4    val is_eof: T -> bool
     1.5    val stopper: T Scan.stopper
     1.6    val !!! : string -> (T list -> 'a) -> T list -> 'a
     1.7 -  val scan_position: T list -> Position.T * T list
     1.8 +  val scan_pos: T list -> Position.T * T list
     1.9    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.10      T list -> T list * T list
    1.11    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.12      T list -> T list * T list
    1.13    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
    1.14      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
    1.15 -  val implode: T list -> string * Position.range
    1.16 -  val explode: string * Position.T -> T list
    1.17 +  type text = string
    1.18 +  val implode: T list -> text * Position.range
    1.19 +  val implode_delim: Position.T -> Position.T -> T list -> text * Position.range
    1.20 +  val explode: text * Position.T -> T list
    1.21  end;
    1.22  
    1.23  structure SymbolPos: SYMBOL_POS =
    1.24 @@ -66,7 +68,7 @@
    1.25  fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
    1.26  fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
    1.27  
    1.28 -val scan_position = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
    1.29 +val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
    1.30  
    1.31  
    1.32  (* ML-style comments *)
    1.33 @@ -101,6 +103,8 @@
    1.34  
    1.35  (* compact representation -- with Symbol.DEL padding *)
    1.36  
    1.37 +type text = string;
    1.38 +
    1.39  local
    1.40  
    1.41  fun pad [] = []
    1.42 @@ -131,8 +135,11 @@
    1.43        in (orig_implode (pad syms), Position.range pos pos') end
    1.44    | implode [] = ("", (Position.none, Position.none));
    1.45  
    1.46 +fun implode_delim pos1 pos2 syms = implode (("", pos1) :: syms @ [("", pos2)]);
    1.47 +
    1.48  fun explode (str, pos) =
    1.49 -  fold_map (fn s => fn p => ((s, p), (Position.advance s p))) (Symbol.explode str) pos
    1.50 +  fold_map (fn s => fn p => ((s, p), (Position.advance s p)))
    1.51 +    (Symbol.explode str) (Position.reset_range pos)
    1.52    |> #1 |> filter_out (fn (s, _) => s = Symbol.DEL);
    1.53  
    1.54  end;