blob: 7df69ba5d898fbd7a54642435982acbd7d4bae5d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
abstract Editor = {
cat Adjective ;
Noun ;
Verb ;
Determiner ;
Sentence ;
fun Available : Adjective ;
Next : Adjective ;
Previous : Adjective ;
fun Bulgarian : Noun ;
Danish : Noun ;
English : Noun ;
Finnish : Noun ;
French : Noun ;
German : Noun ;
Italian : Noun ;
Norwegian : Noun ;
Russian : Noun ;
Spanish : Noun ;
Swedish : Noun ;
fun Float_N : Noun ;
Integer_N : Noun ;
String_N : Noun ;
Language : Noun ;
Node : Noun ;
Page : Noun ;
Refinement : Noun ;
Tree : Noun ;
Wrapper : Noun ;
fun Copy : Verb ;
Cut : Verb ;
Delete : Verb ;
Enter : Verb ;
Parse : Verb ;
Paste : Verb ;
Redo : Verb ;
Refine : Verb ;
Replace : Verb ;
Select : Verb ;
Show : Verb ;
Undo : Verb ;
Wrap : Verb ;
fun DefPlDet : Determiner ;
DefSgDet : Determiner ;
IndefPlDet : Determiner ;
IndefSgDet : Determiner ;
fun Command : Verb -> Determiner -> Noun -> Sentence ;
CommandAdj : Verb -> Determiner -> Adjective -> Noun -> Sentence ;
ErrorMessage : Adjective -> Noun -> Sentence ;
Label : Noun -> Sentence ;
RandomlyCommand : Verb -> Determiner -> Noun -> Sentence ;
SingleWordCommand : Verb -> Sentence ;
}
|
