src/Pure/Thy/thy_output.ML
changeset 59939 7d46aa03696e
parent 59924 801b979ec0c2
child 60094 96a4765ba7d1
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Apr 06 17:28:07 2015 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Apr 06 22:11:01 2015 +0200
     1.3 @@ -384,10 +384,10 @@
     1.4          in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
     1.5  
     1.6      val command = Scan.peek (fn d =>
     1.7 -      Scan.optional (Scan.one Token.is_private -- improper >> op ::) [] --
     1.8 +      Scan.optional (Scan.one Token.is_command_modifier -- improper >> op ::) [] --
     1.9        Scan.one Token.is_command -- Scan.repeat tag
    1.10 -      >> (fn ((private, cmd), tags) =>
    1.11 -        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) private @
    1.12 +      >> (fn ((cmd_mod, cmd), tags) =>
    1.13 +        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
    1.14            [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
    1.15              (Basic_Token cmd, (Latex.markup_false, d)))]));
    1.16