[isabelle-dev] fun : term -> string

Makarius makarius at sketis.net
Thu Sep 23 16:11:41 CEST 2010

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.)


More information about the isabelle-dev mailing list