Lines Matching defs:file
157 (* Reads a request. Calls OS.Process.exit at end-of-file or on a protocol error. *)
168 NONE => protocolError "End of file"
177 | NONE => protocolError "End of file"
192 NONE => protocolError "End of file"
308 NONE => protocolError "End of file"
315 | NONE => protocolError "End of file"
344 and printFullLocation { file, startLine, startPosition, endPosition, ...} =
346 print file; (* TODO double any escapes. *) printEsc #",";
565 (* Reads a request. Calls OS.Process.exit at end-of-file or on a protocol error. *)
772 fun encodeFullLocation { file, startLine, startPosition, endPosition, ...} =
775 if file = "" then [] else encodeItem(Context(1, Primitive), [encodeString file])
967 (({ file, startLine, startPosition, ... }, _),
970 file=file, startLine=startLine,
991 val { file, startLine, startPosition, ... } = loc
993 { file = file, startLine = startLine, endLine = startLine,
1604 (* The next argument is the file name. Open it but skip
1608 | getFileName [] = (print "Missing file name after --script\n"; OS.Process.exit OS.Process.failure)
1681 print("Error trying to use the file: '" ^ filenameArg ^ "'\n");