[isabelle-dev] Explicit option "open" for code_reflect

[Frédéric Tuong]

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