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