[isabelle-dev] fun : term -> string

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Sep 23 12:12:45 CEST 2010

Hi Walther,

> we have hundreds of tests on very old code relying on a function
>    term2str = fn : term -> string, with: term2str @{term "str"} = "str"
> i.e., the string _without_ markup.
> My actual study of Isabelle code got stuck at 'structure Buffer' (via 'writeln') and at 'markup' --- where can I proceed ?

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"}

(The business with filter is there to respect the user's "xsymbols" preference. You probably don't need it.) 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. Also, you might get several spaces in a row, which you might want to simplify.

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. There might exist better solutions. I hope this helps nonetheless.



More information about the isabelle-dev mailing list