78 in |
78 in |
79 |
79 |
80 fun linear_undo n = edit_history n (K (find_and_undo (K true))); |
80 fun linear_undo n = edit_history n (K (find_and_undo (K true))); |
81 |
81 |
82 fun undo n = edit_history n (fn st => fn hist => |
82 fun undo n = edit_history n (fn st => fn hist => |
83 find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist); |
83 find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist); |
84 |
84 |
85 fun kill () = edit_history 1 (fn st => fn hist => |
85 fun kill () = edit_history 1 (fn st => fn hist => |
86 find_and_undo |
86 find_and_undo |
87 (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist); |
87 (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist); |
88 |
88 |
89 fun kill_proof () = edit_history 1 (fn st => fn hist => |
89 fun kill_proof () = edit_history 1 (fn st => fn hist => |
90 if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist |
90 if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist |
91 else raise Toplevel.UNDEF); |
91 else raise Toplevel.UNDEF); |
92 |
92 |
93 end; |
93 end; |
94 |
94 |
95 |
95 |
100 NONE => false |
100 NONE => false |
101 | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true) |
101 | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true) |
102 | SOME (st', NONE) => |
102 | SOME (st', NONE) => |
103 let |
103 let |
104 val name = Toplevel.name_of tr; |
104 val name = Toplevel.name_of tr; |
105 val _ = if OuterKeyword.is_theory_begin name then init () else (); |
105 val _ = if Keyword.is_theory_begin name then init () else (); |
106 val _ = |
106 val _ = |
107 if OuterKeyword.is_regular name |
107 if Keyword.is_regular name |
108 then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else (); |
108 then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else (); |
109 in true end); |
109 in true end); |
110 |
110 |
111 fun op >>> [] = () |
111 fun op >>> [] = () |
112 | op >>> (tr :: trs) = if op >> tr then op >>> trs else (); |
112 | op >>> (tr :: trs) = if op >> tr then op >>> trs else (); |
155 |
155 |
156 (** command syntax **) |
156 (** command syntax **) |
157 |
157 |
158 local |
158 local |
159 |
159 |
160 structure P = OuterParse and K = OuterKeyword; |
|
161 val op >> = Scan.>>; |
160 val op >> = Scan.>>; |
162 |
161 |
163 in |
162 in |
164 |
163 |
165 (* global history *) |
164 (* global history *) |
166 |
165 |
167 val _ = |
166 val _ = |
168 OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control |
167 OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control |
169 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init)); |
168 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init)); |
170 |
169 |
171 val _ = |
170 val _ = |
172 OuterSyntax.improper_command "linear_undo" "undo commands" K.control |
171 OuterSyntax.improper_command "linear_undo" "undo commands" Keyword.control |
173 (Scan.optional P.nat 1 >> |
172 (Scan.optional Parse.nat 1 >> |
174 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n))); |
173 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n))); |
175 |
174 |
176 val _ = |
175 val _ = |
177 OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control |
176 OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control |
178 (Scan.optional P.nat 1 >> |
177 (Scan.optional Parse.nat 1 >> |
179 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n))); |
178 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n))); |
180 |
179 |
181 val _ = |
180 val _ = |
182 OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control |
181 OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" |
183 (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o |
182 Keyword.control |
|
183 (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o |
184 Toplevel.keep (fn state => |
184 Toplevel.keep (fn state => |
185 if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF))); |
185 if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF))); |
186 |
186 |
187 val _ = |
187 val _ = |
188 OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control |
188 OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" |
189 (P.name >> |
189 Keyword.control |
|
190 (Parse.name >> |
190 (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1) |
191 (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1) |
191 | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)))); |
192 | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)))); |
192 |
193 |
193 val _ = |
194 val _ = |
194 OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control |
195 OuterSyntax.improper_command "kill" "kill partial proof or theory development" Keyword.control |
195 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill)); |
196 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill)); |
196 |
197 |
197 end; |
198 end; |
198 |
199 |
199 end; |
200 end; |