+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MatitaTypes
+
+exception Script_failure of string
+
+let remove_constant_from_world ~dbd ~uri =
+ CicEnvironment.remove_obj uri;
+ MetadataDb.unindex ~dbd ~uri;
+ let uri = UriManager.string_of_uri uri in
+ List.iter
+ (* TODO ZACK remove xml files from disk *)
+ (fun suffix -> Http_getter.unregister (uri ^ suffix))
+ [""; ".body"; ".types"]
+
+let remove_inductive_def_from_world ~dbd ~uri =
+ remove_constant_from_world ~dbd ~uri;
+ let uri = UriManager.string_of_uri uri in
+ Http_getter.unregister uri;
+ List.iter
+ (fun suffix ->
+ let uri =
+ Pcre.replace ~pat:"\\.ind$" ~templ:(sprintf "_%s.con" suffix) uri
+ in
+ remove_constant_from_world ~dbd ~uri:(UriManager.uri_of_string uri))
+ ["ind"; "rec"; "rect"]
+
+let is_empty =
+ let rex = Pcre.regexp "^\\s*$" in
+ fun s ->
+ Pcre.pmatch ~rex s
+
+class script ~(interpreter:MatitaTypes.interpreter) () =
+ let gui = MatitaGui.instance () in
+ let script = gui#script in
+ let buf = script#scriptTextView#buffer in
+ let dbd = MatitaMisc.dbd_instance () in
+ let rec undo_item = function
+ | None -> ()
+ | Some item ->
+ (match item with
+ | `Tactic ->
+ let res =
+ interpreter#evalAst (TacticAst.Command (TacticAst.Undo None))
+ in
+ assert (fst res)
+ | `Theorem ->
+ interpreter#setState `Command;
+ (MatitaMathView.sequents_viewer_instance ())#reset
+ | `Qed uri
+ | `Def uri -> remove_constant_from_world ~dbd ~uri
+ | `Inductive uri -> remove_inductive_def_from_world ~dbd ~uri)
+ in
+ object (self)
+ initializer
+ let console = (MatitaGui.instance ())#console in
+ let w f () = ignore (console#wrap_exn (fun () -> f ())) in
+ ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top));
+ ignore (gui#script#scriptWinBottomButton#connect#clicked (w self#bottom));
+ ignore (gui#script#scriptWinForwardButton#connect#clicked
+ (w self#forward));
+ ignore (gui#script#scriptWinBackButton#connect#clicked (w self#back));
+ ignore (gui#script#scriptWinTopButton#connect#clicked (w self#top));
+ ignore (gui#script#scriptWinJumpButton#connect#clicked (w self#jump))
+
+ val mutable items = []
+
+ (** {3 text buffer locking} *)
+
+ (** text mark and tag representing locked part of a script *)
+ val locked_mark =
+ buf#create_mark ~name:"locked" ~left_gravity:true buf#start_iter
+ val locked_tag = buf#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
+
+ (** lock script text view from the beginning to the given offset (in UTF-8
+ * characters) *)
+ method private lockScript offset =
+ let mark = `MARK locked_mark in
+ buf#move_mark mark ~where:(buf#get_iter_at_char offset);
+ buf#remove_tag locked_tag ~start:buf#start_iter ~stop:buf#end_iter;
+ buf#apply_tag locked_tag ~start:buf#start_iter
+ ~stop:(buf#get_iter_at_mark mark)
+
+ method win = gui#script
+
+ method loadFrom fname =
+ buf#set_text (MatitaMisc.input_file fname);
+ gui#script#scriptWin#show ();
+ gui#main#showScriptMenuItem#set_active true
+
+ method advance tactical =
+ let text = "\n" ^ TacticAstPp.pp_tactical tactical in
+ buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) text;
+ let res = self#_forward () in
+ if not (fst res) then begin
+ let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+ buf#delete ~start:locked_iter
+ ~stop:(locked_iter#forward_chars (String.length text));
+ end;
+ res
+
+ (** {3 script progress} *)
+
+ method private jump () =
+ let locked_iter () = buf#get_iter_at_mark (`NAME "locked") in
+ let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
+ let rec forward_until_cursor () =
+ prerr_endline "forward_until_cursor";
+ (* go forward until locked > cursor (or forward fails) *)
+ let success =
+ try
+ fst (self#_forward ~stop:cursor_iter ())
+ with
+ | Script_failure _ | CicTextualParser2.Parse_error _ -> false
+ in
+ if success && (locked_iter ())#compare cursor_iter < 0 then
+ forward_until_cursor ()
+ in
+ let rec back_until_cursor () = (* go backward until locked < cursor *)
+ prerr_endline "back_until_cursor";
+ let res = self#back () in
+ if (locked_iter ())#compare cursor_iter > 0 then
+ back_until_cursor ()
+ in
+ let cmp = (locked_iter ())#compare cursor_iter in
+ if cmp < 0 then (* locked < cursor *)
+ (prerr_endline "locked < cursor"; forward_until_cursor ())
+ else if cmp > 0 then (* locked > cursor *)
+ (prerr_endline "locked > cursor"; back_until_cursor ())
+ else (* cursor = locked *)
+ ()
+
+ method private top () =
+ try while true do self#back () done with Script_failure _ -> ()
+
+ method private bottom () =
+ try
+ while true do
+ let res = self#_forward () in
+ if not (fst res) then raise (Script_failure "error")
+ done
+ with Script_failure _ -> ()
+
+ method private _forward ?(stop = buf#end_iter) () =
+ let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+ let (success, hide) as res =
+ let text = buf#get_text ~start:locked_iter ~stop () in
+ if is_empty text then
+ raise (Script_failure "at bottom")
+ else
+ interpreter#evalPhrase text
+ in
+ if success then begin
+ let old_offset = locked_iter#offset in
+ let new_offset = old_offset + interpreter#endOffset in
+ self#lockScript new_offset;
+ items <- (interpreter#lastItem, old_offset) :: items
+ end;
+ res
+
+ method private forward () = ignore (self#_forward ())
+
+ method private back () =
+ (* clean history backward until the first theorem, return offset before
+ * it and remaning history *)
+ let rec flush_theorem = function
+ | (Some `Theorem, offset) :: tl -> offset, tl
+ | _ :: tl -> flush_theorem tl
+ | [] -> assert false
+ in
+ match items with
+ | [] -> raise (Script_failure "at top")
+ | (item, last_offset) :: tl ->
+ undo_item item;
+ let (last_offset, tl) =
+ (* if undoing a qed, go back before corresponding theorem *)
+ match item with
+ | Some (`Qed _) -> flush_theorem tl
+ | _ -> last_offset, tl
+ in
+ items <- tl;
+ self#lockScript last_offset
+
+ end
+
+let script ~interpreter = new script ~interpreter ()
+