(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Preferences

class command_window name coqtop coqops router =
  let frame = Wg_Detachable.detachable
    ~title:(Printf.sprintf "Query pane (%s)" name) () in
  let _ = frame#hide in
  let _ = GtkData.AccelGroup.create () in
  let notebook =
    GPack.notebook ~height:200 ~scrollable:true ~packing:frame#add () in
  let _ = frame#connect#attached ~callback:(fun _ ->
    notebook#misc#set_size_request ~height:200 ()) in
  let _ = frame#connect#detached ~callback:(fun _ ->
    notebook#misc#set_size_request ~width:600 ~height:500 ();
    notebook#misc#grab_focus ()) in

  let route_id =
    let r = ref 0 in
    fun () -> incr r; !r in

object(self)
  val frame = frame

  val notebook = notebook

  (* We need access to coqops in order to place queries in the proper
     document stint. This should remove access from this module to the
     low-level Coq one. *)
  val coqops = coqops

  method pack_in (f : GObj.widget -> unit) = f frame#coerce

  val mutable new_page : GObj.widget = (GMisc.label ())#coerce

  val mutable views = []

  method private new_page_maker =
    let page = notebook#append_page
      (GMisc.label ~text:"No query" ())#coerce in
    let page = notebook#get_nth_page page in
    let b = GButton.button () in
    b#add (Ideutils.stock_to_widget ~size:(`CUSTOM(12,12)) `NEW);
    ignore(b#connect#clicked ~callback:self#new_query);
    notebook#set_page ~tab_label:b#coerce page;
    new_page <- page

  method new_query ?command ?term () = self#new_query_aux ?command ?term ()

  method private new_query_aux ?command ?term ?(grab_now=true) () =
    let frame = GBin.frame ~shadow_type:`NONE () in
    ignore(notebook#insert_page ~pos:(notebook#page_num new_page) frame#coerce);
    let route_id = route_id () in
    let new_tab_lbl text =
      let hbox = GPack.hbox ~homogeneous:false () in
      ignore(GMisc.label ~width:100 ~ellipsize:`END ~text ~packing:hbox#pack());
      let b = GButton.button ~packing:hbox#pack () in
      ignore(b#connect#clicked ~callback:(fun () ->
        router#delete_route route_id;
        views <-
          List.filter (fun (f,_,_) -> f#get_oid <> frame#coerce#get_oid) views;
        notebook#remove_page (notebook#page_num frame#coerce)));
      b#add (Ideutils.stock_to_widget ~size:(`CUSTOM(12,10)) `CLOSE);
      hbox#coerce in
    notebook#set_page ~tab_label:(new_tab_lbl "New query") frame#coerce;
    notebook#goto_page (notebook#page_num frame#coerce);
    let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
    let combo, entry, ok_b =
      let bar =
        GButton.toolbar ~style:`ICONS ~packing:(vbox#pack ~expand:false) () in
      let bar_add ~expand w =
        let item = GButton.tool_item ~expand () in
        item#add w#coerce;
        bar#insert item in
      let combo, _ =
        GEdit.combo_box_entry_text ~strings:Coq_commands.state_preserving () in
      combo#entry#set_text "Search";
      let entry = GEdit.entry () in
      entry#misc#set_can_default true;
      let ok_b = GButton.button () in
      ok_b#add (Ideutils.stock_to_widget `OK);
      bar_add ~expand:false combo;
      bar_add ~expand:true entry;
      bar_add ~expand:false ok_b;
      combo, entry, ok_b in
    let r_bin =
      GBin.scrolled_window
	~vpolicy:`AUTOMATIC
	~hpolicy:`AUTOMATIC
	~packing:(vbox#pack ~fill:true ~expand:true) () in
    let result = Wg_MessageView.message_view () in
    router#register_route route_id result;
    r_bin#add_with_viewport (result :> GObj.widget);
    views <- (frame#coerce, result, combo#entry) :: views;
    let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
    let _ = background_color#connect#changed ~callback:cb in
    let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
    let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
    stick text_font result cb;
    result#misc#set_can_focus true; (* false causes problems for selection *)
    let callback () =
      let com = combo#entry#text in
      let arg = entry#text in
      if Str.string_match (Str.regexp "^ *$") (com^arg) 0 then () else
      let phrase =
        if Str.string_match (Str.regexp "\\. *$") com 0 then com
        else com ^ " " ^ arg ^" . "
      in
      let process =
        let next = function
        | Interface.Fail (_, _, err) ->
            let err = Ideutils.validate err in
            result#set err;
            notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
            Coq.return ()
        | Interface.Good () ->
            notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
            Coq.return ()
        in
        coqops#raw_coq_query ~route_id ~next phrase
      in
      result#set (Pp.str ("Result for command " ^ phrase ^ ":\n"));
      Coq.try_grab coqtop process ignore
    in
    ignore (combo#entry#connect#activate ~callback);
    ignore (ok_b#connect#clicked ~callback);
    begin match command with
      | None -> ()
      | Some c -> combo#entry#set_text c
    end;
    begin match term with
      | None -> ()
      | Some t -> entry#set_text t
    end;
    combo#entry#misc#grab_focus ();
    if grab_now then entry#misc#grab_default ();
    ignore (entry#connect#activate ~callback);
    ignore (combo#entry#connect#activate ~callback);
    ignore (combo#entry#event#connect#key_press ~callback:(fun ev ->
      if GdkEvent.Key.keyval ev = GdkKeysyms._Tab then
        (entry#misc#grab_focus ();true)
      else false))

  method show =
    frame#show;
    let cur_page = notebook#get_nth_page notebook#current_page in
    match List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views with
    | (_, _, e) -> e#misc#grab_focus ()
    | exception Not_found -> ()

  method hide =
    frame#hide

  method visible =
    frame#visible

  method private refresh_color clr =
    let clr = Tags.color_of_string clr in
    let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in
    List.iter iter views

  initializer
    self#new_page_maker;
    self#new_query_aux ~grab_now:false ();
    frame#misc#hide ();
    let _ = background_color#connect#changed ~callback:self#refresh_color in
    self#refresh_color background_color#get;
    ignore(notebook#event#connect#key_press ~callback:(fun ev ->
      if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true)
      else false
    ));

end