Email Gateway (Aug 22 2022 at 16:54): Email Gateway (Aug 22 2022 at 16:54):From: Viorel Preoteasa <viorel.preoteasa@gmail.com>
Hello,
I am trying to achieve the following syntactic structure:
mainlocale Test =
fixes x::nat
begin
...
mylocale AA =
fixes y::nat
begin
...
end_mylocale
...
end_ mainlocale
mainlocale declaration should behave the same as a locale declaration
mylocale declaration should end mainlocale and then it should behave like
a locale declaration
end_mylocale should end mylocale and it should open the context of the
mainlocale Test.
end_ mainlocale should end the context of mainlocale Test.
I tried to add the following syntax for mylocale:
val End = (Toplevel.exit o Toplevel.end_local_theory o
Toplevel.close_target o
Toplevel.end_proof (K Proof.end_notepad));
fun begin_mylocale begin f = Toplevel.begin_local_theory begin f o End;
val _ =
Outer_Syntax.command @{command_keyword mylocale} "define named
specification context"
(Parse.binding --
Scan.optional (@{keyword =} |-- Parse.!!! locale_val) (([], []), [])
-- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
begin_mylocale begin
(Expression.add_locale_cmd name Binding.empty expr elems #>
snd)));
where End is what seems to be done by the end keyword.
However, this does not work. End seems to do more than just closing the
previous mainlocale declaration.
Additionally, if possible, I would also like to have "end" keyword instead
of end_mylocale and
end_ mainlocale.
Best regards,
Viorel Preoteasa
Last updated: Nov 21 2024 at 12:39 UTC