<commit_before>(************************************************************************)
(*         *   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 Vernacexpr
open Vernacprop
open CErrors
open Util
open Pp
open Printer

module NamedDecl = Context.Named.Declaration
module CompactedDecl = Context.Compacted.Declaration

(** Idetop : an implementation of [Interface], i.e. mainly an interp
    function and a rewind function. *)


(** Signal handling: we postpone ^C during input and output phases,
    but make it directly raise a Sys.Break during evaluation of the request. *)

let catch_break = ref false

let init_signal_handler () =
  let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in
  Sys.set_signal Sys.sigint (Sys.Signal_handle f)

let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s

let pr_error s = pr_with_pid s
let pr_debug s =
  if !Flags.debug then pr_with_pid s
let pr_debug_call q =
  if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q)
let pr_debug_answer q r =
  if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r)

(** Categories of commands *)

let coqide_known_option table = List.mem table [
  ["Printing";"Implicit"];
  ["Printing";"Coercions"];
  ["Printing";"Matching"];
  ["Printing";"Synth"];
  ["Printing";"Notations"];
  ["Printing";"All"];
  ["Printing";"Records"];
  ["Printing";"Existential";"Instances"];
  ["Printing";"Universes"];
  ["Printing";"Unfocused"];
  ["Diffs"]]

let is_known_option cmd = match Vernacprop.under_control cmd with
  | VernacSetOption (_, o, BoolValue true)
  | VernacSetOption (_, o, StringValue _)
  | VernacUnsetOption (_, o) -> coqide_known_option o
  | _ -> false

(** Check whether a command is forbidden in the IDE *)

let ide_cmd_checks ~id {CAst.loc;v=ast} =
  let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in
  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
  if is_debug ast then
    user_error "Debug mode not available in the IDE";
  if is_known_option ast then
    warn "Set this option from the IDE menu instead";
  if is_navigation_vernac ast || is_undo ast then
    warn "Use IDE navigation instead"

(** Interpretation (cf. [Ide_intf.interp]) *)

let ide_doc = ref None
let get_doc () = Option.get !ide_doc
let set_doc doc = ide_doc := Some doc

let add ((s,eid),(sid,verbose)) =
  let doc = get_doc () in
  let pa = Pcoq.Parsable.make (Stream.of_string s) in
  match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
  | None -> assert false (* s is not an empty string *)
  | Some (loc, ast) ->
  let loc_ast = CAst.make ~loc ast in
  let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
  set_doc doc;
  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
  ide_cmd_checks ~id:newid loc_ast;
  (* TODO: the "" parameter is a leftover of the times the protocol
   * used to include stderr/stdout output.
   *
   * Currently, we force all the output meant for the to go via the
   * feedback mechanism, and we don't manipulate stderr/stdout, which
   * are left to the client's discrection. The parameter is still there
   * as not to break the core protocol for this minor change, but it should
   * be removed in the next version of the protocol.
   *)
  newid, (rc, "")

let edit_at id =
  let doc = get_doc () in
  match Stm.edit_at ~doc id with
  | doc, `NewTip -> set_doc doc; CSig.Inl ()
  | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip))<commit_msg>[ide] fail on unavailable commands before adding to the document<commit_after>(************************************************************************)
(*         *   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 Vernacexpr
open Vernacprop
open CErrors
open Util
open Pp
open Printer

module NamedDecl = Context.Named.Declaration
module CompactedDecl = Context.Compacted.Declaration

(** Idetop : an implementation of [Interface], i.e. mainly an interp
    function and a rewind function. *)


(** Signal handling: we postpone ^C during input and output phases,
    but make it directly raise a Sys.Break during evaluation of the request. *)

let catch_break = ref false

let init_signal_handler () =
  let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in
  Sys.set_signal Sys.sigint (Sys.Signal_handle f)

let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s

let pr_error s = pr_with_pid s
let pr_debug s =
  if !Flags.debug then pr_with_pid s
let pr_debug_call q =
  if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q)
let pr_debug_answer q r =
  if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r)

(** Categories of commands *)

let coqide_known_option table = List.mem table [
  ["Printing";"Implicit"];
  ["Printing";"Coercions"];
  ["Printing";"Matching"];
  ["Printing";"Synth"];
  ["Printing";"Notations"];
  ["Printing";"All"];
  ["Printing";"Records"];
  ["Printing";"Existential";"Instances"];
  ["Printing";"Universes"];
  ["Printing";"Unfocused"];
  ["Diffs"]]

let is_known_option cmd = match Vernacprop.under_control cmd with
  | VernacSetOption (_, o, BoolValue true)
  | VernacSetOption (_, o, StringValue _)
  | VernacUnsetOption (_, o) -> coqide_known_option o
  | _ -> false

(** Check whether a command is forbidden in the IDE *)

let ide_cmd_checks ~last_valid {CAst.loc;v=ast} =
  let user_error s =
    try CErrors.user_err ?loc ~hdr:"IDE" (str s)
    with e ->
      let (e, info) = CErrors.push e in
      let info = Stateid.add info ~valid:last_valid Stateid.dummy in
      Exninfo.raise ~info e
  in
  if is_debug ast then
    user_error "Debug mode not available in the IDE"

let ide_cmd_warns ~id {CAst.loc;v=ast} =
  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
  if is_known_option ast then
    warn "Set this option from the IDE menu instead";
  if is_navigation_vernac ast || is_undo ast then
    warn "Use IDE navigation instead"

(** Interpretation (cf. [Ide_intf.interp]) *)

let ide_doc = ref None
let get_doc () = Option.get !ide_doc
let set_doc doc = ide_doc := Some doc

let add ((s,eid),(sid,verbose)) =
  let doc = get_doc () in
  let pa = Pcoq.Parsable.make (Stream.of_string s) in
  match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
  | None -> assert false (* s is not an empty string *)
  | Some (loc, ast) ->
  let loc_ast = CAst.make ~loc ast in
  ide_cmd_checks ~last_valid:sid loc_ast;
  let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
  set_doc doc;
  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
  ide_cmd_warns ~id:newid loc_ast;
  (* TODO: the "" parameter is a leftover of the times the protocol
   * used to include stderr/stdout output.
   *
   * Currently, we force all the output meant for the to go via the
   * feedback mechanism, and we don't manipulate stderr/stdout, which
   * are left to the client's discrection. The parameter is still there
   * as not to break the core protocol for this minor change, but it should
   * be removed in the next version of the protocol.
   *)
  newid, (rc, "")

let edit_at id =
  let doc = get_doc () in
  match Stm.edit_at ~doc id with
  | doc, `NewTip -> set_doc doc; CSig.Inl ()
  | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip))
{'fraction_non_alphanumeric': 0.15702187720536345, 'fraction_numerical': 0.002352387673488591, 'mean_word_length': 3.5788906838987615, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 22, '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': '1944407', 'n_tokens_mistral': 2805, 'n_tokens_neox': 2682, 'n_words': 950}