@@ -0,0 +1,87 @@
1+module JavaScript
2+
3+%access public
4+
5+--------------------------------------------------------------------------------
6+-- Elements
7+--------------------------------------------------------------------------------
8+abstract
9+data Element : Type where
10+ MkElem : Ptr -> Element
11+
12+setText : Element -> String -> IO ()
13+setText (MkElem p) s =
14+ mkForeign (FFun ".textContent=" [FPtr, FString] FUnit) p s
15+
16+
17+setOnClick : Element -> (Event -> IO Bool) -> IO ()
18+setOnClick (MkElem e) f =
19+ mkForeign (
20+ FFun "['onclick']=" [ FPtr
21+ , FFunction (FAny Event) (FAny (IO Bool))
22+ ] FUnit) e f
23+--------------------------------------------------------------------------------
24+-- Events
25+--------------------------------------------------------------------------------
26+abstract
27+data Event : Type where
28+ MkEvent : Ptr -> Event
29+
30+--------------------------------------------------------------------------------
31+-- Nodelists
32+--------------------------------------------------------------------------------
33+abstract
34+data NodeList : Type where
35+ MkNodeList : Ptr -> NodeList
36+
37+elemAt : NodeList -> Nat -> IO Element
38+elemAt (MkNodeList p) i = do
39+ i <- mkForeign (FFun ".item" [FPtr, FInt] FPtr) p (cast i)
40+ return (MkElem i)
41+--------------------------------------------------------------------------------
42+-- Intervals
43+--------------------------------------------------------------------------------
44+abstract
45+data Interval : Type where
46+ MkInterval : Ptr -> Interval
47+
48+setInterval : (() -> IO ()) -> Float -> IO Interval
49+setInterval f t = do
50+ e <- mkForeign (
51+ FFun "setInterval" [FFunction FUnit (FAny (IO ())), FFloat] FPtr) f t
52+ return (MkInterval e)
53+
54+clearInterval : Interval -> IO ()
55+clearInterval (MkInterval p) =
56+ mkForeign (FFun "clearInterval" [FPtr] FUnit) p
57+
58+--------------------------------------------------------------------------------
59+-- Timeouts
60+--------------------------------------------------------------------------------
61+data Timeout : Type where
62+ MkTimeout : Ptr -> Timeout
63+
64+setTimeout : (() -> IO ()) -> Float -> IO Timeout
65+setTimeout f t = do
66+ e <- mkForeign (
67+ FFun "setTimeout" [FFunction FUnit (FAny (IO ())), FFloat] FPtr) f t
68+ return (MkTimeout e)
69+
70+clearTimeout : Timeout -> IO ()
71+clearTimeout (MkTimeout p) =
72+ mkForeign (FFun "clearTimeout" [FPtr] FUnit) p
73+
74+--------------------------------------------------------------------------------
75+-- Basic IO
76+--------------------------------------------------------------------------------
77+alert : String -> IO ()
78+alert msg =
79+ mkForeign (FFun "alert" [FString] FUnit) msg
80+
81+--------------------------------------------------------------------------------
82+-- DOM
83+--------------------------------------------------------------------------------
84+query : String -> IO NodeList
85+query q = do
86+ e <- mkForeign (FFun "document.querySelectorAll" [FString] FPtr) q
87+ return (MkNodeList e)