src/Pure/Isar/outer_syntax.ML
changeset 48768 abc45de5bb22
parent 48749 c197b3c3e7fa
child 48771 2ea997196d04
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Aug 11 17:23:09 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 11 17:24:21 2012 +0200
     1.3 @@ -284,12 +284,12 @@
     1.4          let val name = Token.content_of tok in
     1.5            (case commands name of
     1.6              NONE => []
     1.7 -          | SOME cmd => [(Token.position_of tok, command_markup false (name, cmd))])
     1.8 +          | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
     1.9          end
    1.10        else [];
    1.11  
    1.12      val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
    1.13 -    val _ = Position.reports (token_reports @ maps command_reports toks);
    1.14 +    val _ = Position.reports_text (token_reports @ maps command_reports toks);
    1.15    in
    1.16      if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
    1.17      else