[isabelle] Code Generation: Error Messages



Florian,

Thanks for your recent replies!  I have one more observation regarding
the "No code equations for ..." error messages that export_code may
produce -- namely that they can be tedious to hunt down.  Getting

  *** No code equations for All
  *** At command "export_code".

when trying to export code for some top-level constant that depends on
All only through a lengthy chain of dependencies is helpful, but not
really great.

Ideally, I'd like to be able to click on the error message to go to the
corresponding source location. :-)   Failing this, a textual
representation of the dependency chain would be nice: e.g.,

  *** No code equations for All (required by Foo via Bar via Baz)
  *** At command "export_code".

Tjark






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