abd5f0c · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -6,6 +6,7 @@ New in 0.9.13:

6* Command line option -e (or --eval) to evaluate expressions without loading the

7 REPL. This is useful for writing more portable tests.

8* Many more of the basic functions and datatypes are documented.

9+* Removed javascript lib in favor of idris-hackers/iQuery

9

10

10Internal changes

11Internal changes

11

12

idris.cabal−5

@@ -103,11 +103,6 @@ Extra-source-files:

103 libs/oldeffects/Effect/*.idr

104 libs/oldeffects/*.idr

105

106− libs/javascript/*.idr

107− libs/javascript/JavaScript/*.idr

108− libs/javascript/Makefile

109− libs/javascript/javascript.ipkg

110−

111 llvm/*.c

106 llvm/*.c

112 llvm/Makefile

107 llvm/Makefile

113

108

libs/Makefile−3

@@ -2,19 +2,16 @@ build:

2 $(MAKE) -C prelude build

3 $(MAKE) -C base build

4 $(MAKE) -C effects build

5− $(MAKE) -C javascript build

6

5

7

6

8install:

7install:

9 $(MAKE) -C prelude install

8 $(MAKE) -C prelude install

10 $(MAKE) -C base install

9 $(MAKE) -C base install

11 $(MAKE) -C effects install

10 $(MAKE) -C effects install

12− $(MAKE) -C javascript install

13

11

14clean:

12clean:

15 $(MAKE) -C prelude clean

13 $(MAKE) -C prelude clean

16 $(MAKE) -C base clean

14 $(MAKE) -C base clean

17 $(MAKE) -C effects clean

15 $(MAKE) -C effects clean

18− $(MAKE) -C javascript clean

19

16

20.PHONY: build install clean

17.PHONY: build install clean

libs/javascript/JavaScript.idrdeleted−104

@@ -1,104 +0,0 @@

1−module JavaScript

2−

3−%access public

4−

5−private

6−isUndefined : Ptr -> IO Bool

7−isUndefined p = do

8− res <- mkForeign (

9− FFun "%0 === undefined" [FPtr] FString) p

10− if res == "false"

11− then (return False)

12− else (return True)

13−

14−--------------------------------------------------------------------------------

15−-- Events

16−--------------------------------------------------------------------------------

17−abstract

18−data Event : Type where

19− MkEvent : Ptr -> Event

20−

21−--------------------------------------------------------------------------------

22−-- Elements

23−--------------------------------------------------------------------------------

24−abstract

25−data Element : Type where

26− MkElem : Ptr -> Element

27−

28−setText : Element -> String -> IO ()

29−setText (MkElem p) s =

30− mkForeign (FFun "%0.textContent=%1" [FPtr, FString] FUnit) p s

31−

32−

33−setOnClick : Element -> (Event -> IO Bool) -> IO ()

34−setOnClick (MkElem e) f =

35− mkForeign (

36− FFun "%0['onclick']=%1" [ FPtr

37− , FFunction (FAny Event) (FAny (IO Bool))

38− ] FUnit) e f

39−--------------------------------------------------------------------------------

40−-- Nodelists

41−--------------------------------------------------------------------------------

42−abstract

43−data NodeList : Type where

44− MkNodeList : Ptr -> NodeList

45−

46−elemAt : NodeList -> Nat -> IO (Maybe Element)

47−elemAt (MkNodeList p) i = do

48− e <- mkForeign (FFun "%0.item(%1)" [FPtr, FInt] FPtr) p (

49− prim__truncBigInt_Int (cast i)

50− )

51− d <- isUndefined e

52− if d

53− then return $ Just (MkElem e)

54− else return Nothing

55−

56−--------------------------------------------------------------------------------

57−-- Intervals

58−--------------------------------------------------------------------------------

59−abstract

60−data Interval : Type where

61− MkInterval : Ptr -> Interval

62−

63−setInterval : (() -> IO ()) -> Float -> IO Interval

64−setInterval f t = do

65− e <- mkForeign (

66− FFun "setInterval(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr

67− ) f t

68− return (MkInterval e)

69−

70−clearInterval : Interval -> IO ()

71−clearInterval (MkInterval p) =

72− mkForeign (FFun "clearInterval(%0)" [FPtr] FUnit) p

73−

74−--------------------------------------------------------------------------------

75−-- Timeouts

76−--------------------------------------------------------------------------------

77−data Timeout : Type where

78− MkTimeout : Ptr -> Timeout

79−

80−setTimeout : (() -> IO ()) -> Float -> IO Timeout

81−setTimeout f t = do

82− e <- mkForeign (

83− FFun "setTimeout(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr

84− ) f t

85− return (MkTimeout e)

86−

87−clearTimeout : Timeout -> IO ()

88−clearTimeout (MkTimeout p) =

89− mkForeign (FFun "clearTimeout(%0)" [FPtr] FUnit) p

90−

91−--------------------------------------------------------------------------------

92−-- Basic IO

93−--------------------------------------------------------------------------------

94−alert : String -> IO ()

95−alert msg =

96− mkForeign (FFun "alert(%0)" [FString] FUnit) msg

97−

98−--------------------------------------------------------------------------------

99−-- DOM

100−--------------------------------------------------------------------------------

101−query : String -> IO NodeList

102−query q = do

103− e <- mkForeign (FFun "document.querySelectorAll(%0)" [FString] FPtr) q

104− return (MkNodeList e)

libs/javascript/JavaScript/JSON.idrdeleted−44

@@ -1,44 +0,0 @@

1−module JSON

2−

3−import Data.SortedMap

4−

5−data JSONType : Type where

6− JSONArray : (n : Nat) -> Vect n JSONType -> JSONType

7− JSONString : JSONType

8− JSONNumber : JSONType

9− JSONBool : JSONType

10− JSONObject : SortedMap String JSONType -> JSONType

11− JSONNull : JSONType

12−

13−mutual

14− using (ts : Vect n JSONType, fs : SortedMap String JSONType)

15− namespace JArray

16− data JArray : (n : Nat) -> Vect n JSONType -> Type where

17− Nil : JArray 0 []

18− (::) : JSON t -> JArray n ts -> JArray (S n) (t :: ts)

19−

20− namespace JObject

21− data JObject : SortedMap String JSONType -> Type where

22− Nil : JObject empty

23− (::) : (f : (String, JSON t)) ->

24− JObject fs ->

25− JObject (insert (fst f) t fs)

26−

27− data JSON : JSONType -> Type where

28− JSString : String -> JSON JSONString

29− JSNumber : Float -> JSON JSONNumber

30− JSBool : Bool -> JSON JSONBool

31− JSNull : JSON JSONNull

32− JSArray : JArray n ts -> JSON (JSONArray n ts)

33− JSObject : JObject fs -> JSON (JSONObject fs)

34−

35−index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)

36−index fZ (JSArray (x :: xs)) = x

37−index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)

38−

39−(++) : JSON (JSONArray m ts1) ->

40− JSON (JSONArray n ts2) ->

41− JSON (JSONArray (m + n) (ts1 ++ ts2))

42−(++) (JSArray []) ys = ys

43−(++) (JSArray (x :: xs)) ys with ((JSArray xs) ++ ys)

44− | (JSArray as) = JSArray (x :: as)

libs/javascript/Makefiledeleted−14

@@ -1,14 +0,0 @@

1−IDRIS := idris

2−

3−build:

4− $(IDRIS) --build javascript.ipkg

5−

6−install:

7− $(IDRIS) --install javascript.ipkg

8−

9−clean:

10− $(IDRIS) --clean javascript.ipkg

11−

12−rebuild: clean build

13−

14−.PHONY: build install clean rebuild

libs/javascript/javascript.ipkgdeleted−5

@@ -1,5 +0,0 @@

1−package javascript

2−

3−opts = "--nobasepkgs -i ../prelude -i ../base"

4−modules = JavaScript, JavaScript.JSON

5−