/usr/share/hol88-2.02.19940316/lisp/f-help.l is in hol88-source 2.02.19940316-28.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; HOL 88 Version 2.0 ;;;
;;; ;;;
;;; FILE NAME: f-help.l ;;;
;;; ;;;
;;; DESCRIPTION: On-line help system ;;;
;;; ;;;
;;; USES FILES: f-franz.l (or f-cl.l), f-macro.l ;;;
;;; ;;;
;;; University of Cambridge ;;;
;;; Hardware Verification Group ;;;
;;; Computer Laboratory ;;;
;;; New Museums Site ;;;
;;; Pembroke Street ;;;
;;; Cambridge CB2 3QG ;;;
;;; England ;;;
;;; ;;;
;;; COPYRIGHT: University of Edinburgh ;;;
;;; COPYRIGHT: University of Cambridge ;;;
;;; COPYRIGHT: INRIA ;;;
;;; ;;;
;;; REVISION HISTORY: (none) ;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eval-when (compile)
#+franz (include "lisp/f-franz")
(include "lisp/f-macro")
(special %search-path %help-search-path))
;;; Keyword facility deleted: should be replaced by a more sophisticated
;;; method of looking things up. [TFM 90.09.08]
;;;
;;; (dml |keyword| 1 ml-keyword (|string| -> |void|))
;;;
;;; (defun ml-keyword (tok)
;;; (let
;;; ((file (fileexists 'kwic "hol")))
;;; (if file
;;; (keyword-search tok file)
;;; (failwith "Could not find HOL keyword file"))))
;;; The variable %help-search-path is the search path for help information.
;;; It is set in Makefile.
;;; Added by MJCG on 7 Dec 1989
;;; Revised by TFM 90.12.01 (made available in ML)
;;; Initialized to nil
(setq %help-search-path nil)
;;; TFM 90.12.01 for version 1.12
;;; dml-ed function to return the help search path
(defun ml-help_search_path () %help-search-path)
(dml |help_search_path| 0 ml-help_search_path (|void| -> (|string| |list|)))
;;; TFM 90.12.01 HOL88 version 12
;;; dml-ed function for setting the help search path from ML
(defun ml-set_help_search_path (new-path)
(progn %help-search-path (setq %help-search-path new-path) nil))
(dml |set_help_search_path| 1 ml-set_help_search_path
((|string| |list|) -> |void|))
;;; %help-search-path now set in Makefile. (note %hol-dir no longer used)
;;; (defun set-help-search-path ()
;;; (setq
;;; %help-search-path
;;; (list (concat %hol-dir '|/help/Reference/RULES/|)
;;; (concat %hol-dir '|/help/Reference/TACTICS/|)
;;; (concat %hol-dir '|/help/Reference/GENFNS/|)
;;; (concat %hol-dir '|/help/Reference/LOGFNS/|)
;;; (concat %hol-dir '|/help/Reference/LIBRARIES/|))))
(dml |help| 1 ml-help (|string| -> |void|))
;;; Help system changed to search %help-search-path.
;;; .doc files are looked for first and if found processed
;;; with the sed script help/Reference/doc-to-help.sed.
;;; If no .doc file is found then a .jac file is searched for
;;; and if found processed with help/Reference/jac-to-help.sed
;;; MJCG 7 December 1989
;;; Old code:
;;; (defun ml-help (tok)
;;; (let
;;; ((file (fileexists 'help tok)))
;;; (if file
;;; (display-file file)
;;; (msg-failwith "help" "No information available on " tok))))
;;; Chaneged to allow for alias for whacky help files (eg '/.doc') by using an
;;; association list. [JVT 17 March 1991].
;;; .hat association list entry added [TFM 17.03.91]
(defun ml-help (tok)
(let ((%search-path %help-search-path)
(isothername (assoc tok '((|/| |.div|)(|^| |.hat|)))))
(let ((realname (if (null isothername) tok (cadr isothername))))
(let ((doc-file (fileexists 'doc realname)))
(if doc-file
(display-file doc-file '|doc|)
(let ((jac-file (fileexists 'jac realname)))
(if jac-file
(display-file jac-file '|jac|)
(msg-failwith
"help"
"No information available on " tok))))))))
|