# HG changeset patch # User wenzelm # Date 1459525066 -7200 # Node ID e08c44eed27fa4db2bfa487d4aa7e63228a591a4 # Parent 99f2036f37afc1595eaa01d5eafdcea646a7cf72 tuned signature; diff -r 99f2036f37af -r e08c44eed27f src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Fri Apr 01 17:23:15 2016 +0200 +++ b/src/Pure/General/antiquote.ML Fri Apr 01 17:37:46 2016 +0200 @@ -37,7 +37,7 @@ fun range ants = if null ants then Position.no_range - else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants))); + else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants))); (* split lines *) @@ -110,9 +110,9 @@ Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> (fn (pos1, (pos2, ((body, pos3), pos4))) => - {start = Position.set_range (pos1, pos2), - stop = Position.set_range (pos3, pos4), - range = Position.range pos1 pos4, + {start = Position.range_position (pos1, pos2), + stop = Position.range_position (pos3, pos4), + range = Position.range (pos1, pos4), body = body}); val scan_antiquote = diff -r 99f2036f37af -r e08c44eed27f src/Pure/General/position.ML --- a/src/Pure/General/position.ML Fri Apr 01 17:23:15 2016 +0200 +++ b/src/Pure/General/position.ML Fri Apr 01 17:37:46 2016 +0200 @@ -51,9 +51,9 @@ val here_list: T list -> string type range = T * T val no_range: range - val set_range: range -> T + val range_position: range -> T + val range: T * T -> range val reset_range: T -> T - val range: T -> T -> range val range_of_properties: Properties.T -> range val properties_of_range: range -> Properties.T val thread_data: unit -> T @@ -223,11 +223,11 @@ val no_range = (none, none); -fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props); +fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props); +fun range (pos, pos') = (range_position (pos, pos'), pos'); + fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props); -fun range pos pos' = (set_range (pos, pos'), pos'); - fun range_of_properties props = let val pos = of_properties props; diff -r 99f2036f37af -r e08c44eed27f src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Fri Apr 01 17:23:15 2016 +0200 +++ b/src/Pure/General/symbol_pos.ML Fri Apr 01 17:37:46 2016 +0200 @@ -63,7 +63,7 @@ fun range (syms as (_, pos) :: _) = let val pos' = List.last syms |-> Position.advance - in Position.range pos pos' end + in Position.range (pos, pos') end | range [] = Position.no_range; diff -r 99f2036f37af -r e08c44eed27f src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Apr 01 17:23:15 2016 +0200 +++ b/src/Pure/Isar/token.ML Fri Apr 01 17:37:46 2016 +0200 @@ -183,13 +183,13 @@ fun pos_of (Token ((_, (pos, _)), _, _)) = pos; fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; -fun reset_pos pos (Token ((x, _), y, z)) = +fun reset_range pos (Token ((x, _), y, z)) = let val pos' = Position.reset_range pos in Token ((x, (pos', pos')), y, z) end; fun range_of (toks as tok :: _) = let val pos' = end_pos_of (List.last toks) - in Position.range (pos_of tok) pos' end + in Position.range (pos_of tok, pos') end | range_of [] = Position.no_range; @@ -666,7 +666,7 @@ fun make ((k, n), s) pos = let val pos' = Position.advance_offset n pos; - val range = Position.range pos pos'; + val range = Position.range (pos, pos'); val tok = if 0 <= k andalso k < Vector.length immediate_kinds then Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot) @@ -678,7 +678,7 @@ fun make_string (s, pos) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none) - |> reset_pos pos; + |> reset_range pos; fun make_src a args = make_string a :: args; diff -r 99f2036f37af -r e08c44eed27f src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Fri Apr 01 17:23:15 2016 +0200 +++ b/src/Pure/ML/ml_lex.ML Fri Apr 01 17:37:46 2016 +0200 @@ -312,7 +312,7 @@ let val pos1 = List.last syms |-> Position.advance; val pos2 = Position.advance Symbol.space pos1; - in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end; + in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end; val scan = if SML then scan_sml else scan_ml_antiq; fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok) diff -r 99f2036f37af -r e08c44eed27f src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Fri Apr 01 17:23:15 2016 +0200 +++ b/src/Pure/Syntax/mixfix.ML Fri Apr 01 17:37:46 2016 +0200 @@ -71,7 +71,7 @@ | range_of (Binder (_, _, _, range)) = range | range_of (Structure range) = range; -val pos_of = Position.set_range o range_of; +val pos_of = Position.range_position o range_of; fun reset_pos NoSyn = NoSyn | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range) diff -r 99f2036f37af -r e08c44eed27f src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Fri Apr 01 17:23:15 2016 +0200 +++ b/src/Pure/Tools/rail.ML Fri Apr 01 17:37:46 2016 +0200 @@ -53,7 +53,7 @@ fun range_of (toks as tok :: _) = let val pos' = end_pos_of (List.last toks) - in Position.range (pos_of tok) pos' end + in Position.range (pos_of tok, pos') end | range_of [] = Position.no_range; fun kind_of (Token (_, (k, _))) = k; @@ -116,7 +116,7 @@ scan_keyword >> (token Keyword o single) || Lexicon.scan_id >> token Ident || Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) => - [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]); + [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]); val scan = Scan.repeats scan_token --| @@ -188,7 +188,7 @@ let fun reports r = if r = Position.no_range then [] - else [(Position.set_range r, Markup.expression)]; + else [(Position.range_position r, Markup.expression)]; fun trees (CAT (ts, r)) = reports r @ maps tree ts and tree (BAR (Ts, r)) = reports r @ maps trees Ts | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2