# 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