README
1This directory contains various programs used to generate help
2facilities of various kinds for the HOL system. We have adapted (in an
3extremely ugly way) some code used to generate help files for
4MoscowML. The notice from that code is appended.
5
6Currently, we do the following:
7
8 0. Translate all files in help/Docfiles into a database usable by
9 invoking "help" interactively.
10
11 1. Translate all files in help/Docfiles into HTML versions
12 (via Doc2Html).
13
14 2. Translate all signature files found in <holdir>/sigobj into
15 HTML versions. Links for all value bindings are resolved to
16 the results of (1), if possible. Theory signatures are internally
17 linked to provide efficient access. A signature file contains a
18 link to its source.
19
20 3. Generate an index of all HOL identifiers, with links to the
21 documentation, and the host signature.
22
23 4. Generate a HOLPage which brings all the above together on one
24 sheet.
25
26To add documentation, one simply adds the ".doc" format files into
27the directory help/Docfiles. Each file must have the format
28
29 <structure-name>.<id>.doc or
30 <structure-name>.doc
31
32If <id> is a symbolic identifier (not alphanumeric) then an alphanumeric
33name <alpha> has to be invented for it. Thus the file name will be
34<structure-name>.<alpha>.doc. The structure "Symbolic" must then be
35augmented as well, in order that the system can do the proper
36translations between <id> and <alpha>. See
37
38 help/Docfiles/Parse.minus2.doc
39
40for an example, noting well how alphanumeric variants are *not* used in
41the SEEALSO field.
42
43%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
44File mosml/src/doc/helpsigs/README
45
46This directory contains the program used to create the database used
47by the Moscow ML `help' function. It will not work under MS DOS
48because of the filename name truncation in DOS.
49
50The program illustrates the use of several libraries.
51
52The main program is makebase. It reads the signatures in directory
53mosml/lib/ and creates
54
55 * a help database in helpsigs.val
56 * an ASCII format version of the database in index.txt
57 * a LaTeX format version of the database in ../index.tex
58 * HTML versions of the signature files, and an identifier index,
59 with hyperlinks, in directory htmlsigs
60 * a LaTeX format version of the signature files, with layout and
61 \index{...} markup, in file ../texsigsigs.tex
62
63To create the main program, type
64
65 make
66
67To run the program thus compiled, type
68
69 makebase
70
71The program handles only signatures for (old) Moscow ML structure-mode
72unit interfaces, as used in the Moscow ML library.
73
74
75sestoft@dina.kvl.dk 1996-04-10, 2000-06-28
76