Hi Jasmin,
following your hint this works fine:
fun term2str trm = Print_Mode.setmp (Print_Mode.input ::
filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
(Syntax.string_of_term @{context}) trm;
Thank you very much,
Walther
On 09/23/2010 12:12 PM, Jasmin Christian Blanchette wrote:
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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
