new object $www_preferences: $user_interfaces;

var $dmi_data descriptions = #[];
var $has_commands local = #[];
var $has_commands remote = #[];
var $has_commands shortcuts = #[];
var $root created_on = 867669920;
var $root defined_settings = #[["www-show-line-num", #[['parse, ['is_boolean]], ['format, ['format_boolean]]]], ["www-show-descriptions", #[['parse, ['is_boolean]], ['format, ['format_boolean]]]], ["www-show-methods", #[['parse, ['is_boolean]], ['format, ['format_boolean]]]], ["www-show-variables", #[['parse, ['is_boolean]], ['format, ['format_boolean]]]]];
var $root flags = ['variables, 'methods, 'code, 'fertile, 'core];
var $root inited = 1;
var $root managed = [$www_preferences];
var $root manager = $www_preferences;
var $root settings = #[["www-show-line-num", 0], ["www-show-descriptions", 0], ["www-show-methods", 0], ["www-show-variables", 0]];

public method .set_www_preferences() {
    arg name, value;
    
    (> .perms(caller(), $page_web_prefs, this()) <);
    .set_setting(name, $www_preferences, value);
};