Hi Florian,
Between Isabelle 2014 and 2015, the option "open" appeared for the
command export_code, and by default the reflection minimizes the
exported code.
Would it be acceptable for code_reflect to also have a similar option
"open"?
As a draft example, here is a list of modifications needed for
implementing the option "open":
afp-devel/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_runtime.thy
We basically abstract the parameter "false" of Code_Target.produce_code,
and propagate this information to the parsing step.
Cheers,
Frédéric
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
