clarified Token.range_of in accordance to Symbol_Pos.range;
authorwenzelm
Mon Feb 24 10:48:34 2014 +0100 (2014-02-24)
changeset 557094e5a83a46ded
parent 55708 f4b114070675
child 55710 2d623ab55672
clarified Token.range_of in accordance to Symbol_Pos.range;
eliminated redundant Position.set_range, which is already included in Position.range;
src/Pure/General/symbol_pos.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Mon Feb 24 10:17:29 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Feb 24 10:48:34 2014 +0100
     1.3 @@ -178,8 +178,8 @@
     1.4  fun cartouche_content syms =
     1.5    let
     1.6      fun err () =
     1.7 -      error ("Malformed text cartouche: " ^ quote (content syms) ^
     1.8 -        Position.here (Position.set_range (range syms)));
     1.9 +      error ("Malformed text cartouche: "
    1.10 +        ^ quote (content syms) ^ Position.here (#1 (range syms)));
    1.11    in
    1.12      (case syms of
    1.13        ("\\<open>", _) :: rest =>
     2.1 --- a/src/Pure/Isar/method.ML	Mon Feb 24 10:17:29 2014 +0100
     2.2 +++ b/src/Pure/Isar/method.ML	Mon Feb 24 10:48:34 2014 +0100
     2.3 @@ -425,7 +425,7 @@
     2.4  in
     2.5  
     2.6  val parse =
     2.7 -  Scan.trace meth3 >> (fn (m, toks) => (m, Token.position_range_of toks));
     2.8 +  Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks));
     2.9  
    2.10  end;
    2.11  
    2.12 @@ -438,7 +438,7 @@
    2.13    | text (SOME (txt, _)) = SOME txt;
    2.14  
    2.15  fun position NONE = Position.none
    2.16 -  | position (SOME (_, range)) = Position.set_range range;
    2.17 +  | position (SOME (_, (pos, _))) = pos;
    2.18  
    2.19  
    2.20  (* theory setup *)
     3.1 --- a/src/Pure/Isar/proof.ML	Mon Feb 24 10:17:29 2014 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Mon Feb 24 10:48:34 2014 +0100
     3.3 @@ -825,8 +825,7 @@
     3.4      val (finish_text, terminal_pos, finished_pos) =
     3.5        (case opt_text of
     3.6          NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
     3.7 -      | SOME (text, (pos, end_pos)) =>
     3.8 -          (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
     3.9 +      | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
    3.10    in
    3.11      Seq.APPEND (fn state =>
    3.12        state
    3.13 @@ -861,11 +860,11 @@
    3.14  
    3.15  fun apply_end text = assert_forward #> refine_end text;
    3.16  
    3.17 -fun apply_results (text, range) =
    3.18 -  Seq.APPEND (apply text #> Seq.make_results, method_error "" (Position.set_range range));
    3.19 +fun apply_results (text, (pos, _)) =
    3.20 +  Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
    3.21  
    3.22 -fun apply_end_results (text, range) =
    3.23 -  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" (Position.set_range range));
    3.24 +fun apply_end_results (text, (pos, _)) =
    3.25 +  Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
    3.26  
    3.27  
    3.28  
     4.1 --- a/src/Pure/Isar/token.ML	Mon Feb 24 10:17:29 2014 +0100
     4.2 +++ b/src/Pure/Isar/token.ML	Mon Feb 24 10:48:34 2014 +0100
     4.3 @@ -17,7 +17,7 @@
     4.4    type T
     4.5    val str_of_kind: kind -> string
     4.6    val pos_of: T -> Position.T
     4.7 -  val position_range_of: T list -> Position.range
     4.8 +  val range_of: T list -> Position.range
     4.9    val eof: T
    4.10    val is_eof: T -> bool
    4.11    val not_eof: T -> bool
    4.12 @@ -131,8 +131,10 @@
    4.13  fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
    4.14  fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
    4.15  
    4.16 -fun position_range_of [] = Position.no_range
    4.17 -  | position_range_of toks = (pos_of (hd toks), end_pos_of (List.last toks));
    4.18 +fun range_of (toks as tok :: _) =
    4.19 +      let val pos' = end_pos_of (List.last toks)
    4.20 +      in Position.range (pos_of tok) pos' end
    4.21 +  | range_of [] = Position.no_range;
    4.22  
    4.23  
    4.24  (* control tokens *)
     5.1 --- a/src/Pure/PIDE/command.ML	Mon Feb 24 10:17:29 2014 +0100
     5.2 +++ b/src/Pure/PIDE/command.ML	Mon Feb 24 10:48:34 2014 +0100
     5.3 @@ -128,12 +128,11 @@
     5.4      val outer_syntax = #2 (Outer_Syntax.get_syntax ());
     5.5      val command_reports = Outer_Syntax.command_reports outer_syntax;
     5.6  
     5.7 -    val proper_range =
     5.8 -      Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
     5.9 +    val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
    5.10      val pos =
    5.11        (case find_first Token.is_command span of
    5.12          SOME tok => Token.pos_of tok
    5.13 -      | NONE => proper_range);
    5.14 +      | NONE => #1 proper_range);
    5.15  
    5.16      val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
    5.17      val _ = Position.reports_text (token_reports @ maps command_reports span);
    5.18 @@ -145,9 +144,9 @@
    5.19            if Keyword.is_control (Toplevel.name_of tr) then
    5.20              Toplevel.malformed pos "Illegal control command"
    5.21            else Toplevel.modify_init init tr
    5.22 -      | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
    5.23 -      | _ => Toplevel.malformed proper_range "Exactly one command expected")
    5.24 -      handle ERROR msg => Toplevel.malformed proper_range msg
    5.25 +      | [] => Toplevel.ignored (#1 (Token.range_of span))
    5.26 +      | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
    5.27 +      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
    5.28    end;
    5.29  
    5.30