src/Pure/PIDE/command.ML
changeset 68729 3a02b424d5fb
parent 68728 c07f6fa02c59
child 68858 e1796b8ddbae
     1.1 --- a/src/Pure/PIDE/command.ML	Tue Jul 31 21:06:09 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Jul 31 21:11:24 2018 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4    let
     1.5      val command_reports = Outer_Syntax.command_reports thy;
     1.6  
     1.7 -    val core_range = Token.range_of (drop_suffix Token.is_improper span);
     1.8 +    val core_range = Token.range_of (drop_suffix Token.is_ignored span);
     1.9      val pos =
    1.10        (case find_first Token.is_command span of
    1.11          SOME tok => Token.pos_of tok