[isabelle] debug parts of Pure
We want to understand details of AST translations.
After having studied §8.5. »Syntax transformations« in isar-ref und §3
»Concrete syntax and type-checking« in implementation we still had
questions. So we studied respective code (ast.ML, syntax_phases.ML, etc)
and got stuck again.
Would it be possible to re-compile respective code of Pure, such that we
can investigate it »Step«wise in the debugger ?
PS: »ML_file_debug "syntax_phases.ML"« etc seems impossible in the very
specific bootstrapping process. In the mail archive we did not find more
than the outdated »Toplevel.debug«.
This archive was generated by a fusion of
Pipermail (Mailman edition) and