[isabelle-dev] fun : term -> string

[Makarius]

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