# 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 ("\\", _) :: 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;