diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2014-08-01 15:44:17 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2014-08-01 15:44:17 -0400 |
| commit | 1816e4664bfa4b10cfdb9d10a871343acb250f83 (patch) | |
| tree | 76d0a9801c5ad0dc1e08f11635a8c2010926586b /src/prim.sml | |
| parent | 32aa8589761b58e24715818a7b3af73d69055b27 (diff) | |
Differentiate between HTML and normal string literals
Diffstat (limited to 'src/prim.sml')
| -rw-r--r-- | src/prim.sml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/prim.sml b/src/prim.sml index 94801e7f..1de4fc7b 100644 --- a/src/prim.sml +++ b/src/prim.sml @@ -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 @@ fun p_t t = 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 @@ fun toString t = 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 @@ fun p_t_GCC t = 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 @@ fun compare (p1, p2) = | (Float _, _) => LESS | (_, Float _) => GREATER - | (String n1, String n2) => String.compare (n1, n2) + | (String (_, n1), String (_, n2)) => String.compare (n1, n2) | (String _, _) => LESS | (_, String _) => GREATER |