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