Enzo Zuanazi Bestetti (Dec 08 2025 at 13:45): Enzo Zuanazi Bestetti (Dec 08 2025 at 13:45):Hello everyone!
My name is Enzo, I am a computer science student at King's College London. I am taking a project to systematically test PolyML in the context of its use in Isabelle. My idea requires some knowledge about the tokens produced by the PolyML lexer, and as such I am in need of a way to obtain those.
Has anyone ever attempted this (and succeeded), or has anyone got any ideas which might help me?
Thank you so much!
irvin (Dec 09 2025 at 03:21):I think what you want is Isabelle's lexer since isabelle doesn't really use polyml's lexer
irvin (Dec 09 2025 at 03:22):see src/Pure/ML/ml_lex.ML for the lexer
irvin (Dec 09 2025 at 03:28):You can probably run lex tokens using the ML_Context.eval function
irvin (Dec 09 2025 at 03:29):assuming you're want to run code in the context/namespace of isabelle/ML
Last updated: Dec 28 2025 at 12:45 UTC