Andrea Vezzosi (May 24 2024 at 08:02): Andrea Vezzosi (May 24 2024 at 08:02):Hi, I am trying to catch errors thrown by e.g. Syntax.check_prop and manipulate the resulting string.
One problem is that the strings contain extra info delimited in some way by escape characters #"\^E" and #"\^F", is there a library function to give me the string stripped of that and/or as writeln would show it?
Andrea Vezzosi (May 24 2024 at 08:38):Figured it out: the markup I am seeing is encoding of a YXML tree, YXML.content_of gives me what I want.
Kevin Kappelmann (May 24 2024 at 11:29):Funnily enough, I was looking for exactly the same thing today, thanks! :happy: (tagging @Fabian Huch)
Andrea Vezzosi (May 24 2024 at 11:57):Glad I could help! Isabelle workings can be quite mysterious
Last updated: Dec 21 2024 at 16:20 UTC