-export function refresh_page() {
- let pagename = window.location.pathname.replace('.html', '').replace(/^.*\//, '');
+/**
+ * Update the global page state.
+ *
+ * When called without a parameter, then the current window.location is
+ * parsed and the page state is set accordingly. Otherwise the page state
+ * is set from the parameters. 'pagename' is the overall subpage (without
+ * .html extension). 'params' must be an URLSearchParams object and contain
+ * the requested query parameters. It may also be omitted completely for a
+ * link without query parameters.
+ */
+export function refresh_page(pagename, params) {
+ if (typeof pagename === 'undefined') {
+ pagename = window.location.pathname.replace('.html', '').replace(/^.*\//, '');