1
/* -*- Mode: C++; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*-
3
* The contents of this file are subject to the Mozilla Public License
4
* Version 1.1 (the "License"); you may not use this file except in
5
* compliance with the License. You may obtain a copy of the License at
6
* http://www.mozilla.org/MPL/
8
* Software distributed under the License is distributed on an "AS IS" basis,
9
* WITHOUT WARRANTY OF ANY KIND, either express or implied. See the License
10
* for the specific language governing rights and limitations under the
13
* The Original Code is The JavaScript Debugger
15
* The Initial Developer of the Original Code is
16
* Netscape Communications Corporation
17
* Portions created by Netscape are
18
* Copyright (C) 1998 Netscape Communications Corporation.
20
* Alternatively, the contents of this file may be used under the
21
* terms of the GNU Public License (the "GPL"), in which case the
22
* provisions of the GPL are applicable instead of those above.
23
* If you wish to allow use of your version of this file only
24
* under the terms of the GPL and not to allow others to use your
25
* version of this file under the MPL, indicate your decision by
26
* deleting the provisions above and replace them with the notice
27
* and other provisions required by the GPL. If you do not delete
28
* the provisions above, a recipient may use your version of this
29
* file under either the MPL or the GPL.
32
* Robert Ginda, <rginda@netscape.com>, original author
38
var dir = getSpecialDirectory("ProfD");
39
dir.append("venkman-settings.js");
40
var defaultSettingsFile = dir.path;
42
console.prefManager = new PrefManager("extensions.venkman.");
43
console.prefs = console.prefManager.prefs;
47
["enableChromeFilter", true],
49
["guessPattern", "(\\w+)\\s*[:=]\\s*$"],
50
["initialScripts", ""],
51
["lastErrorMode", "ignore"],
52
["lastThrowMode", "ignore"],
53
["maxStringLength", 4000],
54
["menubarInFloaters", navigator.platform.indexOf ("Mac") != -1],
55
["permitStartupHit", true],
56
["prettyprint", false],
57
["rememberPrettyprint", false],
58
["saveSettingsOnExit", false],
59
["settingsFile", defaultSettingsFile],
61
["statusDuration", 5 * 1000],
65
console.prefManager.addPrefs(prefs);
68
function destroyPrefs()
70
console.prefManager.destroy();