[isabelle-dev] fun : term -> string

Walther Neuper wneuper at ist.tugraz.at
Thu Sep 23 10:54:51 CEST 2010

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,

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.

More information about the isabelle-dev mailing list