-
Notifications
You must be signed in to change notification settings - Fork 8
/
undo.t
112 lines (81 loc) · 1.53 KB
/
undo.t
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
Undo single command
$ cat >undo.ny <<EOF
> axiom A:Type
> axiom a:A
> echo a
> undo 1
> echo a
> EOF
$ narya -v -fake-interact undo.ny
→ info[I0001]
○ axiom A assumed
→ info[I0001]
○ axiom a assumed
a
: A
→ info[I0006]
○ 1 command undone
→ error[E0300]
■ undo.ny
5 | echo a
^ unbound variable: a
Undo multiple commands
$ cat >undo2.ny <<EOF
> axiom A:Type
> axiom a:A
> axiom b:A
> echo a
> undo 2
> echo a
> EOF
$ narya -v -fake-interact undo2.ny
→ info[I0001]
○ axiom A assumed
→ info[I0001]
○ axiom a assumed
→ info[I0001]
○ axiom b assumed
a
: A
→ info[I0006]
○ 2 commands undone
→ error[E0300]
■ undo2.ny
6 | echo a
^ unbound variable: a
Undo nothing
$ cat >no-undo.ny <<EOF
> undo 1
> EOF
$ narya -v -fake-interact no-undo.ny
→ error[E2500]
○ not enough commands to undo
Undo notations
$ cat >undo-notn.ny <<EOF
> axiom A:Type
> axiom a:A
> axiom f : A -> A -> A
> notation 1 f : x "+" y := f x y
> echo a + a
> undo 1
> echo a + a
> EOF
$ narya -v -fake-interact undo-notn.ny
→ info[I0001]
○ axiom A assumed
→ info[I0001]
○ axiom a assumed
→ info[I0001]
○ axiom f assumed
→ info[I0002]
○ notation f defined
a + a
: A
→ info[I0006]
○ 1 command undone
a
: A
→ error[E0200]
■ undo-notn.ny
7 | echo a + a
^ parse error