@@ -94,13 +94,13 @@ class WebSocketComm {
9494 // Provide logging to help track down errors.
9595 this . ws . onerror = ( event : any ) => {
9696 report_error (
97- `CodeChat Client: websocket error ${ JSON . stringify ( event ) } .` ,
97+ `CodeChat Client: websocket error ${ JSON . stringify ( event ) } .`
9898 ) ;
9999 } ;
100100
101101 this . ws . onclose = ( event : any ) => {
102102 console_log (
103- `CodeChat Client: websocket closed by event type ${ event . type } : ${ event . detail } . This should only happen on shutdown.` ,
103+ `CodeChat Client: websocket closed by event type ${ event . type } : ${ event . detail } . This should only happen on shutdown.`
104104 ) ;
105105 } ;
106106
@@ -111,7 +111,9 @@ class WebSocketComm {
111111 const joint_message = JSON . parse ( event . data ) as EditorMessage ;
112112 const { id : id , message : message } = joint_message ;
113113 console_log (
114- `Received data id = ${ id } , message = ${ JSON . stringify ( message ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } ` ,
114+ `Received data id = ${ id } , message = ${ JSON . stringify (
115+ message
116+ ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } `
115117 ) ;
116118 assert ( id !== undefined ) ;
117119 assert ( message !== undefined ) ;
@@ -145,19 +147,22 @@ class WebSocketComm {
145147 root_iframe ! . onload = ( ) => {
146148 set_content (
147149 contents ,
148- current_update . cursor_position ,
150+ current_update . cursor_position
149151 ) ;
150152 this . onloading = false ;
151153 } ;
152154 } else {
153155 set_content (
154156 contents ,
155- current_update . cursor_position ,
157+ current_update . cursor_position
156158 ) ;
157159 }
158160 } else if ( cursor_position !== undefined ) {
159- root_iframe ! . contentWindow ! . CodeChatEditor . scroll_to_line (
160- cursor_position ,
161+ // We might receive a message while the Client is
162+ // reloading; during this period, `scroll_to_line` isn't
163+ // defined.
164+ root_iframe ! . contentWindow ! . CodeChatEditor . scroll_to_line ?.(
165+ cursor_position
161166 ) ;
162167 }
163168
@@ -216,13 +221,15 @@ class WebSocketComm {
216221 const result_contents = value as MessageResult ;
217222 if ( "Err" in result_contents ) {
218223 report_error (
219- `Error in message ${ id } : ${ result_contents . Err } .` ,
224+ `Error in message ${ id } : ${ result_contents . Err } .`
220225 ) ;
221226 }
222227 break ;
223228
224229 default :
225- const msg = `Received unhandled message ${ key } (${ JSON . stringify ( value ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } )` ;
230+ const msg = `Received unhandled message ${ key } (${ JSON . stringify (
231+ value
232+ ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } )`;
226233 report_error ( msg ) ;
227234 this . send_result ( id , msg ) ;
228235 break ;
@@ -254,7 +261,7 @@ class WebSocketComm {
254261 // Send a message expecting a result to the server.
255262 send_message = (
256263 message : EditorMessageContents ,
257- callback : ( ) => void = ( ) => 0 ,
264+ callback : ( ) => void = ( ) => 0
258265 ) => {
259266 const id = this . ws_id ;
260267 this . ws_id += 3 ;
@@ -264,7 +271,10 @@ class WebSocketComm {
264271 message . Update . file_path = this . current_filename ! ;
265272 }
266273 console_log (
267- `Sent message ${ id } , ${ JSON . stringify ( message ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } ` ,
274+ `Sent message ${ id } , ${ JSON . stringify ( message ) . substring (
275+ 0 ,
276+ MAX_MESSAGE_LENGTH
277+ ) } `
268278 ) ;
269279 const jm : EditorMessage = {
270280 id : id ,
@@ -275,7 +285,7 @@ class WebSocketComm {
275285 timer_id : window . setTimeout (
276286 this . report_server_timeout ,
277287 RESPONSE_TIMEOUT ,
278- id ,
288+ id
279289 ) ,
280290 callback,
281291 } ;
@@ -301,7 +311,9 @@ class WebSocketComm {
301311 Result : result === null ? { Ok : "Void" } : { Err : result } ,
302312 } ;
303313 console_log (
304- `Sending result id = ${ id } , message = ${ JSON . stringify ( message ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } ` ,
314+ `Sending result id = ${ id } , message = ${ JSON . stringify (
315+ message
316+ ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } `
305317 ) ;
306318 // We can't simply call `send_message` because that function expects a
307319 // result message back from the server.
@@ -327,7 +339,7 @@ const set_content = (contents: CodeChatForWeb, cursor_position?: number) => {
327339 const cw =
328340 (
329341 root_iframe ! . contentDocument ?. getElementById (
330- "CodeChat-contents" ,
342+ "CodeChat-contents"
331343 ) as HTMLIFrameElement | undefined
332344 ) ?. contentWindow ?? root_iframe ! . contentWindow ! ;
333345 cw . document . open ( ) ;
@@ -337,7 +349,7 @@ const set_content = (contents: CodeChatForWeb, cursor_position?: number) => {
337349 } else {
338350 root_iframe ! . contentWindow ! . CodeChatEditor . open_lp (
339351 contents ,
340- cursor_position ,
352+ cursor_position
341353 ) ;
342354 }
343355} ;
@@ -356,7 +368,7 @@ export const page_init = (
356368 // nice, interactive definition of the components of a URL.
357369 ws_pathname : string ,
358370 // Test mode flag
359- testMode_ : boolean ,
371+ testMode_ : boolean
360372) => {
361373 testMode = testMode_ ;
362374 on_dom_content_loaded ( async ( ) => {
@@ -365,10 +377,10 @@ export const page_init = (
365377 const protocol = window . location . protocol === "http:" ? "ws:" : "wss:" ;
366378 // Build a websocket address based on the URL of the current page.
367379 webSocketComm = new WebSocketComm (
368- `${ protocol } //${ window . location . host } /${ ws_pathname } ` ,
380+ `${ protocol } //${ window . location . host } /${ ws_pathname } `
369381 ) ;
370382 root_iframe = document . getElementById (
371- "CodeChat-iframe" ,
383+ "CodeChat-iframe"
372384 ) ! as HTMLIFrameElement ;
373385 window . CodeChatEditorFramework = {
374386 webSocketComm,
0 commit comments