History log of /seL4-l4v-master/HOL4/help/Docfiles/Lib.S.doc
Revision Date Author Comments
# bfdab2c8 08-Oct-2012 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Combinators A and B were removed from Lib by commit 6b16cc6 (in 2009).


# 5d22e4bb 10-Apr-2002 Michael Norrish <Michael.Norrish@nicta.com.au>

A variety of changes to the help system. ParseDoc now inserts its best
guess as to an identifier's structure into the data structure it returns.
This is done by adding a FIELD("STRUCTURE", [TEXT "foo"]) to the list
of sections. If there's one already present, this is respected, but
otherwise it looks at the filename, and if it's of the form str.id.doc,
then str is taken to be the structure name. This information is then
used in the ASCII and .tex presentations of the .doc file.
The change to the HTML generator is only to make it work the same as
it always did; it throws away extra "STRUCTURE" fields. (It had been
assuming that the second field would always be the \\TYPE field...
now that I think of it, this is reasonable, I will fix the parser not
to mess with this assumption.)
The LaTeX macros in ref-macros change to reflect the fact that there
is now slightly more stuff in the box that encloses an ML identifier.
I've also fixed the .tex generation so that nothing in a .doc file
need be quoted with \ characters because of its sensibilities. This
accounts for the changes to the Lib.[ABCIKSW].doc files. Lib.all2 was
looking very ugly when TeX'ed, so I've tried to make it prettier.


# a4c199c6 13-Dec-2001 Michael Norrish <Michael.Norrish@nicta.com.au>

Huge number of check-ins, implementing change to .doc file syntax.
Now the rule for text within braces is that it appears as given, but
that braces must balance. If you want an unbalanced brace, you can use
\lbrace or \rbrace. No existing .doc file uses unbalanced braces.
Also, there is now no need to use \noindent. In fact, doing so
will get you a complaint from the parser. Similarly, use of \ or
{} characters outside of verbatim text blocks will cause griping.
All of the new files have been generated by a parse-then-print process
from the old files, and it's possible there are errors. If you ever
have a spare moment, casting your eye over a random selection of these
might help to find errors.


# a57fb74a 26-Nov-2001 Michael Norrish <Michael.Norrish@nicta.com.au>

Fixed these entries so that they don't break the latex generation of the
manuals. The shell-script that does the collation of all the entries will
also need to be changed because it now puts things together in the wrong
order.


# ce793cee 23-Nov-2001 Konrad Slind <konrad.slind@gmail.com>

New versions of docfiles.