(* 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" ^ 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 ()