src/Pure/PIDE/command.ML
changeset 68728 c07f6fa02c59
parent 68366 cd387c55e085
child 68729 3a02b424d5fb
     1.1 --- a/src/Pure/PIDE/command.ML	Sun Jul 29 13:18:10 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Jul 31 21:06:09 2018 +0200
     1.3 @@ -136,11 +136,11 @@
     1.4    let
     1.5      val command_reports = Outer_Syntax.command_reports thy;
     1.6  
     1.7 -    val proper_range = Token.range_of (drop_suffix Token.is_improper span);
     1.8 +    val core_range = Token.range_of (drop_suffix Token.is_improper span);
     1.9      val pos =
    1.10        (case find_first Token.is_command span of
    1.11          SOME tok => Token.pos_of tok
    1.12 -      | NONE => #1 proper_range);
    1.13 +      | NONE => #1 core_range);
    1.14  
    1.15      val token_reports = map (reports_of_token keywords) span;
    1.16      val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
    1.17 @@ -150,8 +150,8 @@
    1.18        (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
    1.19          [tr] => Toplevel.modify_init init tr
    1.20        | [] => Toplevel.ignored (#1 (Token.range_of span))
    1.21 -      | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
    1.22 -      handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
    1.23 +      | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected")
    1.24 +      handle ERROR msg => Toplevel.malformed (#1 core_range) msg
    1.25    end;
    1.26  
    1.27  end;