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



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.