# HG changeset patch
# User wenzelm
# Date 1393235314 -3600
# Node ID 4e5a83a46ded44d54269bc170b8a80d971001298
# Parent  f4b114070675be8f4ab922dffe21892f28ad698e
clarified Token.range_of in accordance to Symbol_Pos.range;
eliminated redundant Position.set_range, which is already included in Position.range;

diff -r f4b114070675 -r 4e5a83a46ded src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon Feb 24 10:17:29 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Mon Feb 24 10:48:34 2014 +0100
@@ -178,8 +178,8 @@
 fun cartouche_content syms =
   let
     fun err () =
-      error ("Malformed text cartouche: " ^ quote (content syms) ^
-        Position.here (Position.set_range (range syms)));
+      error ("Malformed text cartouche: "
+        ^ quote (content syms) ^ Position.here (#1 (range syms)));
   in
     (case syms of
       ("\\<open>", _) :: rest =>
diff -r f4b114070675 -r 4e5a83a46ded src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Feb 24 10:17:29 2014 +0100
+++ b/src/Pure/Isar/method.ML	Mon Feb 24 10:48:34 2014 +0100
@@ -425,7 +425,7 @@
 in
 
 val parse =
-  Scan.trace meth3 >> (fn (m, toks) => (m, Token.position_range_of toks));
+  Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks));
 
 end;
 
@@ -438,7 +438,7 @@
   | text (SOME (txt, _)) = SOME txt;
 
 fun position NONE = Position.none
-  | position (SOME (_, range)) = Position.set_range range;
+  | position (SOME (_, (pos, _))) = pos;
 
 
 (* theory setup *)
diff -r f4b114070675 -r 4e5a83a46ded src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Feb 24 10:17:29 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Feb 24 10:48:34 2014 +0100
@@ -825,8 +825,7 @@
     val (finish_text, terminal_pos, finished_pos) =
       (case opt_text of
         NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
-      | SOME (text, (pos, end_pos)) =>
-          (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
+      | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
   in
     Seq.APPEND (fn state =>
       state
@@ -861,11 +860,11 @@
 
 fun apply_end text = assert_forward #> refine_end text;
 
-fun apply_results (text, range) =
-  Seq.APPEND (apply text #> Seq.make_results, method_error "" (Position.set_range range));
+fun apply_results (text, (pos, _)) =
+  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
 
-fun apply_end_results (text, range) =
-  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" (Position.set_range range));
+fun apply_end_results (text, (pos, _)) =
+  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
 
 
 
diff -r f4b114070675 -r 4e5a83a46ded src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Feb 24 10:17:29 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Feb 24 10:48:34 2014 +0100
@@ -17,7 +17,7 @@
   type T
   val str_of_kind: kind -> string
   val pos_of: T -> Position.T
-  val position_range_of: T list -> Position.range
+  val range_of: T list -> Position.range
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -131,8 +131,10 @@
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
-fun position_range_of [] = Position.no_range
-  | position_range_of toks = (pos_of (hd toks), end_pos_of (List.last toks));
+fun range_of (toks as tok :: _) =
+      let val pos' = end_pos_of (List.last toks)
+      in Position.range (pos_of tok) pos' end
+  | range_of [] = Position.no_range;
 
 
 (* control tokens *)
diff -r f4b114070675 -r 4e5a83a46ded src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Feb 24 10:17:29 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Mon Feb 24 10:48:34 2014 +0100
@@ -128,12 +128,11 @@
     val outer_syntax = #2 (Outer_Syntax.get_syntax ());
     val command_reports = Outer_Syntax.command_reports outer_syntax;
 
-    val proper_range =
-      Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
+    val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
     val pos =
       (case find_first Token.is_command span of
         SOME tok => Token.pos_of tok
-      | NONE => proper_range);
+      | NONE => #1 proper_range);
 
     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
     val _ = Position.reports_text (token_reports @ maps command_reports span);
@@ -145,9 +144,9 @@
           if Keyword.is_control (Toplevel.name_of tr) then
             Toplevel.malformed pos "Illegal control command"
           else Toplevel.modify_init init tr
-      | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
-      | _ => Toplevel.malformed proper_range "Exactly one command expected")
-      handle ERROR msg => Toplevel.malformed proper_range msg
+      | [] => Toplevel.ignored (#1 (Token.range_of span))
+      | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
+      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
   end;