[isabelle] installing an Isar command

[Jeremy Dawson]

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

[T***@data61.csiro.au]

My understanding is that the commands defined in this theory won't be
available until subsequent theories.

Cheers,
    Thomas.

Post by Jeremy Dawson
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

[Lars Hupel]

Dear Jeremy,

Post by Jeremy Dawson
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

[Makarius]

Post by Lars Hupel
Dear Jeremy,

Post by Jeremy Dawson
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.

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

[Jeremy Dawson]

Post by Makarius

Post by Lars Hupel
Dear Jeremy,

Post by Jeremy Dawson
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.

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

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

[Lars Hupel]

Post by Jeremy Dawson
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?

[Jeremy Dawson]

Post by Lars Hupel

Post by Jeremy Dawson
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.

Jeremy

[Peter Lammich]

Post by Jeremy Dawson

Post by Lars Hupel

Post by Jeremy Dawson
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.

--
  Peter

Post by Jeremy Dawson
Jeremy

[Makarius]

Post by Jeremy Dawson
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)

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