aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/settings.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-01-13 18:15:04 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2011-01-13 18:15:04 -0500
commite3ce087d0a3473e3905556c226d6c5bbb2bc9a39 (patch)
tree8b084eda74b40c5837e84f4fdd6cc82b57112fb6 /src/settings.sml
parent11df1bdd195e0b04e748d0fe35d1f805e207ead0 (diff)
alwaysInline .urp setting
Diffstat (limited to 'src/settings.sml')
-rw-r--r--src/settings.sml9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/settings.sml b/src/settings.sml
index ec0f582d..5edb1fde 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -539,4 +539,13 @@ val minHeap = ref 0
fun setMinHeap n = if n >= 0 then minHeap := n else raise Fail "Trying to set negative minHeap"
fun getMinHeap () = !minHeap
+structure SS = BinarySetFn(struct
+ type ord_key = string
+ val compare = String.compare
+ end)
+
+val alwaysInline = ref SS.empty
+fun addAlwaysInline s = alwaysInline := SS.add (!alwaysInline, s)
+fun checkAlwaysInline s = SS.member (!alwaysInline, s)
+
end