diff src/prim.sml @ 2048:4d64af730e35

Differentiate between HTML and normal string literals
author Adam Chlipala <adam@chlipala.net>
date Fri, 01 Aug 2014 15:44:17 -0400
parents 3e7c7e200713
children
line wrap: on
line diff
--- a/src/prim.sml	Fri Aug 01 11:43:44 2014 -0400
+++ b/src/prim.sml	Fri Aug 01 15:44:17 2014 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008, 2014, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -27,10 +27,12 @@
 
 structure Prim :> PRIM = struct
 
+datatype string_mode = Normal | Html
+
 datatype t =
          Int of Int64.int
        | Float of Real64.real
-       | String of string
+       | String of string_mode * string
        | Char of char
 
 open Print.PD
@@ -40,7 +42,7 @@
     case t of
         Int n => string (Int64.toString n)
       | Float n => string (Real64.toString n)
-      | String s => box [string "\"", string (String.toString s), string "\""]
+      | String (_, s) => box [string "\"", string (String.toString s), string "\""]
       | Char ch => box [string "#\"", string (String.toString (String.str ch)), string "\""]
 
 fun int2s n =
@@ -61,7 +63,7 @@
     case t of
         Int n => int2s' n
       | Float n => float2s n
-      | String s => s
+      | String (_, s) => s
       | Char ch => str ch
 
 fun pad (n, ch, s) =
@@ -86,14 +88,14 @@
     case t of
         Int n => string (int2s n)
       | Float n => string (float2s n)
-      | String s => box [string "\"", string (toCString s), string "\""]
+      | String (_, s) => box [string "\"", string (toCString s), string "\""]
       | Char ch => box [string "'", string (toCChar ch), string "'"]
 
 fun equal x =
     case x of
         (Int n1, Int n2) => n1 = n2
       | (Float n1, Float n2) => Real64.== (n1, n2)
-      | (String s1, String s2) => s1 = s2
+      | (String (_, s1), String (_, s2)) => s1 = s2
       | (Char ch1, Char ch2) => ch1 = ch2
 
       | _ => false
@@ -108,7 +110,7 @@
       | (Float _, _) => LESS
       | (_, Float _) => GREATER 
 
-      | (String n1, String n2) => String.compare (n1, n2)
+      | (String (_, n1), String (_, n2)) => String.compare (n1, n2)
       | (String _, _) => LESS
       | (_, String _) => GREATER