Hi Florian,
For SML, I kept everything as it is since
a) the code is separate from OCaml anyway
b) the "let … end" is always safe regardless of surrounding whitespace.
Or did I miss something here?
Here the SML part should be kept as it is (the generation was working
correctly for me in SML)
Hi Fréderic,
see now
http://isabelle.in.tum.de/repos/isabelle/rev/774752af4a1f
http://isabelle.in.tum.de/repos/isabelle/rev/8e736ce4c6f4
>> By comparing the generating code for SML and OCaml in
>> src/Tools/Code/code_ml.ML, I would be tempted to replace
>> "brackify_block" by "brackets" everytim
Hi Frédéric,
thanks for going into this so thoroughly.
I will look after these errors as soon possible.
In ancient days, there was a dedicated theory which contained such
»challenges« for the code generator, but with more and more theories
with code generation this had been given up; maybe these
Dear all,
The following is a list with 2 elements:
definition "l = [let x = True in x, False]"
However after doing "export_code l in OCaml", we obtain a list with only
1 element, because at the end no parentheses are inserted around the
corresponding "let".
In particular by default in OCaml [le
