polyml/basis/TopLevelPolyML.sml

48         type basicLoc = (* Locations in request packets. *) { startOffset: FixedInt.int, endOffset: FixedInt.int }
51         datatype request =
69                 of { request: int, requestId: string}
91                 of { request: int, requestId: string }
157                     (* Reads a request.  Calls OS.Process.exit at end-of-file or on a protocol error. *)
158                     fun readRequest (): request =
197                             let (* Compile request. *)
296                         |   #"K" => (* Cancel request. *)
318                                 UnknownRequest { request = Char.ord ch, requestId = "" }
467                         |   makeResponse (UnknownResponse { request, ... }) =
469                                 val startCh = Char.chr request
565                     (* Reads a request.  Calls OS.Process.exit at end-of-file or on a protocol error. *)
566                     fun readRequest (): request =
571                            Position the stream ready to read the next request. *)
604                             Application(3, _) => (* Compilation request. *)
622                                 |   (SOME requestId, _) => UnknownRequest { request = 3, requestId = requestId }
623                                 |   _ => UnknownRequest { request = 3, requestId = "" } (* Malformed *)
644                                 |   (SOME requestId, _, _, _) => UnknownRequest { request = 4, requestId = requestId }
645                                 |   _ => UnknownRequest { request = 4, requestId = "" } (* Malformed *)
648                         |   Application(5, _) => (* Move request. *)
678                                 |   (SOME requestId, _, _, _, _) => UnknownRequest { request = 5, requestId = requestId }
679                                 |   _ => UnknownRequest { request = 5, requestId = "" } (* Malformed *)
712                                 |   (SOME requestId, _, _, _, _) => UnknownRequest { request = 6, requestId = requestId }
713                                 |   _ => UnknownRequest { request = 6, requestId = "" } (* Malformed *)
734                                 |   (SOME requestId, _, _, _) => UnknownRequest { request = 7, requestId = requestId }
735                                 |   _ => UnknownRequest { request = 7, requestId = "" } (* Malformed *)
738                         |   Universal(tagNo, _) => UnknownRequest { request = tagNo, requestId = "" }
739                         |   Application(tagNo, _) => UnknownRequest { request = tagNo, requestId = "" }
740                         |   Context(tagNo, _) => UnknownRequest { request = tagNo, requestId = "" }
741                         |   Private(tagNo, _) => UnknownRequest { request = tagNo, requestId = "" }
756                         |   #"K" => (* Cancel request. *)