Mercurial > urweb
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