diff 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
line wrap: on
line diff
--- a/src/scriptcheck.sml	Tue Jun 23 15:40:35 2009 -0400
+++ b/src/scriptcheck.sml	Tue Jun 23 15:56:04 2009 -0400
@@ -73,6 +73,8 @@
 
 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 @@
 
         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