src/Pure/PIDE/command.ML
changeset 55709 4e5a83a46ded
parent 55708 f4b114070675
child 55788 67699e08e969
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Feb 24 10:17:29 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Feb 24 10:48:34 2014 +0100
     1.3 @@ -128,12 +128,11 @@
     1.4      val outer_syntax = #2 (Outer_Syntax.get_syntax ());
     1.5      val command_reports = Outer_Syntax.command_reports outer_syntax;
     1.6  
     1.7 -    val proper_range =
     1.8 -      Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
     1.9 +    val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
    1.10      val pos =
    1.11        (case find_first Token.is_command span of
    1.12          SOME tok => Token.pos_of tok
    1.13 -      | NONE => proper_range);
    1.14 +      | NONE => #1 proper_range);
    1.15  
    1.16      val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
    1.17      val _ = Position.reports_text (token_reports @ maps command_reports span);
    1.18 @@ -145,9 +144,9 @@
    1.19            if Keyword.is_control (Toplevel.name_of tr) then
    1.20              Toplevel.malformed pos "Illegal control command"
    1.21            else Toplevel.modify_init init tr
    1.22 -      | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
    1.23 -      | _ => Toplevel.malformed proper_range "Exactly one command expected")
    1.24 -      handle ERROR msg => Toplevel.malformed proper_range msg
    1.25 +      | [] => Toplevel.ignored (#1 (Token.range_of span))
    1.26 +      | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
    1.27 +      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
    1.28    end;
    1.29  
    1.30