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" everytime in the corresponding >> "print_case" clause, and skip this optimization like in the SML part >> where "let"..."in"..."end" are inserted everytime, what about you? 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? >> In the same spirit, the following code does not compile after exporting >> to Scala: >> datatype n = N nat >> definition "b = (let _ = N in False)" >> This is because N is a function, and no parentheses are generated around >> functions (at least in this example). Abstractions in Scala are now always in parenthesis, but only once for abstraction chains. Thanks a lot again, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
