diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2018-12-14 15:42:59 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2018-12-14 15:42:59 -0500 |
| commit | c1932084390aca19c748da024b7b168c160a3aea (patch) | |
| tree | 9a9865eda9aed3d1127eecb332ec799bd8d051cd /src/settings.sml | |
| parent | 720e1cb2c84dfd274fcbfd7bf4974a1c110501cb (diff) | |
New .urp option: safeGetDefault
Diffstat (limited to 'src/settings.sml')
| -rw-r--r-- | src/settings.sml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/settings.sml b/src/settings.sml index cfbe98a5..3772fc04 100644 --- a/src/settings.sml +++ b/src/settings.sml @@ -740,9 +740,11 @@ structure SS = BinarySetFn(struct val compare = String.compare end) +val safeGetDefault = ref false val safeGet = ref SS.empty +fun setSafeGetDefault b = safeGetDefault := b fun setSafeGets ls = safeGet := SS.addList (SS.empty, ls) -fun isSafeGet x = SS.member (!safeGet, x) +fun isSafeGet x = !safeGetDefault orelse SS.member (!safeGet, x) val onError = ref (NONE : (string * string list * string) option) fun setOnError x = onError := x |