[isabelle-dev] fun : term -> string

[Walther Neuper]

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 ?

Thanks for any help,
Walther

PS: Actually, our present work aims at getting rid of that kind of 
(partial) solution for term2str ...

ML {*
fun term2str trm = Syntax.string_of_term (ProofContext.init_global
                                               (theory "Isac")) trm;
val trm = @{term "a+b"};
term2str trm;
*}
val term2str = fn : term ->  string
val trm = Const (...) $ Free (...) $ Free (...) : term
val it =
    "\^E\^Fterm\^E\^E\^Fhilite\^E\^E\^Ffree\^Ea\^E\^F\^E\^E\^F\^E \^E\^Fconst\^Fname=Groups.plus_class.plus\^E+\^E\^F\^E \^E\^Fhilite\^E\^E\^Ffree\^Eb\^E\^F\^E\^E\^F\^E\^E\^F\^E"
    : string

... but the many updates from Isabelle2002 to Isabelle2009-2 broke the 
code in several crucial points. So we first want to revive the code 
again, and for that purpose we need the tests, many of them designed in 
a sequence of elementary to complex functionality.