Re: [isabelle] Isabelle2013-1-RC1 available for testing
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"
On 07/10/13 17:28, C. Diekmann wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and