kframework/k — pull request #264 by Multiball (2014-03-04 02:53:01+00:00)
Title: Added many documentation comments; added a "nodoc" tag.

In this update, I have added comments for several builtin modules, listing them in include/builtins/k-reference.k . Kompile this file with the option --backend=doc to generate k-reference-doc.tex. The comments I have added are far from complete, and there are many sections labeled "TODO" that include some question about functionality that should be filled in by people more knowledgeable than I.

I have added a "nodoc" tag to indicate productions that should not be included in the documentation. This is used to hide productions that are essential to internal mechanics but are never used by end users, especially hooking rules.

The greatest difficulty I've encountered is attempting not to display output from modules not included in the original file (which, thusfar, has been k-reference.k). By recursively importing files, many modules are imported that do not include functionality of interest to the end user, and including them in the reference manual would be a mistake. However, determining which modules are imported from the main file and subsequently not producing or deleting latex output from modules imported from outside the main file has proven to be fairly difficult by the time the definition is passed through the BackendFilter. If anyone has any ideas about this, I would like to hear them.

There are some other things I would like to know:
-What are the available color options for configuration cells? As an end user, I've often wanted to have a complete list.
-Where are the functions of the family asValue()? Those are important to know about.
-How much do we want to say about things not directly included in .k files, like KResults and Configurations? Should talking about those be relegated to a piece of documentation separate from this "reference manual," or is it relevant enough to include?