File: host_name.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (38 lines) | stat: -rw-r--r-- 990 bytes parent folder | download | duplicates (11)
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
\DOC host_name

\TYPE {host_name : (void -> string)}

\SYNOPSIS
Returns the name of the host machine.

\EXAMPLE
When the {HOL} system was being run on the host machine {scaup.cl.cam.ac.uk}:
{
   #host_name ();;
   `scaup.cl.cam.ac.uk` : string
}
\COMMENTS
This function uses the facilities provided by the underlying Lisp, which
unfortunately are extremely inconsistent. In Lisps other that Franz, this
function may not work at all. However, the ability to perform system commands
usually provides an adequate alternative, if one is prepared to put in a bit
more work. For example:
{
   #let host_name2() =
   #system `hostname >/tmp/.hostname`;
   #let handle = openi `/tmp/.hostname` in
   #letref name, char = ``, `` in
   #while not (char = `\
   #`) do (name := name^char; char := read handle);
   #close handle;
   #system `rm /tmp/.hostname`;
   #name;;
   host_name2 = - : (* -> string)

   #host_name();;
   `` : string

   #host_name2();;
   `auk.cl.cam.ac.uk` : string
}
\ENDDOC