Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <199405271155.AA20557@borneo.gmd.de>
To: info-hol@leopard.cs.byu.edu
From: Matthew Morley <morley@gmd.de>
Subject: Re: help files for hol90
In-Reply-To: Your message of "Thu, 26 May 94 17:34:00 EDT." <m0q6n4X-00005DC@tiree.research.att.com>
Date: Fri, 27 May 94 13:55:17 +0200


-Dear HOL community,

(recycled)

-Here to date
-the only volunteers for the job have been Steve Brackin, myself, and
-Konrad Slind.  

Not entirely correct, but let it pass.

Elsa's "reminder" seems not unwarranted, but I should like to make
the following observations:

    The HOL helpfiles display a laudable uniformity of style, so
    in translating these to reflect hol90's syntax one ought to
    avoid the temptation to tweak the text at all costs.

    Bear in  mind that the  .doc files are accessed by different
    help utilities, and in  particular neither the built-in help
    command nor  Xhelp, reformat the  text --  unlike the mosaic
    renderer -- so  some effort ought  to  be made  to leave the
    plain text  neatly formatted, say  to column  70. (Justified
    even, as it's trivial in emacs (say) to invoke C-u M-q.)

    Terms are  quoted like `Foo bar` in  in-line text, but often
    displayed  maths is intended  to simulate real hol input. In
    this case

      --`Foo bar`--

    seems more appropriate. Consistency in this is important, so
    the question is "What stylistic convention do we, humble
    translators, observe?"

    Does it not make sense to pre-process all the docs prior to
    individual translation to convert:
      'string' --> "string"
      "term"   --> `term`
    and similarly any other global translations? (Maybe this has
    been done by now, but it wasn't last time I looked.)

    Phil and collegues have put tremendous effort into the
    hypertext documentation, but the doc_to_html `script' is
    non-trivial -- some hand re-touching is inevitable. If there
    are some `adjustments' we can make to the docs that would
    minimise the need to hand-code the html versions, it'd be 
    useful to know in advance. Phil?

    Note that hol90 introduces record types, delimited by { - },
    but these have special meaning in the hol88 docs (akin to
    TeX grouping. So formatting types of functions involving
    record types needs special care (double up the brackets). 

M