<commit_before>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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

(** A session is a script buffer + proof + messages,
    interacting with a coqtop, and a few other elements around *)

class type ['a] page =
  object
    inherit GObj.widget
    method update : 'a -> unit
    method on_update : callback:('a -> unit) -> unit
    method data : 'a
  end

class type control =
  object
    method detach : unit -> unit
  end

type errpage = (int * string) list page
type jobpage = string CString.Map.t page
type breakpoint = {
  mark_id : string;
  mutable prev_byte_offset : int; (* UTF-8 byte offset for Coq *)
  (* prev_uni_offset may differ from mark#offset as the script is edited *)
  mutable prev_uni_offset : int;  (* unicode offset for GTK *)
}

type session = {
  buffer : GText.buffer;
  script : Wg_ScriptView.script_view;
  proof : Wg_ProofView.proof_view;   (* the proof context panel *)
  messages : Wg_RoutedMessageViews.message_views_router;
  segment : Wg_Segment.segment; (* color coded status bar near bottom of the screen *)
  fileops : FileOps.ops;
  coqops : CoqOps.ops;
  coqtop : Coq.coqtop;
  command : Wg_Command.command_window; (* aka the Query Pane *)
  finder : Wg_Find.finder; (* Find / Replace panel *)
  debugger : Wg_Debugger.debugger_view;
  tab_label : GMisc.label;
  errpage : errpage;
  jobpage : jobpage;
  sid : int;
  basename : string;
  mutable control : control;
  mutable abs_file_name : string option;
  mutable debug_stop_pt : (session * int * int) option;
  mutable breakpoints : breakpoint list;
  mutable last_db_goals : Pp.t
}

let next_sid = ref 0

let create_buffer () =
  let buffer = GSourceView3.source_buffer
    ~tag_table:Tags.Script.table
    ~highlight_matching_brackets:true
    ?language:(lang_manager#language source_language#get)
    ?style_scheme:(style_manager#style_scheme source_style#get)
    ()
  in
  let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in
  let _ = buffer#create_mark
    ~left_gravity:false ~name:"stop_of_input" buffer#end_iter in
  let _ = buffer#create_mark ~name:"prev_insert" buffer#start_iter in
  let _ = buffer#place_cursor ~where:buffer#start_iter in
  let _ = buffer#add_selection_clipboard Ideutils.cb in
  buffer

let create_script coqtop source_buffer =
  let script = Wg_ScriptView.script_view coqtop ~source_buffer
    ~show_line_numbers:true ~wrap_mode:`NONE ()
    (* todo: line numbers don't appear *)
  in
  let _ = script#misc#set_name "ScriptWindow"
  in
  script

(** NB: Events during text edition:

    - [begin_user_action]
    - [insert_text] (or [delete_range] when deleting)
    - [changed]
    - [end_user_action]

   When pasting a text containing tags (e.g. the sentence terminators),
   there is actually many [insert_text] and [changed]. For instance,
   for "a. b.":

    - [begin_user_action]
    - [insert_text] (for "a")
    - [changed]
    - [insert_text] (for ".")
    - [changed]
    - [apply_tag] (for the tag of ".")
    - [insert_text] (for " b")
    - [changed]
    - [insert_text] (for ".")
    - [changed]
    - [apply_tag] (for the tag of ".")
    - [end_user_action]

  Since these copy-pasted tags may interact badly with the retag mechanism,
  we now don't monitor the "changed" event, but rather the "begin_user_action"
  and "end_user_action". We begin by setting a mark at the initial cursor
  point. At the end, the zone between the mark and the cursor is to be
  untagged and then retagged. *)

let misc () = CDebug.(get_flag misc)

type action_stack = Gtk.text_mark list option

let call_coq_or_cancel_action coqtop coqops (buffer : GText.buffer) it =
  let () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in
  let mark = buffer#create_mark ~name:"target" it in
  let action = coqops#go_to_mark (`MARK mark) in
  ignore @@ Coq.try_grab coqtop action (fun () -> ())

let init_user_action (stack : action_stack ref) = match !stack with
| None -> stack := Some []
| Some _ -> assert false

let close_user_action (stack : action_stack ref) = match !stack with
| None -> assert false
| Some marks ->
  let () = stack := None in
  marks

let handle_iter coqtop coqops (buffer : GText.buffer) it stack = match it with
| None -> ()
| Some it ->
  match !stack with
  | Some marks ->
    (* We are inside an user action, deferring to its end *)
    let mark = buffer#create_mark it in
    stack := Some (mark :: marks)
  | None ->
    (* Otherwise we move to the mark now *)
    call_coq_or_cancel_action coqtop coqops buffer it

let set_buffer_handlers
  (buffer : GText.buffer) script (coqops : CoqOps.ops) coqtop
=
  let action_stack = ref None in
  let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
  let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in
  let ensure_marks_exist () =
    try ignore(buffer#get_mark (`NAME "stop_of_input"))
    with GText.No_such_mark _ -> assert false in
  let get_insert () = buffer#get_iter_at_mark `INSERT in
  let update_prev it =
    let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
    if it#offset < prev#offset then
      buffer#move_mark (`NAME "prev_insert") ~where:it
  in
  let debug_edit_zone () = if false (*!Minilib.debug*) then begin
    buffer#remove_tag Tags.Script.edit_zone
      ~start:buffer#start_iter ~stop:buffer#end_iter;
    buffer#apply_tag Tags.Script.edit_zone
      ~start:(get_start()) ~stop:(get_stop())
    end in
  let processed_sentence_just_before_error it =
    let rec aux old it =
      if it#is_start then None
      else if it#has_tag Tags.Script.processed then Some old
      else if it#has_tag Tags.Script.error_bg then aux it it#backward_char
      else None in
    aux it it#copy in
  let insert_cb it s = if String.length s = 0 then () else begin
    if misc () then Minilib.log ("insert_cb " ^ string_of_int it#offset);
    let () = update_prev it in
    let iter =
      if it#has_tag Tags.Script.processed then Some it
      else if it#has_tag Tags.Script.error_bg then
        processed_sentence_just_before_error it
      else None
    in
    handle_iter coqtop coqops buffer iter action_stack
    end
  in
  let delete_cb ~start ~stop =
    if misc () then Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
    let min_iter, max_iter =
      if start#compare stop < 0 then start, stop else stop, start in
    let () = update_prev min_iter in
    let rec aux iter =
      if iter#equal max_iter then None
      else if iter#has_tag Tags.Script.processed then
        Some min_iter
      else if iter#has_tag Tags.Script.error_bg then
        processed_sentence_just_before_error iter
      else aux iter#forward_char
    in
    let iter = aux min_iter in
    handle_iter coqtop coqops buffer iter action_stack
  in
  let begin_action_cb () =
    let () = if misc () then Minilib.log "begin_action_cb" in
    let () = init_user_action action_stack in
    let where = get_insert () in
    buffer#move_mark (`NAME "prev_insert") ~where
  in
  let end_action_cb () =
    let () = if misc () then Minilib.log "end_action_cb" in
    let marks = close_user_action action_stack in
    let () = ensure_marks_exist () in
    if CList.is_empty marks then
      let start, stop = get_start (), get_stop () in
      let () = List.iter (fun tag -> buffer#remove_tag tag ~start ~stop) Tags.Script.ephemere in<commit_msg>Handle deletion of end of sentence char correctly<commit_after>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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

(** A session is a script buffer + proof + messages,
    interacting with a coqtop, and a few other elements around *)

class type ['a] page =
  object
    inherit GObj.widget
    method update : 'a -> unit
    method on_update : callback:('a -> unit) -> unit
    method data : 'a
  end

class type control =
  object
    method detach : unit -> unit
  end

type errpage = (int * string) list page
type jobpage = string CString.Map.t page
type breakpoint = {
  mark_id : string;
  mutable prev_byte_offset : int; (* UTF-8 byte offset for Coq *)
  (* prev_uni_offset may differ from mark#offset as the script is edited *)
  mutable prev_uni_offset : int;  (* unicode offset for GTK *)
}

type session = {
  buffer : GText.buffer;
  script : Wg_ScriptView.script_view;
  proof : Wg_ProofView.proof_view;   (* the proof context panel *)
  messages : Wg_RoutedMessageViews.message_views_router;
  segment : Wg_Segment.segment; (* color coded status bar near bottom of the screen *)
  fileops : FileOps.ops;
  coqops : CoqOps.ops;
  coqtop : Coq.coqtop;
  command : Wg_Command.command_window; (* aka the Query Pane *)
  finder : Wg_Find.finder; (* Find / Replace panel *)
  debugger : Wg_Debugger.debugger_view;
  tab_label : GMisc.label;
  errpage : errpage;
  jobpage : jobpage;
  sid : int;
  basename : string;
  mutable control : control;
  mutable abs_file_name : string option;
  mutable debug_stop_pt : (session * int * int) option;
  mutable breakpoints : breakpoint list;
  mutable last_db_goals : Pp.t
}

let next_sid = ref 0

let create_buffer () =
  let buffer = GSourceView3.source_buffer
    ~tag_table:Tags.Script.table
    ~highlight_matching_brackets:true
    ?language:(lang_manager#language source_language#get)
    ?style_scheme:(style_manager#style_scheme source_style#get)
    ()
  in
  let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in
  let _ = buffer#create_mark
    ~left_gravity:false ~name:"stop_of_input" buffer#end_iter in
  let _ = buffer#create_mark ~name:"prev_insert" buffer#start_iter in
  let _ = buffer#place_cursor ~where:buffer#start_iter in
  let _ = buffer#add_selection_clipboard Ideutils.cb in
  buffer

let create_script coqtop source_buffer =
  let script = Wg_ScriptView.script_view coqtop ~source_buffer
    ~show_line_numbers:true ~wrap_mode:`NONE ()
    (* todo: line numbers don't appear *)
  in
  let _ = script#misc#set_name "ScriptWindow"
  in
  script

(** NB: Events during text edition:

    - [begin_user_action]
    - [insert_text] (or [delete_range] when deleting)
    - [changed]
    - [end_user_action]

   When pasting a text containing tags (e.g. the sentence terminators),
   there is actually many [insert_text] and [changed]. For instance,
   for "a. b.":

    - [begin_user_action]
    - [insert_text] (for "a")
    - [changed]
    - [insert_text] (for ".")
    - [changed]
    - [apply_tag] (for the tag of ".")
    - [insert_text] (for " b")
    - [changed]
    - [insert_text] (for ".")
    - [changed]
    - [apply_tag] (for the tag of ".")
    - [end_user_action]

  Since these copy-pasted tags may interact badly with the retag mechanism,
  we now don't monitor the "changed" event, but rather the "begin_user_action"
  and "end_user_action". We begin by setting a mark at the initial cursor
  point. At the end, the zone between the mark and the cursor is to be
  untagged and then retagged. *)

let misc () = CDebug.(get_flag misc)

type action_stack = Gtk.text_mark list option

let call_coq_or_cancel_action coqtop coqops (buffer : GText.buffer) it =
  let () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in
  let mark = buffer#create_mark ~name:"target" it in
  let action = coqops#go_to_mark (`MARK mark) in
  ignore @@ Coq.try_grab coqtop action (fun () -> ())

let init_user_action (stack : action_stack ref) = match !stack with
| None -> stack := Some []
| Some _ -> assert false

let close_user_action (stack : action_stack ref) = match !stack with
| None -> assert false
| Some marks ->
  let () = stack := None in
  marks

let handle_iter coqtop coqops (buffer : GText.buffer) it stack = match it with
| None -> ()
| Some it ->
  match !stack with
  | Some marks ->
    (* We are inside an user action, deferring to its end *)
    let mark = buffer#create_mark it in
    stack := Some (mark :: marks)
  | None ->
    (* Otherwise we move to the mark now *)
    call_coq_or_cancel_action coqtop coqops buffer it

let set_buffer_handlers
  (buffer : GText.buffer) script (coqops : CoqOps.ops) coqtop
=
  let action_stack = ref None in
  let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
  let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in
  let ensure_marks_exist () =
    try ignore(buffer#get_mark (`NAME "stop_of_input"))
    with GText.No_such_mark _ -> assert false in
  let get_insert () = buffer#get_iter_at_mark `INSERT in
  let update_prev it =
    let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
    if it#offset < prev#offset then
      buffer#move_mark (`NAME "prev_insert") ~where:it
  in
  let debug_edit_zone () = if false (*!Minilib.debug*) then begin
    buffer#remove_tag Tags.Script.edit_zone
      ~start:buffer#start_iter ~stop:buffer#end_iter;
    buffer#apply_tag Tags.Script.edit_zone
      ~start:(get_start()) ~stop:(get_stop())
    end in
  let processed_sentence_just_before_error it =
    let rec aux old it =
      if it#is_start then None
      else if it#has_tag Tags.Script.processed then Some old
      else if it#has_tag Tags.Script.error_bg then aux it it#backward_char
      else None in
    aux it it#copy in
  let insert_cb it s = if String.length s = 0 then () else begin
    if misc () then Minilib.log ("insert_cb " ^ string_of_int it#offset);
    let () = update_prev it in
    let iter =
      if it#has_tag Tags.Script.processed then Some it
      else if it#has_tag Tags.Script.error_bg then
        processed_sentence_just_before_error it
      else None
    in
    handle_iter coqtop coqops buffer iter action_stack
    end
  in
  let delete_cb ~start ~stop =
    if misc () then Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
    let min_iter, max_iter =
      if start#compare stop < 0 then start, stop else stop, start in
    let () = update_prev min_iter in
    let rec aux iter =
      if iter#equal max_iter then None
      else if iter#has_tag Tags.Script.processed then
        Some min_iter#backward_char
      else if iter#has_tag Tags.Script.error_bg then
        processed_sentence_just_before_error iter
      else aux iter#forward_char
    in
    let iter = aux min_iter in
    handle_iter coqtop coqops buffer iter action_stack
  in
  let begin_action_cb () =
    let () = if misc () then Minilib.log "begin_action_cb" in
    let () = init_user_action action_stack in
    let where = get_insert () in
    buffer#move_mark (`NAME "prev_insert") ~where
  in
  let end_action_cb () =
    let () = if misc () then Minilib.log "end_action_cb" in
    let marks = close_user_action action_stack in
    let () = ensure_marks_exist () in
    if CList.is_empty marks then
      let start, stop = get_start (), get_stop () in
      let () = List.iter (fun tag -> buffer#remove_tag tag ~start ~stop) Tags.Script.ephemere in
{'fraction_non_alphanumeric': 0.1183553780883454, 'fraction_numerical': 0.0008734714250062391, 'mean_word_length': 3.3795081967213116, 'pattern_counts': {'":': 2, '<': 9, '<?xml version=': 0, '>': 35, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7110655', 'n_tokens_mistral': 5198, 'n_tokens_neox': 5064, 'n_words': 1612}