Re: [isabelle] Isabelle2013-1-RC1 available for testing



Hi Cornelius,

The former "code_modulename Scala Theory Module" is now

code_identifer code_module Theory => (Scala) Module

You can now use code_identifier also with other kinds of code generator data. For example, the following moves a single constant foo to module M and renames it to bar:

code_identifier constant c => (Scala) "M.bar"

Best,
Andreas

On 07/10/13 17:28, C. Diekmann wrote:
Dear all,

I encountered the following when testing Isabelle2013-1-RC1.

When using code_modulename, the buffer displays a Warning:
"Legacy feature! prefer "code_identifier" over "code_modulename""
However, the warning is not visualized by jEdit (I expected a yellow
marking at the left border)

Say I have my mathematical definitions in X.thy and an executable
implementation in X_impl.thy. I used
code_modulename Scala X_impl X
to export the code in the module X, not X_impl. How do I translate
this using the suggested code_identifier?

On a German keyboard layout, the "Go to Recent Buffer" does (still) not work.

Cheers
   Cornelius





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