aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/monoize.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-14 09:33:48 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-14 09:33:48 -0400
commitb6163966d74b8f4636d63f28179205ed9f6daaaf (patch)
treea2cae7eab132b9d3a0e2a1761daa414b869cdf3e /src/monoize.sml
parent9e6bd5dd1394c99f0a9b29369a4957c958e0830c (diff)
cselect
Diffstat (limited to 'src/monoize.sml')
-rw-r--r--src/monoize.sml31
1 files changed, 30 insertions, 1 deletions
diff --git a/src/monoize.sml b/src/monoize.sml
index b71b13a5..86a27543 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -2563,7 +2563,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
| SOME (_, src, _) =>
(strcat [str "<span><script type=\"text/javascript\">inp(\"input\",",
(L'.EJavaScript (L'.Script, src, NONE), loc),
- str ")</script></span>"],
+ str ",\"\")</script></span>"],
fm))
| _ => (Print.prefaces "Targs" (map (fn t => ("T", CorePrint.p_con env t)) targs);
raise Fail "No name passed to textbox tag"))
@@ -2635,6 +2635,33 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
let
val sc = strcat [str "inp(\"input\",",
(L'.EJavaScript (L'.Script, src, NONE), loc),
+ str ",\"\")"]
+ val sc = setAttrs sc
+ in
+ (strcat [str "<span><script type=\"text/javascript\">",
+ sc,
+ str "</script></span>"],
+ fm)
+ end)
+
+ | "cselect" =>
+ (case List.find (fn ("Source", _, _) => true | _ => false) attrs of
+ NONE =>
+ let
+ val (ts, fm) = tagStart "select"
+ in
+ ((L'.EStrcat (ts,
+ (L'.EPrim (Prim.String "/>"), loc)),
+ loc), fm)
+ end
+ | SOME (_, src, _) =>
+ let
+ val (xml, fm) = monoExp (env, st, fm) xml
+
+ val sc = strcat [str "inp(\"select\",",
+ (L'.EJavaScript (L'.Script, src, NONE), loc),
+ str ",",
+ (L'.EJavaScript (L'.Script, xml, NONE), loc),
str ")"]
val sc = setAttrs sc
in
@@ -2644,6 +2671,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
fm)
end)
+ | "coption" => normal ("option", NONE, NONE)
+
| "tabl" => normal ("table", NONE, NONE)
| _ => normal (tag, NONE, NONE)
end