[isabelle] defining keywords



Playing with Isabelle's parsers I would like to define new keywords.

My definition of keywords, however, is not accessible within ML blocks
as expected:

    theory Xxxxx imports Pure

    keywords "yyyyy" :: prf_open
    begin

    ML \<open>
      @{keyword "("} : string parser; (* this works as expected *)

      val _ =
        Outer_Syntax.command @{command_keyword yyyyy} "dummy definition
yyyyy"
          (Scan.succeed (Toplevel.proof Proof.begin_block));

      @{keyword "yyyyy"};                 (*ERROR Bad outer syntax
keyword "yyyyy"*)
    \<close>
    end

What I'm doing wrong ?

Thanks in advance, Walther
theory Xxxxx imports Pure

keywords "yyyyy" :: prf_open
begin

ML \<open>
  @{keyword "("} : string parser; (* this works as expected *)

  val _ =
    Outer_Syntax.command @{command_keyword yyyyy} "dummy definition yyyyy"
      (Scan.succeed (Toplevel.proof Proof.begin_block));

  @{keyword "yyyyy"};             (*ERROR Bad outer syntax keyword "yyyyy"*)
\<close>
end 


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.