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