helm/matita/matitaScript.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   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.
   6  *
   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.
  11  *
  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.
  16  *
  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,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 open MatitaTypes
  29
  30 exception Script_failure of string
  31
  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
  36   List.iter
  37     (* TODO ZACK remove xml files from disk *)
  38     (fun suffix -> Http_getter.unregister (uri ^ suffix))
  39     [""; ".body"; ".types"]
  40
  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;
  45   List.iter
  46     (fun suffix ->
  47       let uri =
  48         Pcre.replace ~pat:"\\.ind$" ~templ:(sprintf "_%s.con" suffix) uri
  49       in
  50       remove_constant_from_world ~dbd ~uri:(UriManager.uri_of_string uri))
  51     ["ind"; "rec"; "rect"]
  52
  53 let is_empty =
  54   let rex = Pcre.regexp "^\\s*$" in
  55   fun s ->
  56     Pcre.pmatch ~rex s
  57
  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
  64     | None -> ()
  65     | Some item ->
  66         (match item with
  67         | `Tactic ->
  68             let res =
  69               interpreter#evalAst (TacticAst.Command (TacticAst.Undo None))
  70             in
  71             assert (fst res)
  72         | `Theorem ->
  73             interpreter#setState `Command;
  74             (MatitaMathView.sequents_viewer_instance ())#reset
  75         | `Qed uri
  76         | `Def uri -> remove_constant_from_world ~dbd ~uri
  77         | `Inductive uri -> remove_inductive_def_from_world ~dbd ~uri)
  78   in
  79   object (self)
  80     initializer
  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
  86         (w self#forward));
  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))
  90
  91     val mutable items = []
  92
  93     (** {3 text buffer locking} *)
  94
  95       (** text mark and tag representing locked part of a script *)
  96     val locked_mark =
  97       buf#create_mark ~name:"locked" ~left_gravity:true buf#start_iter
  98     val locked_tag = buf#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
  99
 100       (** lock script text view from the beginning to the given offset (in UTF-8
 101       * characters) *)
 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)
 108
 109     method win = gui#script
 110
 111     method loadFrom fname =
 112       buf#set_text (MatitaMisc.input_file fname);
 113       gui#script#scriptWin#show ();
 114       gui#main#showScriptMenuItem#set_active true
 115
 116     method advance tactical =
 117       let text = "\n" ^ TacticAstPp.pp_tactical 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));
 124       end;
 125       res
 126
 127     (** {3 script progress} *)
 128
 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) *)
 135         let success =
 136           try
 137             fst (self#_forward ~stop:cursor_iter ())
 138           with
 139           | Script_failure _ | CicTextualParser2.Parse_error _ -> false
 140         in
 141         if success && (locked_iter ())#compare cursor_iter < 0 then
 142           forward_until_cursor ()
 143       in
 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
 148           back_until_cursor ()
 149       in
 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 *)
 156         ()
 157
 158     method private top () =
 159       try while true do self#back () done with Script_failure _ -> ()
 160
 161     method private bottom () =
 162       try
 163         while true do
 164           let res = self#_forward () in
 165           if not (fst res) then raise (Script_failure "error")
 166         done
 167       with Script_failure _ -> ()
 168
 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")
 175         else
 176           interpreter#evalPhrase text
 177       in
 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
 183       end;
 184       res
 185
 186     method private forward () = ignore (self#_forward ())
 187
 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
 194         | [] -> assert false
 195       in
 196       match items with
 197       | [] -> raise (Script_failure "at top")
 198       | (item, last_offset) :: tl ->
 199           undo_item item;
 200           let (last_offset, tl) =
 201             (* if undoing a qed, go back before corresponding theorem *)
 202             match item with
 203             | Some (`Qed _) -> flush_theorem tl
 204             | _ -> last_offset, tl
 205           in
 206           items <- tl;
 207           self#lockScript last_offset
 208
 209   end
 210
 211 let script ~interpreter = new script ~interpreter ()
 212