comparison src/scriptcheck.sml @ 855:28e42b22424d

Initial implementation of protocols in Settings
author Adam Chlipala <adamc@hcoop.net>
date Tue, 23 Jun 2009 15:56:04 -0400
parents 9330ba3a2799
children 346cf1908a17
comparison
equal deleted inserted replaced
854:158d980889ac 855:28e42b22424d
71 71
72 val pushWords = ["rv("] 72 val pushWords = ["rv("]
73 73
74 fun classify (ds, ps) = 74 fun classify (ds, ps) =
75 let 75 let
76 val proto = Settings.currentProtocol ()
77
76 fun inString {needle, haystack} = 78 fun inString {needle, haystack} =
77 let 79 let
78 val (_, suffix) = Substring.position needle (Substring.full haystack) 80 val (_, suffix) = Substring.position needle (Substring.full haystack)
79 in 81 in
80 not (Substring.isEmpty suffix) 82 not (Substring.isEmpty suffix)
156 | _ => (pull_ids, push_ids) 158 | _ => (pull_ids, push_ids)
157 end 159 end
158 160
159 val (pull_ids, push_ids) = foldl decl (IS.empty, IS.empty) ds 161 val (pull_ids, push_ids) = foldl decl (IS.empty, IS.empty) ds
160 162
163 val foundBad = ref false
164
161 val ps = map (fn (ek, x, n, ts, t, _) => 165 val ps = map (fn (ek, x, n, ts, t, _) =>
162 (ek, x, n, ts, t, 166 (ek, x, n, ts, t,
163 if IS.member (push_ids, n) then 167 if IS.member (push_ids, n) then
164 ServerAndPullAndPush 168 (if not (#supportsPush proto) andalso not (!foundBad) then
169 (foundBad := true;
170 ErrorMsg.error ("This program needs server push, but the current protocol ("
171 ^ #name proto ^ ") doesn't support that."))
172 else
173 ();
174 ServerAndPullAndPush)
165 else if IS.member (pull_ids, n) then 175 else if IS.member (pull_ids, n) then
166 ServerAndPull 176 ServerAndPull
167 else 177 else
168 ServerOnly)) ps 178 ServerOnly)) ps
169 in 179 in