Re: [isabelle] defining keywords



On 15/06/18 10:09, Walther Neuper wrote:
> 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 

The @{keyword} antiquotation refers to "minor keywords", but "yyyyy"
above is a "major keyword" for commands, see also Keyword.is_keyword vs.
Keyword.is_command.

Isar command parsers will never see command keywords in their input
stream, because command spans are managed by the system: the next
command keyword starts a new span.

See also my recent paper about "Isabelle/jEdit as Formal IDE"
https://sketis.net/wp-content/uploads/2018/05/isabelle-jedit-fide2018.pdf
on page 4 about "Commands":

"""
Any command is free to define its own concrete syntax, within the token
language of outer syntax of Isabelle theories, but excluding the
keywords of other commands.
"""


	Makarius




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