--- 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
--- 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);
--- 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;
--- 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
--- 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)
--- 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