[isabelle] Nested locales


I am trying to achieve the following syntactic structure:

mainlocale Test =
  fixes x::nat
  mylocale AA =
    fixes y::nat
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 #>

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

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