Re: [isabelle] defining "minor keywords"

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"
> 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,

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