On Thu, 23 Sep 2010, Jasmin Christian Blanchette wrote:
The business with filter is there to respect the user's "xsymbols"
preference. You probably don't need it.
There might be more user preferences that are getting lost here.
Under normal circumstances the default print mode should not be
filtered.
But something has to be filtered away, otherwise one gets YXML.
For the record: What I'm trying to do is to take a nameless fact and
produce a `foo` string out of it, hoping that this might work (and if it
doesn't, hoping the user is smart enough to find out which fact
Sledgehammer was trying to refer to and repair or name it).
Yes this is difficult in general. It is an instance of the "syntax
round-trip problem": a term should be printed in a way such that the
system agrees on it after reading it again.
I would say it is OK to print with only the "xsymbols" mode left and hope
for the best.
You can also try some explicit checks with Syntax.read_prop on the result,
but this is not bullet proof. (In HOL-Import Sebastian Skalberg had a load
of workarounds to approximate a full round trip, but this is not
necessarily for end-user consumption, only for the system reading slightly
odd generated theories again.)
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
