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.
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
