git.iko.soy/Idris-dev
on 6dc5ea2 help sign in
Idris-dev/javascript/JavaScript.idr
101 lines 3.3 kB history raw
1module JavaScript
3%access public
5-- TODO: Get rid of this hack, and find a better way.
6private
7isUndefined : Ptr -> IO Bool
8isUndefined p = do
9 res <- mkForeign (
10 FFun "(function(arg) { return arg === undefined;})" [FPtr] FString) p
11 if res == "false"
12 then (return False)
13 else (return True)
15--------------------------------------------------------------------------------
16-- Events
17--------------------------------------------------------------------------------
18abstract
19data Event : Type where
20 MkEvent : Ptr -> Event
22--------------------------------------------------------------------------------
23-- Elements
24--------------------------------------------------------------------------------
25abstract
26data Element : Type where
27 MkElem : Ptr -> Element
29setText : Element -> String -> IO ()
30setText (MkElem p) s =
31 mkForeign (FFun ".textContent=" [FPtr, FString] FUnit) p s
34setOnClick : Element -> (Event -> IO Bool) -> IO ()
35setOnClick (MkElem e) f =
36 mkForeign (
37 FFun "['onclick']=" [ FPtr
38 , FFunction (FAny Event) (FAny (IO Bool))
39 ] FUnit) e f
40--------------------------------------------------------------------------------
41-- Nodelists
42--------------------------------------------------------------------------------
43abstract
44data NodeList : Type where
45 MkNodeList : Ptr -> NodeList
47elemAt : NodeList -> Nat -> IO (Maybe Element)
48elemAt (MkNodeList p) i = do
49 e <- mkForeign (FFun ".item" [FPtr, FInt] FPtr) p (prim__truncBigInt_Int (cast i))
50 d <- isUndefined e
51 if d
52 then return $ Just (MkElem e)
53 else return Nothing
55--------------------------------------------------------------------------------
56-- Intervals
57--------------------------------------------------------------------------------
58abstract
59data Interval : Type where
60 MkInterval : Ptr -> Interval
62setInterval : (() -> IO ()) -> Float -> IO Interval
63setInterval f t = do
64 e <- mkForeign (
65 FFun "setInterval" [FFunction FUnit (FAny (IO ())), FFloat] FPtr) f t
66 return (MkInterval e)
68clearInterval : Interval -> IO ()
69clearInterval (MkInterval p) =
70 mkForeign (FFun "clearInterval" [FPtr] FUnit) p
72--------------------------------------------------------------------------------
73-- Timeouts
74--------------------------------------------------------------------------------
75data Timeout : Type where
76 MkTimeout : Ptr -> Timeout
78setTimeout : (() -> IO ()) -> Float -> IO Timeout
79setTimeout f t = do
80 e <- mkForeign (
81 FFun "setTimeout" [FFunction FUnit (FAny (IO ())), FFloat] FPtr) f t
82 return (MkTimeout e)
84clearTimeout : Timeout -> IO ()
85clearTimeout (MkTimeout p) =
86 mkForeign (FFun "clearTimeout" [FPtr] FUnit) p
88--------------------------------------------------------------------------------
89-- Basic IO
90--------------------------------------------------------------------------------
91alert : String -> IO ()
92alert msg =
93 mkForeign (FFun "alert" [FString] FUnit) msg
95--------------------------------------------------------------------------------
96-- DOM
97--------------------------------------------------------------------------------
98query : String -> IO NodeList
99query q = do
100 e <- mkForeign (FFun "document.querySelectorAll" [FString] FPtr) q
101 return (MkNodeList e)