Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] defining "minor keywords"

Email Gateway (Aug 22 2022 at 17:23):

From: Makarius <makarius@sketis.net>
The 'keywords' declaration works for both kinds of keywords: "keywords
foo" declares a minor keyword, "keywords bar :: kind" declares a major
(command) keyword.

Makarius

Email Gateway (Aug 22 2022 at 17:37):

From: Walther Neuper <wneuper@ist.tugraz.at>
On 2018-06-15 16:36, Makarius wrote:

On 15/06/18 10:09, Walther Neuper wrote:

theory Xxxxx imports Pure

keywords "yyyyy" :: prf_open
begin

ML \<open>
@{keyword "where"} : string parser; (* this works as expected *)
@{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.
Reading structure Keyword and Pure.thy I conclude, that all keywords
declared in Pure.thy remain "minor keywords" ("keywords" as seen by
print_commands) unless they are explicitly made "commands" (as seen by
print_commands) by "Outer_Syntax.command" and colleagues.

And I found no further way, to declare a "minor keyword" within
Isabelle's user space, neither in the code nor in isar-ref.pdf.

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.
Ah, now I understand another aspect of parsing (isar-ref.pdf: "Major
keywords and minor keywords are guaranteed to be disjoint. This helps
user-interfaces to determine the overall structure of a theory text.."),
thank you: "minor keywords" are found within the span of a "command"
(but I couldn't find respective code, e.g. for command "spark_vc" and
enclosed keywords "from", "with", "by" etc).
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":
Thank you very much for this most recent paper, very illuminating !!!
"""
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.
... while "minor keywords" like "from", "with", "by" etc are not
excluded, right?
In isar-ref.pdf §3.2 I read

"Both minor keywords and major keywords of the Isar command language
    need to be specified, ..."

... but I find no hint how to specify minor keywords. Can this be done
? If yes, how?

Any hint is highly appreciated,
Walther

Last updated: Apr 26 2024 at 16:20 UTC