# HG changeset patch # User wenzelm # Date 1459526174 -7200 # Node ID 7ac100f86863a6f76d71943ea91ad04c6840ba82 # Parent 46e6f91c4da1fdd98a072a2df39111ba3e46cfa7 tuned signature; diff -r 46e6f91c4da1 -r 7ac100f86863 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Fri Apr 01 17:49:03 2016 +0200 +++ b/src/Pure/General/position.ML Fri Apr 01 17:56:14 2016 +0200 @@ -51,7 +51,7 @@ val here_list: T list -> string type range = T * T val no_range: range - val reset_range: T -> T + val no_range_position: T -> T val range_position: range -> T val range: T * T -> range val range_of_properties: Properties.T -> range @@ -223,9 +223,9 @@ val no_range = (none, none); -fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props); +fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props); fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props); -fun range (pos, pos') = (range_position (pos, pos'), reset_range pos'); +fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos'); fun range_of_properties props = let diff -r 46e6f91c4da1 -r 7ac100f86863 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Fri Apr 01 17:49:03 2016 +0200 +++ b/src/Pure/General/symbol_pos.ML Fri Apr 01 17:56:14 2016 +0200 @@ -275,7 +275,7 @@ let val (res, _) = fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p)) - (Symbol.explode str) ([], Position.reset_range pos); + (Symbol.explode str) ([], Position.no_range_position pos); in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end; fun explode0 str = explode (str, Position.none); diff -r 46e6f91c4da1 -r 7ac100f86863 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Apr 01 17:49:03 2016 +0200 +++ b/src/Pure/Isar/token.ML Fri Apr 01 17:56:14 2016 +0200 @@ -675,7 +675,7 @@ fun make_string (s, pos) = let val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none); - val pos' = Position.reset_range pos; + val pos' = Position.no_range_position pos; in Token ((x, (pos', pos')), y, z) end; fun make_src a args = make_string a :: args; diff -r 46e6f91c4da1 -r 7ac100f86863 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Fri Apr 01 17:49:03 2016 +0200 +++ b/src/Pure/ML/ml_compiler.ML Fri Apr 01 17:56:14 2016 +0200 @@ -38,7 +38,7 @@ (* parse trees *) fun breakpoint_position loc = - let val pos = Position.reset_range (Exn_Properties.position_of_location loc) in + let val pos = Position.no_range_position (Exn_Properties.position_of_location loc) in (case Position.offset_of pos of NONE => pos | SOME 1 => pos diff -r 46e6f91c4da1 -r 7ac100f86863 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 01 17:49:03 2016 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 01 17:56:14 2016 +0200 @@ -338,7 +338,7 @@ if len <= 1 then [] else [cat_lines - (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^ + (("Ambiguous input" ^ Position.here (Position.no_range_position pos) ^ " produces " ^ string_of_int len ^ " parse trees" ^ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree) diff -r 46e6f91c4da1 -r 7ac100f86863 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Fri Apr 01 17:49:03 2016 +0200 +++ b/src/Pure/Thy/document_antiquotations.ML Fri Apr 01 17:56:14 2016 +0200 @@ -15,7 +15,7 @@ Thy_Output.antiquotation binding (Scan.succeed ()) (fn {source, ...} => fn _ => error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^ - Position.here (Position.reset_range (#1 (Token.range_of source))))) + Position.here (Position.no_range_position (#1 (Token.range_of source))))) in