44//
55// window, wsHost, wsPort
66//
7+ const document = window . document ;
78
89import morphdom from 'morphdom' ;
910
11+ import cssText from 'bundle-text:./watch_hotreload_style.css' ;
12+
1013declare var wsHost : string ;
1114declare var wsPort : number ;
1215
@@ -154,7 +157,7 @@ function updateInstructionsReceived(mainContainer: HTMLElement, info : UpdateInf
154157}*/
155158
156159type UpdateInfo = {
157- action : 'update-main-content' ,
160+ action : 'update-main-content' | 'error-display' ,
158161 content_html : string ,
159162} ;
160163
@@ -360,9 +363,46 @@ function stampMathContentSources(mainContainer: HTMLElement, elements: HTMLEleme
360363 }
361364}
362365
366+ function clearErrorOverlay ( )
367+ {
368+ const overlayDiv = document . getElementById ( 'ErrorOverlay' ) ;
369+ if ( overlayDiv != null ) {
370+ overlayDiv . classList . remove ( 'error-overlay-shown' ) ;
371+ }
372+ }
373+ function displayErrorOverlay ( mainContainer : HTMLElement , info : UpdateInfo )
374+ {
375+ const makeErrorOverlayDiv = ( ) => {
376+ const el = document . getElementById ( 'ErrorOverlay' ) ;
377+ if ( el != null ) {
378+ return el ;
379+ }
380+ const newEl = document . createElement ( 'div' ) ;
381+ newEl . setAttribute ( 'id' , 'ErrorOverlay' ) ;
382+ document . body . appendChild ( newEl ) ;
383+ return newEl ;
384+ } ;
385+ let overlay = makeErrorOverlayDiv ( ) ;
386+
387+ overlay . classList . add ( 'error-overlay-shown' ) ;
388+
389+ overlay . innerHTML = info . content_html ;
390+ }
391+
363392window . addEventListener ( "DOMContentLoaded" , ( ) => {
364393
394+ //
395+ // inject our style tag, mainly for the error overlay display
396+ //
397+ let style = document . createElement ( 'style' ) ;
398+ style . textContent = cssText ;
399+ document . head . appendChild ( style ) ;
400+
401+ //
402+ // Our main container div
403+ //
365404 const mainContainer = document . getElementById ( 'Main' ) ! ;
405+
366406 //
367407 // First of all, stamp all our equations with the source math data to help
368408 // us process updates.
@@ -376,11 +416,18 @@ window.addEventListener("DOMContentLoaded", () => {
376416 websocket . addEventListener ( "message" , function ( m ) {
377417 console . log ( "Message!" , m ) ;
378418 const info = JSON . parse ( m . data ) as UpdateInfo ;
379- try {
380- updateMainContent ( mainContainer , info ) ;
381- } catch ( err ) {
382- // failure in the incremental update, so reload everything ... :/
383- window . location . reload ( ) ;
419+ clearErrorOverlay ( ) ;
420+ if ( info . action === 'update-main-content' ) {
421+ try {
422+ updateMainContent ( mainContainer , info ) ;
423+ } catch ( err ) {
424+ // failure in the incremental update, so reload everything ... :/
425+ window . location . reload ( ) ;
426+ }
427+ } else if ( info . action === 'error-display' ) {
428+ displayErrorOverlay ( mainContainer , info ) ;
429+ } else {
430+ console . error ( "Invalid update info action!" , info ) ;
384431 }
385432 } ) ;
386433 websocket . addEventListener ( "open" , function ( ) { console . log ( "websocket open" ) ; } ) ;
0 commit comments