[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 ?

Walther

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 MHonArc.