NameDateSize

..25-Jul-20196

Asynt.smlH A D25-Jul-20192.1 KiB

Database.sigH A D25-Jul-20191 KiB

Database.smlH A D25-Jul-20196 KiB

Doc2Html.smlH A D25-Jul-20197.6 KiB

Doc2Tex.smlH A D08-Sep-20207.6 KiB

Doc2Txt.smlH A D25-Jul-20195.5 KiB

DOTH A D25-Jul-20197.4 KiB

Flash.sigH A D25-Jul-2019100

Flash.smlH A D25-Jul-2019584

HolmakefileH A D25-Jul-20192.5 KiB

HOLPage.smlH A D25-Jul-20194.3 KiB

Htmlsigs.sigH A D25-Jul-2019362

Htmlsigs.smlH A D25-Jul-201914.6 KiB

index.htmlH A D25-Jul-201911.3 KiB

Keepers.smlH A D01-Feb-2020388

Lexer.lexH A D25-Jul-20197.5 KiB

makebase.smlH A D25-Jul-20199.8 KiB

MyDatabase-sig.smlH A D25-Jul-20191 KiB

MyDatabase.smlH A D25-Jul-20193 KiB

MySML90.smlH A D25-Jul-201964

MyWord32.smlH A D25-Jul-201924

ParseDoc.sigH A D25-Jul-20191.2 KiB

ParseDoc.smlH A D25-Jul-201911.7 KiB

Parser.grmH A D25-Jul-201911 KiB

Parsspec.smlH A D25-Jul-20193.8 KiB

poly-Doc2Html.MLH A D25-Jul-2019629

poly-Doc2Tex.MLH A D25-Jul-2019901

poly-Doc2Txt.MLH A D25-Jul-2019628

poly-makebase.MLH A D25-Jul-20191.2 KiB

Printbase.smlH A D25-Jul-20192.5 KiB

READMEH A D25-Jul-20192.6 KiB

runDoc2Html.smlH A D25-Jul-201924

runDoc2Tex.smlH A D25-Jul-201923

runDoc2Txt.smlH A D25-Jul-201923

runmakebase.smlH A D25-Jul-201924

Symbolic.sigH A D25-Jul-201993

Symbolic.smlH A D25-Jul-20191.4 KiB

unCRH A D25-Jul-20192.3 KiB

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