added content;
authorwenzelm
Sat Aug 09 00:09:29 2008 +0200 (2008-08-09)
changeset 277979861b39a2fd5
parent 27796 a6da5f68e776
child 27798 b96c73f11a23
added content;
simplified implode: interface and permissive padding via Position.distance_of;
added range;
renamed implode_delim to implode_range;
src/Pure/General/symbol_pos.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Sat Aug 09 00:09:26 2008 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Aug 09 00:09:29 2008 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  signature SYMBOL_POS =
     1.5  sig
     1.6    include BASIC_SYMBOL_POS
     1.7 +  val content: T list -> string
     1.8    val is_eof: T -> bool
     1.9    val stopper: T Scan.stopper
    1.10    val !!! : string -> (T list -> 'a) -> T list -> 'a
    1.11 @@ -27,8 +28,9 @@
    1.12    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
    1.13      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
    1.14    type text = string
    1.15 -  val implode: T list -> text * Position.range
    1.16 -  val implode_delim: Position.T -> Position.T -> T list -> text * Position.range
    1.17 +  val implode: T list -> text
    1.18 +  val range: T list -> Position.range
    1.19 +  val implode_range: 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 @@ -40,6 +42,7 @@
    1.24  type T = Symbol.symbol * Position.T;
    1.25  
    1.26  fun symbol ((s, _): T) = s;
    1.27 +val content = implode o map symbol;
    1.28  
    1.29  
    1.30  (* stopper *)
    1.31 @@ -105,37 +108,24 @@
    1.32  
    1.33  type text = string;
    1.34  
    1.35 -local
    1.36 -
    1.37  fun pad [] = []
    1.38    | pad [(s, _)] = [s]
    1.39    | pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) =
    1.40        let
    1.41 -        fun err () =
    1.42 -          raise Fail ("Misaligned symbols: " ^
    1.43 -            quote s1 ^ Position.str_of pos1 ^ " " ^
    1.44 -            quote s2 ^ Position.str_of pos2);
    1.45 -
    1.46          val end_pos1 = Position.advance s1 pos1;
    1.47 -        val _ = Position.line_of end_pos1 = Position.line_of pos2 orelse err ();
    1.48 -        val d =
    1.49 -          (case (Position.column_of end_pos1, Position.column_of pos2) of
    1.50 -            (NONE, NONE) => 0
    1.51 -          | (SOME n1, SOME n2) => n2 - n1
    1.52 -          | _ => err ());
    1.53 -        val _ = d >= 0 orelse err ();
    1.54 +        val d = Int.max (0, Position.distance_of end_pos1 pos2);
    1.55        in s1 :: replicate d Symbol.DEL @ pad rest end;
    1.56  
    1.57 -val orig_implode = implode;
    1.58 -
    1.59 -in
    1.60 +val implode = implode o pad;
    1.61  
    1.62 -fun implode (syms as (_, pos) :: _) =
    1.63 +fun range (syms as (_, pos) :: _) =
    1.64        let val pos' = List.last syms |-> Position.advance
    1.65 -      in (orig_implode (pad syms), Position.range pos pos') end
    1.66 -  | implode [] = ("", (Position.none, Position.none));
    1.67 +      in Position.range pos pos' end
    1.68 +  | range [] = Position.no_range;
    1.69  
    1.70 -fun implode_delim pos1 pos2 syms = implode (("", pos1) :: syms @ [("", pos2)]);
    1.71 +fun implode_range pos1 pos2 syms =
    1.72 +  let val syms' = (("", pos1) :: syms @ [("", pos2)])
    1.73 +  in (implode syms', range syms') end;
    1.74  
    1.75  fun explode (str, pos) =
    1.76    fold_map (fn s => fn p => ((s, p), (Position.advance s p)))
    1.77 @@ -144,7 +134,5 @@
    1.78  
    1.79  end;
    1.80  
    1.81 -end;
    1.82 -
    1.83  structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos;   (*not open by default*)
    1.84