[COMMITTED] poke: fix styling in settings

[Jose E. Marchesi]

2023-10-28  Jose E. Marchesi  <jemarch@gnu.org>

        * poke/pk-settings.pk (pk_settings_dump): Do not emit hyperlinks
        for setting headers, but style it.
        * poke/pk-cmd-set.c (pk_cmd_set_dump): Likewise.
---
 ChangeLog           |  6 ++++++
 poke/pk-cmd-set.c   | 17 ++---------------
 poke/pk-settings.pk |  3 +--
 3 files changed, 9 insertions(+), 17 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index b16b947a..1b7f99fe 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2023-10-28  Jose E. Marchesi  <jemarch@gnu.org>
+
+       * poke/pk-settings.pk (pk_settings_dump): Do not emit hyperlinks
+       for setting headers, but style it.
+       * poke/pk-cmd-set.c (pk_cmd_set_dump): Likewise.
+
 2023-10-28  Jose E. Marchesi  <jemarch@gnu.org>
 
        * poke/pk-hserver.pk (hserver_print_hl): Make it possible to style
diff --git a/poke/pk-cmd-set.c b/poke/pk-cmd-set.c
index a8dfa08d..64ee2a3f 100644
--- a/poke/pk-cmd-set.c
+++ b/poke/pk-cmd-set.c
@@ -41,22 +41,9 @@ pk_cmd_set_dump (int argc, struct pk_cmd_arg argv[], 
uint64_t uflags)
       || exit_exception != PK_NULL)
     PK_UNREACHABLE (); /* This shouldn't happen.  */
 
-#if HAVE_HSERVER
-  {
-    char *hyperlink;
-
-    hyperlink = pk_hserver_make_hyperlink ('e', ".help error-on-warning", 
PK_NULL);
-    pk_term_class ("hyperlink");
-    pk_term_hyperlink (hyperlink, NULL);
-  }
-#endif
-
+  pk_term_class ("setting-header");
   pk_puts ("error-on-warning");
-
-#if HAVE_HSERVER
-  pk_term_end_hyperlink ();
-  pk_term_end_class ("hyperlink");
-#endif
+  pk_term_end_class ("setting-header");
   pk_printf (" %s\n", pk_error_on_warning (poke_compiler) ? "yes" : "no");
 
   return 0;
diff --git a/poke/pk-settings.pk b/poke/pk-settings.pk
index 72a0885f..6ac6415f 100644
--- a/poke/pk-settings.pk
+++ b/poke/pk-settings.pk
@@ -654,8 +654,7 @@ fun pk_settings_dump = void:
     for (setting in pk_settings.entries)
       {
         table.row;
-        table.column (setting.name, "",
-                      hserver_make_hyperlink ('e', ".help " + setting.name));
+        table.column (setting.name, "setting-header");
         table.column (setting.kind == POKE_SETTING_INT
                       ? format ("%i32d", setting.getter as int<32>)
                       : setting.kind == POKE_SETTING_BOOL
-- 
2.30.2