diff src/export.sml @ 735:5ccb67665d05

Only use cookie signatures when cookies might be read
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Apr 2009 14:10:10 -0400
parents 5819fb63c93a
children b106ca8200b1
line wrap: on
line diff
--- a/src/export.sml	Thu Apr 16 19:12:12 2009 -0400
+++ b/src/export.sml	Thu Apr 23 14:10:10 2009 -0400
@@ -25,13 +25,14 @@
  * POSSIBILITY OF SUCH DAMAGE.
  *)
 
-structure Export = struct
+structure Export :> EXPORT = struct
 
 open Print.PD
 open Print
 
 datatype effect =
          ReadOnly
+       | ReadCookieWrite
        | ReadWrite
 
 datatype export_kind =
@@ -42,6 +43,7 @@
 fun p_effect ef =
     case ef of
         ReadOnly => string "r"
+      | ReadCookieWrite => string "rcw"
       | ReadWrite => string "rw"
 
 fun p_export_kind ck =