Email Gateway (Aug 22 2022 at 18:10): Email Gateway (Aug 22 2022 at 18:10):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi,
In the following theory file,
theory Scratch imports Main begin
setup {* Thy_Header.add_keywords
[(("myname", Position.none), (("diag", []), []))] ; *}
ML {*
val _ =
Outer_Syntax.command \<^command_keyword>\<open>myname\<close> "print
myname"
(Scan.succeed (Toplevel.keep (fn _ => writeln "jeremy")));
*}
print_commands
print_commands
myname
end
the print_commands commands shows that the new command "myname" has been
added, but when we get to using it, it fails with a message like
command expected but identifier myname found
Why is this?
When I replace the use of Thy_Header.add_keywords with inserting
keyword myname :: "diag" in the theory file header it works OK
What is happening here?
Thanks
Jeremy
Email Gateway (Aug 22 2022 at 18:11):From: Thomas.Sewell@data61.csiro.au
My understanding is that the commands defined in this theory won't be
available until subsequent theories.
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 18:11):From: Lars Hupel <hupel@in.tum.de>
Dear Jeremy,
When I replace the use of Thy_Header.add_keywords with inserting
keyword myname :: "diag" in the theory file header it works OK
this is indeed the recommended way of adding new commands. It is
required so that Isabelle/jEdit (and other frontends) can statically
understand the outer command syntax of a theory.
Cheers
Lars
Email Gateway (Aug 22 2022 at 18:11):From: Makarius <makarius@sketis.net>
Even more it is mandatory to declare keywords statically.
Recall that the usual way to do things properly in Isabelle is to look
at representative examples, to see how people have done it successfully
before.
If all fails, there is also some documentation: "implementation" manual
section 9.1.2:
"""
The file 🗏‹~~/src/HOL/ex/Commands.thy› shows some example Isar command
definitions, with the all-important theory header declarations for outer
syntax keywords.
"""
Makarius
Email Gateway (Aug 22 2022 at 18:11):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Well, I haven't found any examples showing how to add a new command at
an arbitrary point in a theory file (the examples all add the required
keyword right at the start of the theory file)
Jeremy
Email Gateway (Aug 22 2022 at 18:12):From: Lars Hupel <hupel@in.tum.de>
That's because you should not add a new command at an arbitrary point,
but at the header. It's just not supported. Why do you want to do it
somewhere else?
Email Gateway (Aug 22 2022 at 18:12):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Well, I was thinking of the possibility that the need for a new command
might be discovered during the interactive development of a theory.
It's not clear at this point it would be needed, or couldn't be worked
around. But that's what I was trying to do, in trying to figure out how
to add a command.
Jeremy
Email Gateway (Aug 22 2022 at 18:12):From: Peter Lammich <lammich@in.tum.de>
On Di, 2018-08-07 at 18:19 +1000, Jeremy Dawson wrote:
On 07/08/18 16:41, Lars Hupel wrote:
Well, I haven't found any examples showing how to add a new
command at
an arbitrary point in a theory file (the examples all add the
required
keyword right at the start of the theory file)
That's because you should not add a new command at an arbitrary
point,
but at the header. It's just not supported. Why do you want to do
it
somewhere else?
Well, I was thinking of the possibility that the need for a new
command
might be discovered during the interactive development of a theory.It's not clear at this point it would be needed, or couldn't be
worked
around. But that's what I was trying to do, in trying to figure out
how
to add a command.
The need for new commands is usually rare enough that it is realistic
to go back to the header of the theory each time you discover its need,
and add a keyword there.
Email Gateway (Aug 22 2022 at 18:12):From: Makarius <makarius@sketis.net>
The 'keywords' are part of the theory header and have to be there on top
-- there is no way around it.
The actual command definition can be anywhere in the same theory, and
you can use the command right after defining it.
The example ~~/src/HOL/ex/Commands.thy demonstrates both aspects.
Makarius
Last updated: Apr 24 2024 at 04:17 UTC