src/Pure/General/position.ML
changeset 62797 e08c44eed27f
parent 62750 3f8f7aa1b11e
child 62798 2948681ea85f
     1.1 --- a/src/Pure/General/position.ML	Fri Apr 01 17:23:15 2016 +0200
     1.2 +++ b/src/Pure/General/position.ML	Fri Apr 01 17:37:46 2016 +0200
     1.3 @@ -51,9 +51,9 @@
     1.4    val here_list: T list -> string
     1.5    type range = T * T
     1.6    val no_range: range
     1.7 -  val set_range: range -> T
     1.8 +  val range_position: range -> T
     1.9 +  val range: T * T -> range
    1.10    val reset_range: T -> T
    1.11 -  val range: T -> T -> range
    1.12    val range_of_properties: Properties.T -> range
    1.13    val properties_of_range: range -> Properties.T
    1.14    val thread_data: unit -> T
    1.15 @@ -223,11 +223,11 @@
    1.16  
    1.17  val no_range = (none, none);
    1.18  
    1.19 -fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
    1.20 +fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
    1.21 +fun range (pos, pos') = (range_position (pos, pos'), pos');
    1.22 +
    1.23  fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
    1.24  
    1.25 -fun range pos pos' = (set_range (pos, pos'), pos');
    1.26 -
    1.27  fun range_of_properties props =
    1.28    let
    1.29      val pos = of_properties props;