annotate lib/ur/option.ur @ 2142:3288e3c9948b
Fix XML indentation in Emacs mode
The return value of MATCH-STRING is a string. At least on Emacs 25,
the comparisons between string and character with EQUAL could never
succeed, and so the cases for matching braces were never triggered.
GET-TEXT-PROPERTY may return a list rather than an atom (for example,
on long lines with whitespace-mode turned on), and this broke the
heuristic of looking for the tag face in previous text.
| author |
Julian Squires <julian@cipht.net> |
| date |
Mon, 04 May 2015 14:35:07 -0400 |
| parents |
36428d853c97 |
| children |
|
| rev |
line source |
|
adamc@841
|
1 datatype t = datatype Basis.option
|
|
adamc@841
|
2
|
|
adam@1544
|
3 val monad = mkMonad {Return = @@Some,
|
|
adam@1544
|
4 Bind = fn [a] [b] (m1 : t a) (m2 : a -> t b) =>
|
|
adam@1544
|
5 case m1 of
|
|
adam@1544
|
6 None => None
|
|
adam@1544
|
7 | Some v => m2 v}
|
|
adam@1544
|
8
|
|
adamc@846
|
9 fun eq [a] (_ : eq a) =
|
|
adamc@846
|
10 mkEq (fn x y =>
|
|
adamc@846
|
11 case (x, y) of
|
|
adamc@846
|
12 (None, None) => True
|
|
adamc@846
|
13 | (Some x, Some y) => x = y
|
|
adamc@846
|
14 | _ => False)
|
|
adamc@846
|
15
|
|
adamc@961
|
16 fun ord [a] (_ : ord a) =
|
|
adamc@961
|
17 mkOrd {Lt = fn x y =>
|
|
adamc@961
|
18 case (x, y) of
|
|
adamc@961
|
19 (None, Some _) => True
|
|
adamc@961
|
20 | (Some x, Some y) => x < y
|
|
adamc@961
|
21 | _ => False,
|
|
adamc@961
|
22 Le = fn x y =>
|
|
adamc@961
|
23 case (x, y) of
|
|
adamc@961
|
24 (None, _) => True
|
|
adamc@961
|
25 | (Some x, Some y) => x <= y
|
|
adamc@961
|
26 | _ => False}
|
|
adamc@961
|
27
|
|
adamc@944
|
28 fun isNone [a] x =
|
|
adamc@944
|
29 case x of
|
|
adamc@944
|
30 None => True
|
|
adamc@944
|
31 | Some _ => False
|
|
adamc@944
|
32
|
|
adamc@841
|
33 fun isSome [a] x =
|
|
adamc@841
|
34 case x of
|
|
adamc@841
|
35 None => False
|
|
adamc@841
|
36 | Some _ => True
|
|
adamc@844
|
37
|
|
adamc@844
|
38 fun mp [a] [b] f x =
|
|
adamc@844
|
39 case x of
|
|
adamc@844
|
40 None => None
|
|
adamc@844
|
41 | Some y => Some (f y)
|
|
adamc@846
|
42
|
|
adamc@846
|
43 fun bind [a] [b] f x =
|
|
adamc@846
|
44 case x of
|
|
adamc@846
|
45 None => None
|
|
adamc@846
|
46 | Some y => f y
|
|
adamc@1068
|
47
|
|
adamc@1068
|
48 fun get [a] (x : a) (o : option a) =
|
|
adamc@1068
|
49 case o of
|
|
adamc@1068
|
50 None => x
|
|
adamc@1068
|
51 | Some v => v
|
|
mad@1831
|
52
|
|
mad@1831
|
53 fun unsafeGet [a] (o : option a) =
|
|
mad@1831
|
54 case o of
|
|
mad@1831
|
55 None => error <xml>Option.unsafeGet: encountered None</xml>
|
|
mad@1831
|
56 | Some v => v
|
