Email Gateway (Aug 22 2022 at 17:36): Email Gateway (Aug 22 2022 at 17:36):From: Walther Neuper <wneuper@ist.tugraz.at>
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
Xxxxx.thy
Email Gateway (Aug 22 2022 at 17:37):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 25 2024 at 20:15 UTC