On Thu, 23 Sep 2010, Jasmin Christian Blanchette wrote:
I found a couple of ad hoc solutions to this problem. One way is to set
the print mode to "input":
Print_Mode.setmp (Print_Mode.input ::
filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
(Syntax.string_of_term ctxt) @{term "str"}
Note that the Print_Mode.input never has any effect on output, it is
filtered out from the print_mode_value. So there is no point of adding it
to the list.
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.
You might need to follow this with
String.translate (fn c => if Char.isPrint c then str c else "")
which I have in my code.
As explained in the Isabelle/Isar implementation manual, Isabelle/ML lacks
type char altogether -- the smallest textual unit is Symbol.symbol. Char
operations may only be used in rare circumstances involving external
tools, never for regular Isabelle text manipulation.
The other solution is to strip away the YXML tags, using the following function:
val unyxml = XML.content_of o YXML.parse_body
These are the solutions I found in those rare cases where I needed this.
This is better. The above form requires some more recent repositoy
version like 3810834690c4 (as usual there can be some non-monotonic
fluctioations on non-release versions of Isabelle.)
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
