1structure Help :> Help = struct
2
3(* Help -- a simple Moscow ML library browser, PS 1995-04-30, 2000-04-22
4
5Invoking `help s' has the following effect:
6
7 (a) s is normalized to lower case
8 (b) if s is the empty string, then the help browser is invoked with the
9     message !welcome;
10 (c) otherwise, if the term s appears in !specialfiles, then the browser
11     is invoked with the file associated with s;
12 (d) otherwise, if the term appears in one of the index files in
13     !indexfiles, then the help system asks the user to choose which
14     help file to load, in case there are several, and invokes the
15     browser with that file;
16 (e) otherwise, a standard error message is shown.
17
18The help system looks for help files in the -stdlib and in the
19directories in !helpdirs.
20
21The browser can open a file on a specified line, attempting to center
22that lines in the display (assuming the display can hold !displayLines
23lines at a time).
24
25The browser accepts several commands for moving forth and back in the
26current file.
27
28The browser's search facility cyclically searches (case-insensitive)
29for occurrences of a given string and displays the line in which the
30string was found, as close to the center of the display (or portion
31displayed) as possible.
32
33Several hacks are being used to avoid loading too many other libraries
34along with Help.
35*)
36
37(* The number of lines to show interactively: *)
38
39val displayLines = ref 24
40
41(* Additional directories to search for help files *)
42
43val helpdirs = ref [] : string list ref
44
45
46
47
48val slash = #"/"
49
50
51fun joinDirFile dir file =
52    let open String
53    in
54	if dir <> "" andalso sub(dir, size dir - 1) = slash then
55	    dir ^ file
56	else
57	    dir ^ str slash ^ file
58    end
59
60(* Find the standard library directory: *)
61(*
62fun getstdlib () =
63    let open Vector
64	prim_val argv_ : string vector = 0 "command_line";
65	val stop = length argv_ - 1;
66	fun h i =
67	    if i < stop then
68		if sub(argv_, i) = "-stdlib" then sub(argv_, i+1)
69		else h (i+1)
70	    else
71		raise Fail "Cannot find the standard libraries!"
72    in h 0 end;
73    *)
74
75(* Full path of the signature index database: *)
76
77val indexfiles = ref [(*joinDirFile (getstdlib ()) "helpsigs.val"*)]
78
79(* Mapping particular search terms to non-.sig files: *)
80
81val specialfiles = ref [{term="lib", file="README", title="Overview"}];
82
83(* The help system's response to help "" : *)
84val welcome =
85    ref (Vector.fromList ["HOL ML library browser: \n",
86	  "\n",
87	  "   help \"lib\";   gives an overview of the library units\n",
88	  "   help \"id\";    provides help on identifier id\n",
89	  "\n"])
90
91local
92fun print s = TextIO.print s
93
94(* Auxiliaries: *)
95
96fun min (x, y) = if x < y then x else y : int;
97fun max (x, y) = if x < y then y else x : int;
98
99fun normalize []           = []
100  | normalize (#"\n" :: _) = []
101  | normalize (c :: cr)    = Char.toLower c :: normalize cr
102
103fun toLower s = String.implode (normalize (String.explode s))
104
105(* The signature browser: *)
106
107fun show name centerline initiallySought (strs : string Vector.vector) =
108    let
109	val lines = Vector.length strs
110	val sought = ref initiallySought
111	fun instr s str =
112	    let val len = String.size s
113		fun eq j k =
114		    j >= len orelse
115		    String.sub (s, j) = Char.toLower (String.sub (str, k)) andalso eq (j+1) (k+1)
116		val stop = String.size str - len
117		fun cmp k = k<=stop andalso (eq 0 k orelse cmp(k+1))
118	    in cmp 0 end;
119	fun occurshere str =
120	    case !sought of
121		NONE   => false
122	      | SOME s => instr s str
123	fun findline s curr =
124	    let fun h i =
125		if i >= lines then NONE
126		else if instr s (Vector.sub(strs, (i+curr) mod lines)) then
127		    SOME ((i + curr) mod lines)
128		else h(i+1)
129	    in h 0 end
130	val portion = max(!displayLines, 5) - 1
131	fun wait next =
132	    let val prompt =
133		"---- " ^ name ^ "[" ^
134		Int.toString((100 * next) div lines)
135		^ "%]: down, up, bottom, top, /(find), next, quit: "
136		fun toend () = (print "\n....\n";
137				nextpart (lines - portion) portion)
138		fun tobeg () = (print "\n....\n"; nextpart 0 portion)
139		fun up   ()  = (print "\n....\n";
140				nextpart (next-3*portion div 2) portion)
141		fun down ()  = if next=lines then toend()
142			       else nextpart next (portion div 2)
143		fun find s =
144		    case findline s next of
145			NONE      =>
146			    (print ("**** String \"" ^ s ^ "\" not found\n");
147			     wait next)
148		      | SOME line =>
149			    (print "\n....\n";
150			     nextpart (line - portion div 2) portion)
151		fun search chars =
152		    let val s = String.implode (normalize chars)
153		    in sought := SOME s; find s end
154		fun findnext () =
155		    (case !sought of
156			 NONE   => (print "**** No previous search string\n";
157				    wait next)
158		       | SOME s => find s)
159	    in
160		print prompt;
161		case Option.map String.explode (TextIO.inputLine TextIO.stdIn) of
162                    NONE => ()
163		  | SOME (#"q" :: _) => ()
164		  | SOME (#"u" :: _) => up ()
165		  | SOME (#"d" :: _) => down ()
166		  | SOME (#"t" :: _) => tobeg ()
167		  | SOME (#"g" :: _) => tobeg ()
168		  | SOME (#"b" :: _) => toend ()
169		  | SOME (#"G" :: _) => toend ()
170                  | SOME (#"/" :: s) => search s
171                  | SOME (#"n" :: s) => findnext ()
172		  | _         => if next=lines then toend ()
173				 else nextpart next portion
174	    end
175	and nextpart first amount =
176	    let val start = max(0, min(lines - amount + 1, first))
177		val stop  = min(start + amount, lines)
178	    in prt wait start stop end
179	and prt wait i stop =
180	    if i >= stop then wait i
181	    else
182		let val line = Vector.sub(strs, i)
183		in
184		    if occurshere line then print "@>" else print "+ ";
185		    print line;
186		    prt wait (i+1) stop
187		end
188    in
189	print "\n";
190	if lines <= portion then prt ignore 0 lines
191	else nextpart (centerline - portion div 2) portion
192    end
193
194(* Read a signature file from the standard library: *)
195
196fun readfile file =
197    let fun openFile [] =
198	    raise Fail ("Help.readFile: help file `" ^ file ^ "' not found")
199	  | openFile (dir1 :: dirr) =
200		(TextIO.openIn (joinDirFile dir1 file))
201		handle IO.Io _ => openFile dirr
202	val is = openFile ((*getstdlib () :: *)!helpdirs)
203	fun h () = case TextIO.inputLine is of
204                       NONE => []
205                     | SOME s => s :: h ()
206    in Vector.fromList (h ()) end;
207
208(* Invoke the browser on a particular line of a signature: *)
209local
210open Database
211in
212fun showFile sought entry =
213    (case entry of
214	 {comp = Str, file, ...} =>
215	     show file 0 NONE (readfile (file ^ ".sig"))
216       | {comp = Term _, file, line} =>
217	     show file line NONE (readfile file)
218       | {comp, file, line} =>
219	     show file line (SOME sought) (readfile (file ^ ".sig")))
220    handle OS.SysErr _ => raise Fail "Help.showFile: inconsistent help database"
221end
222
223(* Let the user select from the menu: *)
224
225fun choose sought entries =
226    let val _ = print "\nChoose number to browse, or quit: "
227	val response =
228          case TextIO.inputLine TextIO.stdIn of
229               NONE => ""
230             | SOME s => s
231    in
232	case Int.fromString response of
233	    NONE => (case String.explode response of
234			  []        => ()
235	                | [#"\n"]   => ()
236			| #"Q" :: _ => ()
237			| #"q" :: _ => ()
238			| _         => choose sought entries)
239	  | SOME choice =>
240		if choice = 0 then ()
241		else showFile sought (List.nth(entries, choice - 1))
242    end
243    handle Subscript => choose sought entries
244	 | Overflow  => choose sought entries;
245
246(* Display the menu of identifiers matching the given one, or
247 * invoke the browser directly if these is only one match:
248 *)
249
250fun display sought []                  = raise Fail "Help.display"
251  | display sought [entry]             = showFile sought entry
252  | display sought (entries as e0::er) =
253    let open Database
254        fun render (entry as {comp, file, ...}) =
255	    case comp of
256		Str    => "structure " ^ file
257	      | Exc id => "exn  " ^ file ^ "." ^ id
258	      | Typ id => "type " ^ file ^ "." ^ id
259	      | Val id => "val  " ^ file ^ "." ^ id
260	      | Con id => "con  " ^ file ^ "." ^ id
261	      | Term (id, NONE)      => id ^ " (" ^ file ^ ")"
262	      | Term (id, SOME kind) => kind ^ " " ^ id ^ " (" ^ file ^ ")"
263	fun maxlen []         max = max
264	  | maxlen (e1 :: er) max =
265	    let val len = size (render e1)
266	    in maxlen er (if len > max then len else max) end
267	val maxwidth = maxlen er (size (render e0))
268	val boxwidth = 6 + 3 + 3 + maxwidth + 2
269	val horizontal = StringCvt.padRight #"-" boxwidth "    " ^ "\n"
270
271	fun prline lin [] = ()
272	  | prline lin (e1 :: rest) =
273	    (print "    | ";
274	     print (StringCvt.padLeft #" " 3 (Int.toString lin));
275	     print " | ";
276	     print (StringCvt.padRight #" " maxwidth (render e1));
277	     print " |\n";
278	     prline (lin+1) rest)
279    in
280	print "\n";
281	print horizontal;
282	prline 1 entries;
283	print horizontal;
284	choose sought entries
285    end
286
287in
288
289(* Main help function: search for a string in the signature index database: *)
290
291fun defaultBrowser ""    = show "help"     0 NONE (!welcome)
292  | defaultBrowser "lib" = show "Overview" 0 NONE (readfile "README")
293  | defaultBrowser id    =
294    let fun getdb filename =
295	    (Database.readbase filename)
296	    handle OS.SysErr _ => raise Fail "Cannot read help database!"
297	val sought = toLower id
298	fun lookone(dbn, res) = Database.lookup(getdb dbn, sought) :: res
299	fun tryspecial [] =
300	    (case List.concat(List.foldl lookone [] (!indexfiles)) of
301		 [] =>
302		     print ("\nSorry, no help on identifier `" ^ id ^ "'\n\n")
303	       | entries  => display sought entries)
304	  | tryspecial ({term, file, title} :: rest) =
305	    if term = sought then show title 0 NONE (readfile file)
306	    else tryspecial rest
307    in
308	tryspecial (!specialfiles)
309    end
310val browser = ref defaultBrowser
311
312fun help s = !browser s
313
314end
315end
316