@@ -43,6 +43,7 @@ import {
4343} from "./shared_types.mjs" ;
4444import {
4545 console_log ,
46+ DEBUG_ENABLED ,
4647 on_error ,
4748 on_dom_content_loaded ,
4849} from "./CodeChatEditor.mjs" ;
@@ -65,9 +66,11 @@ class WebSocketComm {
6566 // Use a unique ID for each websocket message sent. See the Implementation
6667 // section on Message IDs for more information.
6768 ws_id = - 9007199254740988 ;
69+
6870 // The websocket used by this class. Really a `ReconnectingWebSocket`, but
6971 // that's not a type.
7072 ws : WebSocket ;
73+
7174 // A map of message id to (timer id, callback) for all pending messages.
7275 pending_messages : Record <
7376 number ,
@@ -76,10 +79,16 @@ class WebSocketComm {
7679 callback : ( ) => void ;
7780 }
7881 > = { } ;
82+
7983 // The current filename of the file being edited. This is provided by the
8084 // IDE and passed back to it, but not otherwise used by the Framework.
8185 current_filename : string | undefined = undefined ;
8286
87+ // True when the iframe is loading, so that an `Update` should be postponed
88+ // until the page load is finished. Otherwise, the page is fully loaded, so
89+ // the `Update` may be applied immediately.
90+ is_loading = false ;
91+
8392 // A promise to serialize calls to `set_content`.
8493 promise = Promise . resolve ( ) ;
8594
@@ -112,11 +121,9 @@ class WebSocketComm {
112121 // Parse the received message, which must be a single element of a
113122 // dictionary representing a `JointMessage`.
114123 const joint_message = JSON . parse ( event . data ) as EditorMessage ;
115- const { id : id , message : message } = joint_message ;
124+ const { id, message } = joint_message ;
116125 console_log (
117- `Received data id = ${ id } , message = ${ JSON . stringify (
118- message ,
119- ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } `,
126+ `Received data id = ${ id } , message = ${ format_struct ( message ) } ` ,
120127 ) ;
121128 assert ( id !== undefined ) ;
122129 assert ( message !== undefined ) ;
@@ -130,62 +137,61 @@ class WebSocketComm {
130137 case "Update" :
131138 // Load this data in.
132139 const current_update = value as UpdateMessageContents ;
133- // Check or update the `current_filename`.
134- if ( this . current_filename === undefined ) {
135- this . current_filename = current_update . file_path ;
136- } else if (
137- current_update . file_path !== this . current_filename
138- ) {
139- const msg = `Ignoring update for ${ current_update . file_path } because it's not the current file ${ this . current_filename } .` ;
140- report_error ( msg ) ;
141- this . send_result ( id , msg ) ;
142- break ;
143- }
144- const contents = current_update . contents ;
145- const cursor_position = current_update . cursor_position ;
146- if ( contents !== undefined ) {
147- if (
148- root_iframe ! . contentDocument ?. readyState ===
149- "complete"
140+ // The rest of this should run after all other messages have been processed.
141+ this . promise = this . promise . finally ( async ( ) => {
142+ // Check or update the `current_filename`.
143+ if ( this . current_filename === undefined ) {
144+ this . current_filename = current_update . file_path ;
145+ } else if (
146+ current_update . file_path !== this . current_filename
150147 ) {
151- // Wait until after the DOM is ready, since we rely on content set in `on_dom_content_loaded` in the Client.
152- this . promise = this . promise . finally (
153- async ( ) =>
154- await set_content (
155- contents ,
156- current_update . cursor_position ,
157- ) ,
158- ) ;
159- } else {
160- // If the page is still loading, wait until the load
161- // completes before updating the editable contents.
162- //
163- // Construct the promise to use; this causes the
164- // `onload` callback to be set immediately.
165- const p = new Promise < void > (
166- ( resolve ) =>
167- ( root_iframe ! . onload = async ( ) => {
168- await set_content (
169- contents ,
170- current_update . cursor_position ,
171- ) ;
172- resolve ( ) ;
173- } ) ,
174- ) ;
175- this . promise = this . promise . finally ( ( ) => p ) ;
148+ const msg = `Ignoring update for ${ current_update . file_path } because it's not the current file ${ this . current_filename } .` ;
149+ report_error ( msg ) ;
150+ this . send_result ( id , msg ) ;
151+ return ;
176152 }
177- } else if ( cursor_position !== undefined ) {
178- // We might receive a message while the Client is
179- // reloading; during this period, `scroll_to_line` isn't
180- // defined.
181- this . promise = this . promise . finally ( ( ) =>
182- root_iframe ! . contentWindow ?. CodeChatEditor . scroll_to_line ?.(
153+ const contents = current_update . contents ;
154+ const cursor_position = current_update . cursor_position ;
155+ if ( contents !== undefined ) {
156+ // I'd prefer to use a system-maintained value to determine the ready state of the iframe,
157+ // such as `readyState`. However, this value only applies to the initial load of the iframe;
158+ // it doesn't change when the iframe's `src` attribute is changed. So, we have to track
159+ // this manually instead.
160+ if ( ! this . is_loading ) {
161+ // Wait until after the DOM is ready, since we rely on content set in `on_dom_content_loaded` in the Client.
162+ await set_content (
163+ contents ,
164+ current_update . cursor_position ,
165+ ) ;
166+ } else {
167+ // If the page is still loading, wait until the load
168+ // completes before updating the editable contents.
169+ //
170+ // Construct the promise to use; this causes the
171+ // `onload` callback to be set immediately.
172+ await new Promise < void > (
173+ ( resolve ) =>
174+ ( root_iframe ! . onload = async ( ) => {
175+ this . is_loading = false ;
176+ await set_content (
177+ contents ,
178+ current_update . cursor_position ,
179+ ) ;
180+ resolve ( ) ;
181+ } ) ,
182+ ) ;
183+ }
184+ } else if ( cursor_position !== undefined ) {
185+ // We might receive a message while the Client is
186+ // reloading; during this period, `scroll_to_line` isn't
187+ // defined.
188+ root_iframe ! . contentWindow ?. CodeChatEditor ?. scroll_to_line ?.(
183189 cursor_position ,
184- ) ,
185- ) ;
186- }
190+ ) ;
191+ }
187192
188- this . send_result ( id , null ) ;
193+ this . send_result ( id , null ) ;
194+ } ) ;
189195 break ;
190196
191197 case "CurrentFile" :
@@ -199,27 +205,27 @@ class WebSocketComm {
199205 ? "?test"
200206 : "&test"
201207 : "" ;
202- // If the page is still loading, then don't save. Otherwise,
203- // save the editor contents if necessary.
204- const cce = get_client ( ) ;
205- this . promise = this . promise
206- . finally ( ( ) => cce ?. on_save ( true ) )
207- . finally ( ( ) => {
208- // Now, it's safe to load a new file.
209- // Tell the client to allow this navigation -- the
210- // document it contains has already been saved.
211- if ( cce !== undefined ) {
212- cce . allow_navigation = true ;
213- }
214- this . set_root_iframe_src ( current_file + testSuffix ) ;
215- // The `current_file` is a URL-encoded path, not a
216- // filesystem path. So, we can't use it for
217- // `current_filename`. Instead, signal that the
218- // `current_filename` should be set on the next `Update`
219- // message.
220- this . current_filename = undefined ;
221- this . send_result ( id , null ) ;
222- } ) ;
208+ // Execute this after all other messages have been processed.
209+ this . promise = this . promise . finally ( async ( ) => {
210+ // If the page is still loading, then don't save. Otherwise,
211+ // save the editor contents if necessary.
212+ const cce = get_client ( ) ;
213+ await cce ?. on_save ( true ) ;
214+ // Now, it's safe to load a new file.
215+ // Tell the client to allow this navigation -- the
216+ // document it contains has already been saved.
217+ if ( cce !== undefined ) {
218+ cce . allow_navigation = true ;
219+ }
220+ this . set_root_iframe_src ( current_file + testSuffix ) ;
221+ // The `current_file` is a URL-encoded path, not a
222+ // filesystem path. So, we can't use it for
223+ // `current_filename`. Instead, signal that the
224+ // `current_filename` should be set on the next `Update`
225+ // message.
226+ this . current_filename = undefined ;
227+ this . send_result ( id , null ) ;
228+ } ) ;
223229 break ;
224230
225231 case "Result" :
@@ -244,27 +250,30 @@ class WebSocketComm {
244250 break ;
245251
246252 default :
247- const msg = `Received unhandled message ${ key } (${ JSON . stringify (
253+ const msg = `Received unhandled message ${ key } (${ format_struct (
248254 value ,
249- ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } )`;
255+ ) } )`;
250256 report_error ( msg ) ;
251257 this . send_result ( id , msg ) ;
252258 break ;
253259 }
254260 } ;
255261 }
256262
263+ send = ( data : any ) => this . ws . send ( data ) ;
264+ close = ( ...args : any ) => this . ws . close ( ...args ) ;
265+
257266 set_root_iframe_src = ( url : string ) => {
258267 // Set the new src to (re)load content. At startup, the `srcdoc`
259268 // attribute shows some welcome text. Remove it so that we can now
260269 // assign the `src` attribute.
261270 root_iframe ! . removeAttribute ( "srcdoc" ) ;
262271 root_iframe ! . src = url ;
272+ // Track the `is_loading` status.
273+ this . is_loading = true ;
274+ root_iframe ! . onload = ( ) => ( this . is_loading = false ) ;
263275 } ;
264276
265- send = ( data : any ) => this . ws . send ( data ) ;
266- close = ( ...args : any ) => this . ws . close ( ...args ) ;
267-
268277 // Report an error from the server.
269278 report_server_timeout = ( message_id : number ) => {
270279 delete this . pending_messages [ message_id ] ;
@@ -283,12 +292,7 @@ class WebSocketComm {
283292 assert ( this . current_filename !== undefined ) ;
284293 message . Update . file_path = this . current_filename ! ;
285294 }
286- console_log (
287- `Sent message ${ id } , ${ JSON . stringify ( message ) . substring (
288- 0 ,
289- MAX_MESSAGE_LENGTH ,
290- ) } `,
291- ) ;
295+ console_log ( `Sent message ${ id } , ${ format_struct ( message ) } ` ) ;
292296 const jm : EditorMessage = {
293297 id : id ,
294298 message : message ,
@@ -304,17 +308,24 @@ class WebSocketComm {
304308 } ;
305309 } ;
306310
311+ // This is called by the Client when the user navigates to another webpage.
307312 current_file = ( url : URL ) => {
308- // If this points to the Server, then tell the IDE to load a new file.
309- if ( url . host === window . location . host ) {
310- this . send_message ( { CurrentFile : [ url . toString ( ) , null ] } , ( ) => {
313+ this . promise = this . promise . finally ( ( ) => {
314+ if ( url . host === window . location . host ) {
315+ // If this points to the Server, then tell the IDE to load a new file.
316+ this . send_message (
317+ { CurrentFile : [ url . toString ( ) , null ] } ,
318+ ( ) => {
319+ this . set_root_iframe_src ( url . toString ( ) ) ;
320+ } ,
321+ ) ;
322+ } else {
323+ // Otherwise, navigate to the provided page.
311324 this . set_root_iframe_src ( url . toString ( ) ) ;
312- } ) ;
313- } else {
314- this . set_root_iframe_src ( url . toString ( ) ) ;
315- }
316- // Read the `current_filename` from the next `Update` message.
317- this . current_filename = undefined ;
325+ }
326+ // Read the `current_filename` from the next `Update` message.
327+ this . current_filename = undefined ;
328+ } ) ;
318329 } ;
319330
320331 // Send a result (a response to a message from the server) back to the
@@ -324,9 +335,7 @@ class WebSocketComm {
324335 Result : result === null ? { Ok : "Void" } : { Err : result } ,
325336 } ;
326337 console_log (
327- `Sending result id = ${ id } , message = ${ JSON . stringify (
328- message ,
329- ) . substring ( 0 , MAX_MESSAGE_LENGTH ) } `,
338+ `Sending result id = ${ id } , message = ${ format_struct ( message ) } ` ,
330339 ) ;
331340 // We can't simply call `send_message` because that function expects a
332341 // result message back from the server.
@@ -426,6 +435,15 @@ const show_toast = (text: string) => {
426435 }
427436} ;
428437
438+ // Format a complex data structure as a string when in debug mode.
439+ export const format_struct = ( complex_data_structure : any ) : string =>
440+ DEBUG_ENABLED
441+ ? JSON . stringify ( complex_data_structure ) . substring (
442+ 0 ,
443+ MAX_MESSAGE_LENGTH ,
444+ )
445+ : "" ;
446+
429447const report_error = ( text : string ) => {
430448 console . error ( text ) ;
431449 show_toast ( text ) ;
0 commit comments