[isabelle-dev] fun : term -> string

[Jasmin Christian Blanchette]

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.

Regards,

Jasmin