// Copyright 2024 The Go Authors. All rights reserved.
// Use of this source code is governed by a BSD-style
// license that can be found in the LICENSE file.
// httpGET requests a URL for its effects only.
// (It is needed for /open URLs; see objHTML.)
function httpGET(url) {
var x = new XMLHttpRequest();
x.open("GET", url, true);
x.send();
return false; // disable usual <a href=...> behavior
}
// disconnect banner
window.addEventListener('load', function() {
// Create a hidden <div id='disconnected'> element.
var banner = document.createElement("div");
banner.id = "disconnected";
banner.innerText = "Gopls server has terminated. Page is inactive.";
document.body.appendChild(banner);
// Start a GET /hang request. If it ever completes, the server
// has disconnected. Reveal the banner in that case.
var x = new XMLHttpRequest();
x.open("GET", "/hang", true);
x.onloadend = () => { banner.style.display = "block"; };
x.send();
});