On 24/06/13 21:20, Makarius wrote: > Last week, I actually intended to make a proper exposition about > Isabelle/ML futures in the "implementation" manual, but for now it > just points to ~~/src/Pure/Concurrent/future.ML with its slightly odd > "Notes" at the beginning. That needs to be turned into proper text > outside the sources, as part of the manual.
As a single data-point: I personally find the "Notes" at the top of the file far more useful than out-of-line documentation. In particular, I never think to look in the implementation manual because only a very small percentage of the Isabelle sources are documented there. > (There is a conceptual problem with putting such explanations into the > sources, since they are built in bottom-up manner, but explanations > should be more top-down; this is also relevant for worked examples > that are actually run.) Again, users don't need a function-by-function running commentary of the sources, but just need to get a high-level idea of what is going on: I would claim that a description at the top of the file---and perhaps a few sentences on top of important functions---helps just as much as pages of carefully typeset prose. Further, the latter tends to require much more effort, meaning that often the choice boils down to either having quick-and-dirty notes in the source that exist, versus polished documentation outside the sources that doesn't. On this note, if you would like someone to go through and add documentation inline to the Isabelle sources, I would be willing to put my hand up to help out. (Assuming, of course, there was an interest in committing the patches, and a willing expert to review them.) Cheers, David ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
