[isabelle] Slots for diagnostic value command

In 4044a7d1720f, there was a change: the ancient »slots« for value
(code, nbe, simp) and the default behaviour of sequential trys have been
given up in favour of one hard-coded behaviour:
* If the term to evaluate does not contain free variables, evaluate
using ML.
* If the term contains free variables or the first step fails, evaluate
using nbe.

Recent experience suggests that this step was maybe too rigorous since
»value« is also used for purposes beyond diagnostic evaluation which
demand a more predictable behaviour, esp. wrt. ongoing developments of

My suggestion would be to revive the »slots« as follows:
* Slot »default« implementents the current behavior and is the default.
* The former slots (s.a.) are restored again.

Any comments?

This is something I definitely do not promote for the approaching
release, but rather for its successor.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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