diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-06-23 15:56:04 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-06-23 15:56:04 -0400 |
| commit | 32b2d196fc02ca4f9f87574e6da1ffa6c1ea12ab (patch) | |
| tree | 5c08087fd98403edb3500ac4399ddece25c667ad /src/scriptcheck.sml | |
| parent | 1109a4e1c8b10a8f524c1406a4db98eff55b435c (diff) | |
Initial implementation of protocols in Settings
Diffstat (limited to 'src/scriptcheck.sml')
| -rw-r--r-- | src/scriptcheck.sml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/scriptcheck.sml b/src/scriptcheck.sml index 834ff1c7..e0b9f855 100644 --- a/src/scriptcheck.sml +++ b/src/scriptcheck.sml @@ -73,6 +73,8 @@ val pushWords = ["rv("] fun classify (ds, ps) = let + val proto = Settings.currentProtocol () + fun inString {needle, haystack} = let val (_, suffix) = Substring.position needle (Substring.full haystack) @@ -158,10 +160,18 @@ fun classify (ds, ps) = val (pull_ids, push_ids) = foldl decl (IS.empty, IS.empty) ds + val foundBad = ref false + val ps = map (fn (ek, x, n, ts, t, _) => (ek, x, n, ts, t, if IS.member (push_ids, n) then - ServerAndPullAndPush + (if not (#supportsPush proto) andalso not (!foundBad) then + (foundBad := true; + ErrorMsg.error ("This program needs server push, but the current protocol (" + ^ #name proto ^ ") doesn't support that.")) + else + (); + ServerAndPullAndPush) else if IS.member (pull_ids, n) then ServerAndPull else |