Re: [isabelle] Proof_Context abstraction



> Since you mention type-driven: Do you know of a way of having the
> system tell me the types of non-exported functions in existing ML
> code in Pure/? The exported functions have their types visible in the
> signature specification.

This is going to sound very low-tech, but I usually copy-paste
significant chunks or even a whole file into a "ML{* *}" block in a
theory. This usually works fine and gives you the full markup.

> And for code in my own modules Ctrl-Hover is very helpful, but that
> doesn’t work in ML files that have been loaded in the heap. Is there
> maybe a way to get jEdit process Pure (instead of loading a Heap)?

As far as I know, that is only possible for theories loaded *after* Pure
has been bootstrapped. You're probably out of luck there.

Cheeers
Lars




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