tuned signature;
authorwenzelm
Fri Apr 01 17:37:46 2016 +0200 (2016-04-01)
changeset 62797e08c44eed27f
parent 62796 99f2036f37af
child 62798 2948681ea85f
tuned signature;
src/Pure/General/antiquote.ML
src/Pure/General/position.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_lex.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Tools/rail.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Fri Apr 01 17:23:15 2016 +0200
     1.2 +++ b/src/Pure/General/antiquote.ML	Fri Apr 01 17:37:46 2016 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  
     1.5  fun range ants =
     1.6    if null ants then Position.no_range
     1.7 -  else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants)));
     1.8 +  else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
     1.9  
    1.10  
    1.11  (* split lines *)
    1.12 @@ -110,9 +110,9 @@
    1.13      Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
    1.14        (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
    1.15      (fn (pos1, (pos2, ((body, pos3), pos4))) =>
    1.16 -      {start = Position.set_range (pos1, pos2),
    1.17 -       stop = Position.set_range (pos3, pos4),
    1.18 -       range = Position.range pos1 pos4,
    1.19 +      {start = Position.range_position (pos1, pos2),
    1.20 +       stop = Position.range_position (pos3, pos4),
    1.21 +       range = Position.range (pos1, pos4),
    1.22         body = body});
    1.23  
    1.24  val scan_antiquote =
     2.1 --- a/src/Pure/General/position.ML	Fri Apr 01 17:23:15 2016 +0200
     2.2 +++ b/src/Pure/General/position.ML	Fri Apr 01 17:37:46 2016 +0200
     2.3 @@ -51,9 +51,9 @@
     2.4    val here_list: T list -> string
     2.5    type range = T * T
     2.6    val no_range: range
     2.7 -  val set_range: range -> T
     2.8 +  val range_position: range -> T
     2.9 +  val range: T * T -> range
    2.10    val reset_range: T -> T
    2.11 -  val range: T -> T -> range
    2.12    val range_of_properties: Properties.T -> range
    2.13    val properties_of_range: range -> Properties.T
    2.14    val thread_data: unit -> T
    2.15 @@ -223,11 +223,11 @@
    2.16  
    2.17  val no_range = (none, none);
    2.18  
    2.19 -fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
    2.20 +fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
    2.21 +fun range (pos, pos') = (range_position (pos, pos'), pos');
    2.22 +
    2.23  fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
    2.24  
    2.25 -fun range pos pos' = (set_range (pos, pos'), pos');
    2.26 -
    2.27  fun range_of_properties props =
    2.28    let
    2.29      val pos = of_properties props;
     3.1 --- a/src/Pure/General/symbol_pos.ML	Fri Apr 01 17:23:15 2016 +0200
     3.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Apr 01 17:37:46 2016 +0200
     3.3 @@ -63,7 +63,7 @@
     3.4  
     3.5  fun range (syms as (_, pos) :: _) =
     3.6        let val pos' = List.last syms |-> Position.advance
     3.7 -      in Position.range pos pos' end
     3.8 +      in Position.range (pos, pos') end
     3.9    | range [] = Position.no_range;
    3.10  
    3.11  
     4.1 --- a/src/Pure/Isar/token.ML	Fri Apr 01 17:23:15 2016 +0200
     4.2 +++ b/src/Pure/Isar/token.ML	Fri Apr 01 17:37:46 2016 +0200
     4.3 @@ -183,13 +183,13 @@
     4.4  fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
     4.5  fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
     4.6  
     4.7 -fun reset_pos pos (Token ((x, _), y, z)) =
     4.8 +fun reset_range pos (Token ((x, _), y, z)) =
     4.9    let val pos' = Position.reset_range pos
    4.10    in Token ((x, (pos', pos')), y, z) end;
    4.11  
    4.12  fun range_of (toks as tok :: _) =
    4.13        let val pos' = end_pos_of (List.last toks)
    4.14 -      in Position.range (pos_of tok) pos' end
    4.15 +      in Position.range (pos_of tok, pos') end
    4.16    | range_of [] = Position.no_range;
    4.17  
    4.18  
    4.19 @@ -666,7 +666,7 @@
    4.20  fun make ((k, n), s) pos =
    4.21    let
    4.22      val pos' = Position.advance_offset n pos;
    4.23 -    val range = Position.range pos pos';
    4.24 +    val range = Position.range (pos, pos');
    4.25      val tok =
    4.26        if 0 <= k andalso k < Vector.length immediate_kinds then
    4.27          Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
    4.28 @@ -678,7 +678,7 @@
    4.29  
    4.30  fun make_string (s, pos) =
    4.31    #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none)
    4.32 -  |> reset_pos pos;
    4.33 +  |> reset_range pos;
    4.34  
    4.35  fun make_src a args = make_string a :: args;
    4.36  
     5.1 --- a/src/Pure/ML/ml_lex.ML	Fri Apr 01 17:23:15 2016 +0200
     5.2 +++ b/src/Pure/ML/ml_lex.ML	Fri Apr 01 17:37:46 2016 +0200
     5.3 @@ -312,7 +312,7 @@
     5.4          let
     5.5            val pos1 = List.last syms |-> Position.advance;
     5.6            val pos2 = Position.advance Symbol.space pos1;
     5.7 -        in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
     5.8 +        in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
     5.9  
    5.10      val scan = if SML then scan_sml else scan_ml_antiq;
    5.11      fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
     6.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 01 17:23:15 2016 +0200
     6.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 01 17:37:46 2016 +0200
     6.3 @@ -71,7 +71,7 @@
     6.4    | range_of (Binder (_, _, _, range)) = range
     6.5    | range_of (Structure range) = range;
     6.6  
     6.7 -val pos_of = Position.set_range o range_of;
     6.8 +val pos_of = Position.range_position o range_of;
     6.9  
    6.10  fun reset_pos NoSyn = NoSyn
    6.11    | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)
     7.1 --- a/src/Pure/Tools/rail.ML	Fri Apr 01 17:23:15 2016 +0200
     7.2 +++ b/src/Pure/Tools/rail.ML	Fri Apr 01 17:37:46 2016 +0200
     7.3 @@ -53,7 +53,7 @@
     7.4  
     7.5  fun range_of (toks as tok :: _) =
     7.6        let val pos' = end_pos_of (List.last toks)
     7.7 -      in Position.range (pos_of tok) pos' end
     7.8 +      in Position.range (pos_of tok, pos') end
     7.9    | range_of [] = Position.no_range;
    7.10  
    7.11  fun kind_of (Token (_, (k, _))) = k;
    7.12 @@ -116,7 +116,7 @@
    7.13    scan_keyword >> (token Keyword o single) ||
    7.14    Lexicon.scan_id >> token Ident ||
    7.15    Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
    7.16 -    [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
    7.17 +    [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]);
    7.18  
    7.19  val scan =
    7.20    Scan.repeats scan_token --|
    7.21 @@ -188,7 +188,7 @@
    7.22      let
    7.23        fun reports r =
    7.24          if r = Position.no_range then []
    7.25 -        else [(Position.set_range r, Markup.expression)];
    7.26 +        else [(Position.range_position r, Markup.expression)];
    7.27        fun trees (CAT (ts, r)) = reports r @ maps tree ts
    7.28        and tree (BAR (Ts, r)) = reports r @ maps trees Ts
    7.29          | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2