src/Pure/Isar/outer_syntax.ML
changeset 68729 3a02b424d5fb
parent 68184 6c693b2700b3
child 69289 bf6937af7fe8
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 31 21:06:09 2018 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 31 21:11:24 2018 +0200
     1.3 @@ -233,7 +233,7 @@
     1.4  fun ship span =
     1.5    let
     1.6      val kind =
     1.7 -      if forall Token.is_improper span then Command_Span.Ignored_Span
     1.8 +      if forall Token.is_ignored span then Command_Span.Ignored_Span
     1.9        else if exists Token.is_error span then Command_Span.Malformed_Span
    1.10        else
    1.11          (case find_first Token.is_command span of
    1.12 @@ -241,18 +241,18 @@
    1.13          | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
    1.14    in cons (Command_Span.Span (kind, span)) end;
    1.15  
    1.16 -fun flush (result, content, improper) =
    1.17 +fun flush (result, content, ignored) =
    1.18    result
    1.19    |> not (null content) ? ship (rev content)
    1.20 -  |> not (null improper) ? ship (rev improper);
    1.21 +  |> not (null ignored) ? ship (rev ignored);
    1.22  
    1.23 -fun parse tok (result, content, improper) =
    1.24 -  if Token.is_improper tok then (result, content, tok :: improper)
    1.25 +fun parse tok (result, content, ignored) =
    1.26 +  if Token.is_ignored tok then (result, content, tok :: ignored)
    1.27    else if Token.is_command_modifier tok orelse
    1.28      Token.is_command tok andalso
    1.29        (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
    1.30 -  then (flush (result, content, improper), [tok], [])
    1.31 -  else (result, tok :: (improper @ content), []);
    1.32 +  then (flush (result, content, ignored), [tok], [])
    1.33 +  else (result, tok :: (ignored @ content), []);
    1.34  
    1.35  in
    1.36