1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 exception Script_failure of string
32 let remove_constant_from_world ~dbd ~uri =
33 CicEnvironment.remove_obj uri;
34 MetadataDb.unindex ~dbd ~uri;
35 let uri = UriManager.string_of_uri uri in
37 (* TODO ZACK remove xml files from disk *)
38 (fun suffix -> Http_getter.unregister (uri ^ suffix))
39 [""; ".body"; ".types"]
41 let remove_inductive_def_from_world ~dbd ~uri =
42 remove_constant_from_world ~dbd ~uri;
43 let uri = UriManager.string_of_uri uri in
44 Http_getter.unregister uri;
48 Pcre.replace ~pat:"\\.ind$" ~templ:(sprintf "_%s.con" suffix) uri
50 remove_constant_from_world ~dbd ~uri:(UriManager.uri_of_string uri))
51 ["ind"; "rec"; "rect"]
54 let rex = Pcre.regexp "^\\s*$" in
58 class script ~(interpreter:MatitaTypes.interpreter) () =
59 let gui = MatitaGui.instance () in
60 let script = gui#script in
61 let buf = script#scriptTextView#buffer in
62 let dbd = MatitaMisc.dbd_instance () in
63 let rec undo_item = function
69 interpreter#evalAst (TacticAst.Command (TacticAst.Undo None))
73 interpreter#setState `Command;
74 (MatitaMathView.sequents_viewer_instance ())#reset
76 | `Def uri -> remove_constant_from_world ~dbd ~uri
77 | `Inductive uri -> remove_inductive_def_from_world ~dbd ~uri)
81 let console = (MatitaGui.instance ())#console in
82 let w f () = ignore (console#wrap_exn (fun () -> f ())) in
83 ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top));
84 ignore (gui#script#scriptWinBottomButton#connect#clicked (w self#bottom));
85 ignore (gui#script#scriptWinForwardButton#connect#clicked
87 ignore (gui#script#scriptWinBackButton#connect#clicked (w self#back));
88 ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top));
89 ignore (gui#script#scriptWinJumpButton#connect#clicked (w self#jump))
91 val mutable items = []
93 (** {3 text buffer locking} *)
95 (** text mark and tag representing locked part of a script *)
97 buf#create_mark ~name:"locked" ~left_gravity:true buf#start_iter
98 val locked_tag = buf#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
100 (** lock script text view from the beginning to the given offset (in UTF-8
102 method private lockScript offset =
103 let mark = `MARK locked_mark in
104 buf#move_mark mark ~where:(buf#get_iter_at_char offset);
105 buf#remove_tag locked_tag ~start:buf#start_iter ~stop:buf#end_iter;
106 buf#apply_tag locked_tag ~start:buf#start_iter
107 ~stop:(buf#get_iter_at_mark mark)
109 method win = gui#script
111 method loadFrom fname =
112 buf#set_text (MatitaMisc.input_file fname);
113 gui#script#scriptWin#show ();
114 gui#main#showScriptMenuItem#set_active true
116 method advance tactical =
117 let text = "\n" ^ tactical in
118 buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) text;
119 let res = self#_forward () in
120 if not (fst res) then begin
121 let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
122 buf#delete ~start:locked_iter
123 ~stop:(locked_iter#forward_chars (String.length text));
127 (** {3 script progress} *)
129 method private jump () =
130 let locked_iter () = buf#get_iter_at_mark (`NAME "locked") in
131 let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
132 let rec forward_until_cursor () =
133 prerr_endline "forward_until_cursor";
134 (* go forward until locked > cursor (or forward fails) *)
137 fst (self#_forward ~stop:cursor_iter ())
139 | Script_failure _ | CicTextualParser2.Parse_error _ -> false
141 if success && (locked_iter ())#compare cursor_iter < 0 then
142 forward_until_cursor ()
144 let rec back_until_cursor () = (* go backward until locked < cursor *)
145 prerr_endline "back_until_cursor";
146 let res = self#back () in
147 if (locked_iter ())#compare cursor_iter > 0 then
150 let cmp = (locked_iter ())#compare cursor_iter in
151 if cmp < 0 then (* locked < cursor *)
152 (prerr_endline "locked < cursor"; forward_until_cursor ())
153 else if cmp > 0 then (* locked > cursor *)
154 (prerr_endline "locked > cursor"; back_until_cursor ())
155 else (* cursor = locked *)
158 method private top () =
159 try while true do self#back () done with Script_failure _ -> ()
161 method private bottom () =
164 let res = self#_forward () in
165 if not (fst res) then raise (Script_failure "error")
167 with Script_failure _ -> ()
169 method private _forward ?(stop = buf#end_iter) () =
170 let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
171 let (success, hide) as res =
172 let text = buf#get_text ~start:locked_iter ~stop () in
173 if is_empty text then
174 raise (Script_failure "at bottom")
176 interpreter#evalPhrase text
178 if success then begin
179 let old_offset = locked_iter#offset in
180 let new_offset = old_offset + interpreter#endOffset in
181 self#lockScript new_offset;
182 items <- (interpreter#lastItem, old_offset) :: items
186 method private forward () = ignore (self#_forward ())
188 method private back () =
189 (* clean history backward until the first theorem, return offset before
190 * it and remaning history *)
191 let rec flush_theorem = function
192 | (Some `Theorem, offset) :: tl -> offset, tl
193 | _ :: tl -> flush_theorem tl
197 | [] -> raise (Script_failure "at top")
198 | (item, last_offset) :: tl ->
200 let (last_offset, tl) =
201 (* if undoing a qed, go back before corresponding theorem *)
203 | Some (`Qed _) -> flush_theorem tl
204 | _ -> last_offset, tl
207 self#lockScript last_offset
211 let script ~interpreter = new script ~interpreter ()