search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
489 stars 86 forks source link

Error in coq-tq.el when saving a `.ml` file. #308

Closed proofbot closed 7 years ago

proofbot commented 7 years ago

Note: the issue was imported automatically using json2github.py

Original issue: psteckler/ProofGeneral#72 Opened by: @ejgallego

After some time, when executing save-current-buffer in an ml file with merlin-mode enabled, I get an error in coq-tq.el:

Debugger entered--Lisp error: (wrong-number-of-arguments (lambda (tq question closure fn) "Add a transaction to transaction queue TQ.
This sends the string QUESTION to the process that TQ communicates with.

When the corresponding answer comes back, we call FN with two
arguments: CLOSURE, which may contain additional data that FN
needs, and the answer to the question." (let ((sendp (tq-queue-empty tq))) (tq-queue-add tq (if sendp nil question) closure fn) (if sendp (progn (tq-log-and-send tq question))))) 5)
  tq-enqueue(nil "((assoc) (document auto \"/home/egallego/external/coq-master/ide/ide_slave.ml\") (query tell start end \"(************************************************************************)\n\n(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)\n(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)\n(*   \\\\VV/  **************************************************************)\n(*    //   *      This file is distributed under the terms of the       *)\n(*         *       GNU Lesser General Public License Version 2.1        *)\n(************************************************************************)\n\nopen Vernacexpr\nopen CErrors\nopen Util\nopen Pp\nopen Printer\n\nmodule RelDecl = Context.Rel.Declaration\nmodule NamedDecl = Context.Named.Declaration\nmodule CompactedDecl = Context.Compacted.Declaration\n\n(** Ide_slave : an implementation of [Interface], i.e. mainly an interp\n    function and a rewind function. This specialized loop is triggered\n    when the -ideslave option is passed to Coqtop. Currently CoqIDE is\n    the only one using this mode, but we try here to be as generic as\n    possible, so this may change in the future... *)\n\n(** Signal handling: we postpone ^C during input and output phases,\n    but make it directly raise a Sys.Break during evaluation of the request. *)\n\nlet catch_break = ref false\n\nlet init_signal_handler () =\n  let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in\n  Sys.set_signal Sys.sigint (Sys.Signal_handle f)\n\nlet pr_with_pid s = Printf.eprintf \\\"[pid %d] %s\\\\n%!\\\" (Unix.getpid ()) s\n\nlet pr_error s = pr_with_pid s\nlet pr_debug s =\n  if !Flags.debug then pr_with_pid s\nlet pr_debug_call q =\n  if !Flags.debug then pr_with_pid (\\\"<-- \\\" ^ Xmlprotocol.pr_call q)\nlet pr_debug_answer q r =\n  if !Flags.debug then pr_with_pid (\\\"--> \\\" ^ Xmlprotocol.pr_full_value q r)\n\n(** Categories of commands *)\n\nlet coqide_known_option table = List.mem table [\n  [\\\"Printing\\\";\\\"Implicit\\\"];\n  [\\\"Printing\\\";\\\"Coercions\\\"];\n  [\\\"Printing\\\";\\\"Matching\\\"];\n  [\\\"Printing\\\";\\\"Synth\\\"];\n  [\\\"Printing\\\";\\\"Notations\\\"];\n  [\\\"Printing\\\";\\\"All\\\"];\n  [\\\"Printing\\\";\\\"Records\\\"];\n  [\\\"Printing\\\";\\\"Existential\\\";\\\"Instances\\\"];\n  [\\\"Printing\\\";\\\"Universes\\\"]]\n\nlet is_known_option cmd = match cmd with\n  | VernacSetOption (o,BoolValue true)\n  | VernacUnsetOption o -> coqide_known_option o\n  | _ -> false\n\nlet is_debug cmd = match cmd with\n  | VernacSetOption ([\\\"Ltac\\\";\\\"Debug\\\"], _) -> true\n  | _ -> false\n\nlet is_query cmd = match cmd with\n  | VernacChdir None\n  | VernacMemOption _\n  | VernacPrintOption _\n  | VernacCheckMayEval _\n  | VernacGlobalCheck _\n  | VernacPrint _\n  | VernacSearch _\n  | VernacLocate _ -> true\n  | _ -> false\n\nlet is_undo cmd = match cmd with\n  | VernacUndo _ | VernacUndoTo _ -> true\n  | _ -> false\n\n(** Check whether a command is forbidden by CoqIDE *)\n\nlet coqide_cmd_checks (loc,ast) =\n  let user_error s = CErrors.user_err ~loc ~hdr:\\\"CoqIde\\\" (str s) in\n  if is_debug ast then\n    user_error \\\"Debug mode not available within CoqIDE\\\";\n  if is_known_option ast then\n    Feedback.msg_warning (strbrk\\\"This will not work. Use CoqIDE view menu instead\\\");\n  if Vernac.is_navigation_vernac ast || is_undo ast then\n    Feedback.msg_warning (strbrk \\\"Rather use CoqIDE navigation instead\\\");\n  if is_query ast then\n    Feedback.msg_warning (strbrk \\\"Query commands should not be inserted in scripts\\\")\n\n(** Interpretation (cf. [Ide_intf.interp]) *)\n\nlet add ((s,eid),(sid,verbose)) =\n  let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in\n  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in\n  newid, (rc, \\\"\\\")\n\nlet edit_at id =\n  match Stm.edit_at id with\n  | `NewTip -> CSig.Inl ()\n  | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip))\n\nlet query (s,id) = Stm.query ~at:id s; \\\"\\\"\n\nlet annotate phrase =\n  let (loc, ast) =\n    let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in\n    Vernac.parse_sentence (pa,None)\n  in\n  (* XXX: Width should be a parameter of annotate... *)\n  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)\n\n(** Goal display *)\n\nlet hyp_next_tac sigma env decl =\n  let id = NamedDecl.get_id decl in\n  let ast = NamedDecl.get_type decl in\n  let id_s = Names.Id.to_string id in\n  let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in\n  [\n    (\\\"clear \\\"^id_s),(\\\"clear \\\"^id_s^\\\".\\\");\n    (\\\"apply \\\"^id_s),(\\\"apply \\\"^id_s^\\\".\\\");\n    (\\\"exact \\\"^id_s),(\\\"exact \\\"^id_s^\\\".\\\");\n    (\\\"generalize \\\"^id_s),(\\\"generalize \\\"^id_s^\\\".\\\");\n    (\\\"absurd <\\\"^id_s^\\\">\\\"),(\\\"absurd \\\"^type_s^\\\".\\\")\n  ] @ [\n    (\\\"discriminate \\\"^id_s),(\\\"discriminate \\\"^id_s^\\\".\\\");\n    (\\\"injection \\\"^id_s),(\\\"injection \\\"^id_s^\\\".\\\")\n  ] @ [\n    (\\\"rewrite \\\"^id_s),(\\\"rewrite \\\"^id_s^\\\".\\\");\n    (\\\"rewrite <- \\\"^id_s),(\\\"rewrite <- \\\"^id_s^\\\".\\\")\n  ] @ [\n    (\\\"elim \\\"^id_s), (\\\"elim \\\"^id_s^\\\".\\\");\n    (\\\"inversion \\\"^id_s), (\\\"inversion \\\"^id_s^\\\".\\\");\n    (\\\"inversion clear \\\"^id_s), (\\\"inversion_clear \\\"^id_s^\\\".\\\")\n  ]\n\nlet concl_next_tac sigma concl =\n  let expand s = (s,s^\\\".\\\") in\n  List.map expand ([\n    \\\"intro\\\";\n    \\\"intros\\\";\n    \\\"intuition\\\"\n  ] @ [\n    \\\"reflexivity\\\";\n    \\\"discriminate\\\";\n    \\\"symmetry\\\"\n  ] @ [\n    \\\"assumption\\\";\n    \\\"omega\\\";\n    \\\"ring\\\";\n    \\\"auto\\\";\n    \\\"eauto\\\";\n    \\\"tauto\\\";\n    \\\"trivial\\\";\n    \\\"decide equality\\\";\n    \\\"simpl\\\";\n    \\\"subst\\\";\n    \\\"red\\\";\n    \\\"split\\\";\n    \\\"left\\\";\n    \\\"right\\\"\n  ])\n\nlet process_goal sigma g =\n  let env = Goal.V82.env sigma g in\n  let min_env = Environ.reset_context env in\n  let id = Goal.uid g in\n  let ccl =\n    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in\n    pr_goal_concl_style_env env sigma norm_constr\n  in\n  let process_hyp d (env,l) =\n    let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in\n    let d' = CompactedDecl.to_named_context d in\n      (List.fold_right Environ.push_named d' env,\n       (pr_compacted_decl env sigma d) :: l) in\n  let (_env, hyps) =\n    Context.Compacted.fold process_hyp\n      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in\n  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }\n\nlet export_pre_goals pgs =\n  {\n    Interface.fg_goals       = pgs.Proof.fg_goals;\n    Interface.bg_goals       = pgs.Proof.bg_goals;\n    Interface.shelved_goals  = pgs.Proof.shelved_goals;\n    Interface.given_up_goals = pgs.Proof.given_up_goals\n  }\n\nlet goals () =\n  Stm.finish ();\n  try\n    let pfts = Proof_global.give_me_the_proof () in\n    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))\n  with Proof_global.NoCurrentProof -> None\n\nlet evars () =\n  try\n    Stm.finish ();\n    let pfts = Proof_global.give_me_the_proof () in\n    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in\n    let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in\n    let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in\n    let el = List.map map_evar exl in\n    Some el\n  with Proof_global.NoCurrentProof -> None\n\nlet hints () =\n  try\n    let pfts = Proof_global.give_me_the_proof () in\n    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in\n    match all_goals with\n    | [] -> None\n    | g :: _ ->\n      let env = Goal.V82.env sigma g in\n      let hint_goal = concl_next_tac sigma g in\n      let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in\n      let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in\n      Some (hint_hyps, hint_goal)\n  with Proof_global.NoCurrentProof -> None\n\n\n(** Other API calls *)\n\nlet status force =\n  (** We remove the initial part of the current [DirPath.t]\n      (usually Top in an interactive session, cf \\\"coqtop -top\\\"),\n      and display the other parts (opened sections and modules) *)\n  Stm.finish ();\n  if force then Stm.join ();\n  let path =\n    let l = Names.DirPath.repr (Lib.cwd ()) in\n    List.rev_map Names.Id.to_string l\n  in\n  let proof =\n    try Some (Names.Id.to_string (Proof_global.get_current_proof_name ()))\n    with Proof_global.NoCurrentProof -> None\n  in\n  let allproofs =\n    let l = Proof_global.get_all_proof_names () in\n    List.map Names.Id.to_string l\n  in\n  {\n    Interface.status_path = path;\n    Interface.status_proofname = proof;\n    Interface.status_allproofs = allproofs;\n    Interface.status_proofnum = Stm.current_proof_depth ();\n  }\n\nlet export_coq_object t = {\n  Interface.coq_object_prefix = t.Search.coq_object_prefix;\n  Interface.coq_object_qualid = t.Search.coq_object_qualid;\n  Interface.coq_object_object = t.Search.coq_object_object\n}\n\nlet pattern_of_string ?env s =\n  let env =\n    match env with\n    | None -> Global.env ()\n    | Some e -> e\n  in\n  let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in\n  let (_, pat) = Constrintern.intern_constr_pattern env constr in\n  pat\n\nlet dirpath_of_string_list s =\n  let path = String.concat \\\".\\\" s in\n  let m = Pcoq.parse_string Pcoq.Constr.global path in\n  let (_, qid) = Libnames.qualid_of_reference m in\n  let id =\n    try Nametab.full_name_module qid\n    with Not_found ->\n      CErrors.user_err ~hdr:\\\"Search.interface_search\\\"\n        (str \\\"Module \\\" ++ str path ++ str \\\" not found.\\\")\n  in\n  id\n\nlet import_search_constraint = function\n  | Interface.Name_Pattern s    -> Search.Name_Pattern (Str.regexp s)\n  | Interface.Type_Pattern s    -> Search.Type_Pattern (pattern_of_string s)\n  | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s)\n  | Interface.In_Module ms      -> Search.In_Module (dirpath_of_string_list ms)\n  | Interface.Include_Blacklist -> Search.Include_Blacklist\n\nlet search flags =\n  List.map export_coq_object (Search.interface_search (\n    List.map (fun (c, b) -> (import_search_constraint c, b)) flags)\n  )\n\nlet export_option_value = function\n  | Goptions.BoolValue b   -> Interface.BoolValue b\n  | Goptions.IntValue x    -> Interface.IntValue x\n  | Goptions.StringValue s -> Interface.StringValue s\n  | Goptions.StringOptValue s -> Interface.StringOptValue s\n\nlet import_option_value = function\n  | Interface.BoolValue b   -> Goptions.BoolValue b\n  | Interface.IntValue x    -> Goptions.IntValue x\n  | Interface.StringValue s -> Goptions.StringValue s\n  | Interface.StringOptValue s -> Goptions.StringOptValue s\n\nlet export_option_state s = {\n  Interface.opt_sync  = s.Goptions.opt_sync;\n  Interface.opt_depr  = s.Goptions.opt_depr;\n  Interface.opt_name  = s.Goptions.opt_name;\n  Interface.opt_value = export_option_value s.Goptions.opt_value;\n}\n\nlet get_options () =\n  let table = Goptions.get_tables () in\n  let fold key state accu = (key, export_option_state state) :: accu in\n  Goptions.OptionMap.fold fold table []\n\nlet set_options options =\n  let iter (name, value) = match import_option_value value with\n  | BoolValue b -> Goptions.set_bool_option_value name b\n  | IntValue i -> Goptions.set_int_option_value name i\n  | StringValue s -> Goptions.set_string_option_value name s\n  | StringOptValue (Some s) -> Goptions.set_string_option_value name s\n  | StringOptValue None -> Goptions.unset_option_value_gen None name\n  in\n  List.iter iter options\n\nlet about () = {\n  Interface.coqtop_version = Coq_config.version;\n  Interface.protocol_version = Xmlprotocol.protocol_version;\n  Interface.release_date = Coq_config.date;\n  Interface.compile_date = Coq_config.compile_date;\n}\n\nlet handle_exn (e, info) =\n  let dummy = Stateid.dummy in\n  let loc_of e = match Loc.get_loc e with\n    | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)\n    | _ -> None in\n  let mk_msg () = CErrors.print ~info e in\n  match e with\n  | CErrors.Drop -> dummy, None, Pp.str \\\"Drop is not allowed by coqide!\\\"\n  | CErrors.Quit -> dummy, None, Pp.str \\\"Quit is not allowed by coqide!\\\"\n  | e ->\n      match Stateid.get info with\n      | Some (valid, _) -> valid, loc_of info, mk_msg ()\n      | None -> dummy, loc_of info, mk_msg ()\n\nlet init =\n  let initialized = ref false in\n  fun file ->\n   if !initialized then anomaly (str \\\"Already initialized\\\")\n   else begin\n     initialized := true;\n     match file with\n     | None -> Stm.get_current_state ()\n     | Some file ->\n         let dir = Filename.dirname file in\n         let open Loadpath in let open CUnix in\n         let initial_id, _ =\n           if not (is_in_load_paths (physical_path_of_string dir)) then\n             Stm.add false ~ontop:(Stm.get_current_state ())\n               0 (Printf.sprintf \\\"Add LoadPath \\\\\\\"%s\\\\\\\". \\\" dir)\n           else Stm.get_current_state (), `NewTip in\n         if Filename.check_suffix file \\\".v\\\" then\n           Stm.set_compilation_hints file;\n         Stm.finish ();\n         initial_id\n   end\n\n(* Retrocompatibility stuff *)\nlet interp ((_raw, verbose), s) =\n  let vernac_parse s =\n    let pa = Pcoq.Gram.parsable (Stream.of_string s) in\n    Flags.with_option Flags.we_are_parsing (fun () ->\n      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with\n      | None -> raise (Invalid_argument \\\"vernac_parse\\\")\n      | Some ast -> ast)\n    () in\n  Stm.interp verbose (vernac_parse s);\n  Stm.get_current_state (), CSig.Inl \\\"\\\"\n\n(** When receiving the Quit call, we don't directly do an [exit 0],\n    but rather set this reference, in order to send a final answer\n    before exiting. *)\n\nlet quit = ref false\n\n(** Serializes the output of Stm.get_ast  *)\nlet print_ast id =\n  match Stm.get_ast id with\n  | Some (expr, loc) -> begin\n      try  Texmacspp.tmpp expr loc\n      with e -> Xml_datatype.PCData (\\\"ERROR \\\" ^ Printexc.to_string e)\n    end\n  | None     -> Xml_datatype.PCData \\\"ERROR\\\"\n\n(** Grouping all call handlers together + error handling *)\n\nlet eval_call c =\n  let interruptible f x =\n    catch_break := true;\n    Control.check_for_interrupt ();\n    let r = f x in\n    catch_break := false;\n    r\n  in\n  let handler = {\n    Interface.add = interruptible add;\n    Interface.edit_at = interruptible edit_at;\n    Interface.query = interruptible query;\n    Interface.goals = interruptible goals;\n    Interface.evars = interruptible evars;\n    Interface.hints = interruptible hints;\n    Interface.status = interruptible status;\n    Interface.search = interruptible search;\n    Interface.get_options = interruptible get_options;\n    Interface.set_options = interruptible set_options;\n    Interface.mkcases = interruptible Vernacentries.make_cases;\n    Interface.quit = (fun () -> quit := true);\n    Interface.init = interruptible init;\n    Interface.about = interruptible about;\n    Interface.interp = interruptible interp;\n    Interface.handle_exn = handle_exn;\n    Interface.stop_worker = Stm.stop_worker;\n    Interface.print_ast = print_ast;\n    Interface.annotate = interruptible annotate;\n  } in\n  Xmlprotocol.abstract_eval_call handler c\n\n(** Message dispatching.\n    Since coqtop -ideslave starts 1 thread per slave, and each\n    thread forwards feedback messages from the slave to the GUI on the same\n    xml channel, we need mutual exclusion.  The mutex should be per-channel, but\n    here we only use 1 channel. *)\nlet print_xml =\n  let m = Mutex.create () in\n  fun oc xml ->\n    Mutex.lock m;\n    try Xml_printer.print oc xml; Mutex.unlock m\n    with e -> let e = CErrors.push e in Mutex.unlock m; iraise e\n\nlet slave_feeder fmt xml_oc msg =\n  let xml = Xmlprotocol.(of_feedback fmt msg) in\n  print_xml xml_oc xml\n\n(** The main loop *)\n\n(** Exceptions during eval_call should be converted into [Interface.Fail]\n    messages by [handle_exn] above. Otherwise, we die badly, without\n    trying to answer malformed requests. *)\n\nlet msg_format = ref (fun () ->\n    let margin = Option.default 72 (Topfmt.get_margin ()) in\n    Xmlprotocol.Richpp margin\n)\n\nlet loop () =\n  init_signal_handler ();\n  catch_break := false;\n  let in_ch, out_ch = Spawned.get_channels ()                        in\n  let xml_oc        = Xml_printer.make (Xml_printer.TChannel out_ch) in\n  let in_lb         = Lexing.from_function (fun s len ->\n                      CThread.thread_friendly_read in_ch s ~off:0 ~len) in\n  (* SEXP parser make *)\n  let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in\n  let () = Xml_parser.check_eof xml_ic false in\n  ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));\n  (* We'll handle goal fetching and display in our own way *)\n  Vernacentries.enable_goal_printing := false;\n  Vernacentries.qed_display_script := false;\n  while not !quit do\n    try\n      let xml_query = Xml_parser.parse xml_ic in\n(*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)\n      let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in\n      let () = pr_debug_call q in\n      let r  = eval_call q in\n      let () = pr_debug_answer q r in\n(*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)\n      print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r);\n      flush out_ch\n    with\n      | Xml_parser.Error (Xml_parser.Empty, _) ->\n        pr_debug \\\"End of input, exiting gracefully.\\\";\n        exit 0\n      | Xml_parser.Error (err, loc) ->\n        pr_error (\\\"XML syntax error: \\\" ^ Xml_parser.error_msg err)\n      | Serialize.Marshal_error (msg,node) ->\n        pr_error \\\"Unexpected XML message\\\";\n        pr_error (\\\"Expected XML node: \\\" ^ msg);\n        pr_error (\\\"XML tree received: \\\" ^ Xml_printer.to_string_fmt node)\n      | any ->\n        pr_debug (\\\"Fatal exception in coqtop:\\\\n\\\" ^ Printexc.to_string any);\n        exit 1\n  done;\n  pr_debug \\\"Exiting gracefully.\\\";\n  exit 0\n\nlet rec parse = function\n  | \\\"--help-XML-protocol\\\" :: rest ->\n        Xmlprotocol.document Xml_printer.to_string_fmt; exit 0\n  | \\\"--xml_format=Ppcmds\\\" :: rest ->\n        msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest\n  | x :: rest -> x :: parse rest\n  | [] -> []\n\nlet () = Coqtop.toploop_init := (fun args ->\n        let args = parse args in\n        Flags.make_silent true;\n        CoqworkmgrApi.(init Flags.High);\n        args)\n\nlet () = Coqtop.toploop_run := loop\n\nlet () = Usage.add_to_usage \\\"coqidetop\\\" \\\"  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\\\\n\\\"\n\"))\n" "\n" ((nil) (lambda (data) data) nil ((assoc) (document auto "/home/egallego/external/coq-master/ide/ide_slave.ml") (query tell start end "(************************************************************************)\n\n(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)\n(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)\n(*   \\VV/  **************************************************************)\n(*    //   *      This file is distributed under the terms of the       *)\n(*         *       GNU Lesser General Public License Version 2.1        *)\n(************************************************************************)\n\nopen Vernacexpr\nopen CErrors\nopen Util\nopen Pp\nopen Printer\n\nmodule RelDecl = Context.Rel.Declaration\nmodule NamedDecl = Context.Named.Declaration\nmodule CompactedDecl = Context.Compacted.Declaration\n\n(** Ide_slave : an implementation of [Interface], i.e. mainly an interp\n    function and a rewind function. This specialized loop is triggered\n    when the -ideslave option is passed to Coqtop. Currently CoqIDE is\n    the only one using this mode, but we try here to be as generic as\n    possible, so this may change in the future... *)\n\n(** Signal handling: we postpone ^C during input and output phases,\n    but make it directly raise a Sys.Break during evaluation of the request. *)\n\nlet catch_break = ref false\n\nlet init_signal_handler () =\n  let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in\n  Sys.set_signal Sys.sigint (Sys.Signal_handle f)\n\nlet pr_with_pid s = Printf.eprintf \"[pid %d] %s\\n%!\" (Unix.getpid ()) s\n\nlet pr_error s = pr_with_pid s\nlet pr_debug s =\n  if !Flags.debug then pr_with_pid s\nlet pr_debug_call q =\n  if !Flags.debug then pr_with_pid (\"<-- \" ^ Xmlprotocol.pr_call q)\nlet pr_debug_answer q r =\n  if !Flags.debug then pr_with_pid (\"--> \" ^ Xmlprotocol.pr_full_value q r)\n\n(** Categories of commands *)\n\nlet coqide_known_option table = List.mem table [\n  [\"Printing\";\"Implicit\"];\n  [\"Printing\";\"Coercions\"];\n  [\"Printing\";\"Matching\"];\n  [\"Printing\";\"Synth\"];\n  [\"Printing\";\"Notations\"];\n  [\"Printing\";\"All\"];\n  [\"Printing\";\"Records\"];\n  [\"Printing\";\"Existential\";\"Instances\"];\n  [\"Printing\";\"Universes\"]]\n\nlet is_known_option cmd = match cmd with\n  | VernacSetOption (o,BoolValue true)\n  | VernacUnsetOption o -> coqide_known_option o\n  | _ -> false\n\nlet is_debug cmd = match cmd with\n  | VernacSetOption ([\"Ltac\";\"Debug\"], _) -> true\n  | _ -> false\n\nlet is_query cmd = match cmd with\n  | VernacChdir None\n  | VernacMemOption _\n  | VernacPrintOption _\n  | VernacCheckMayEval _\n  | VernacGlobalCheck _\n  | VernacPrint _\n  | VernacSearch _\n  | VernacLocate _ -> true\n  | _ -> false\n\nlet is_undo cmd = match cmd with\n  | VernacUndo _ | VernacUndoTo _ -> true\n  | _ -> false\n\n(** Check whether a command is forbidden by CoqIDE *)\n\nlet coqide_cmd_checks (loc,ast) =\n  let user_error s = CErrors.user_err ~loc ~hdr:\"CoqIde\" (str s) in\n  if is_debug ast then\n    user_error \"Debug mode not available within CoqIDE\";\n  if is_known_option ast then\n    Feedback.msg_warning (strbrk\"This will not work. Use CoqIDE view menu instead\");\n  if Vernac.is_navigation_vernac ast || is_undo ast then\n    Feedback.msg_warning (strbrk \"Rather use CoqIDE navigation instead\");\n  if is_query ast then\n    Feedback.msg_warning (strbrk \"Query commands should not be inserted in scripts\")\n\n(** Interpretation (cf. [Ide_intf.interp]) *)\n\nlet add ((s,eid),(sid,verbose)) =\n  let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in\n  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in\n  newid, (rc, \"\")\n\nlet edit_at id =\n  match Stm.edit_at id with\n  | `NewTip -> CSig.Inl ()\n  | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip))\n\nlet query (s,id) = Stm.query ~at:id s; \"\"\n\nlet annotate phrase =\n  let (loc, ast) =\n    let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in\n    Vernac.parse_sentence (pa,None)\n  in\n  (* XXX: Width should be a parameter of annotate... *)\n  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)\n\n(** Goal display *)\n\nlet hyp_next_tac sigma env decl =\n  let id = NamedDecl.get_id decl in\n  let ast = NamedDecl.get_type decl in\n  let id_s = Names.Id.to_string id in\n  let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in\n  [\n    (\"clear \"^id_s),(\"clear \"^id_s^\".\");\n    (\"apply \"^id_s),(\"apply \"^id_s^\".\");\n    (\"exact \"^id_s),(\"exact \"^id_s^\".\");\n    (\"generalize \"^id_s),(\"generalize \"^id_s^\".\");\n    (\"absurd <\"^id_s^\">\"),(\"absurd \"^type_s^\".\")\n  ] @ [\n    (\"discriminate \"^id_s),(\"discriminate \"^id_s^\".\");\n    (\"injection \"^id_s),(\"injection \"^id_s^\".\")\n  ] @ [\n    (\"rewrite \"^id_s),(\"rewrite \"^id_s^\".\");\n    (\"rewrite <- \"^id_s),(\"rewrite <- \"^id_s^\".\")\n  ] @ [\n    (\"elim \"^id_s), (\"elim \"^id_s^\".\");\n    (\"inversion \"^id_s), (\"inversion \"^id_s^\".\");\n    (\"inversion clear \"^id_s), (\"inversion_clear \"^id_s^\".\")\n  ]\n\nlet concl_next_tac sigma concl =\n  let expand s = (s,s^\".\") in\n  List.map expand ([\n    \"intro\";\n    \"intros\";\n    \"intuition\"\n  ] @ [\n    \"reflexivity\";\n    \"discriminate\";\n    \"symmetry\"\n  ] @ [\n    \"assumption\";\n    \"omega\";\n    \"ring\";\n    \"auto\";\n    \"eauto\";\n    \"tauto\";\n    \"trivial\";\n    \"decide equality\";\n    \"simpl\";\n    \"subst\";\n    \"red\";\n    \"split\";\n    \"left\";\n    \"right\"\n  ])\n\nlet process_goal sigma g =\n  let env = Goal.V82.env sigma g in\n  let min_env = Environ.reset_context env in\n  let id = Goal.uid g in\n  let ccl =\n    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in\n    pr_goal_concl_style_env env sigma norm_constr\n  in\n  let process_hyp d (env,l) =\n    let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in\n    let d' = CompactedDecl.to_named_context d in\n      (List.fold_right Environ.push_named d' env,\n       (pr_compacted_decl env sigma d) :: l) in\n  let (_env, hyps) =\n    Context.Compacted.fold process_hyp\n      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in\n  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }\n\nlet export_pre_goals pgs =\n  {\n    Interface.fg_goals       = pgs.Proof.fg_goals;\n    Interface.bg_goals       = pgs.Proof.bg_goals;\n    Interface.shelved_goals  = pgs.Proof.shelved_goals;\n    Interface.given_up_goals = pgs.Proof.given_up_goals\n  }\n\nlet goals () =\n  Stm.finish ();\n  try\n    let pfts = Proof_global.give_me_the_proof () in\n    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))\n  with Proof_global.NoCurrentProof -> None\n\nlet evars () =\n  try\n    Stm.finish ();\n    let pfts = Proof_global.give_me_the_proof () in\n    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in\n    let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in\n    let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in\n    let el = List.map map_evar exl in\n    Some el\n  with Proof_global.NoCurrentProof -> None\n\nlet hints () =\n  try\n    let pfts = Proof_global.give_me_the_proof () in\n    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in\n    match all_goals with\n    | [] -> None\n    | g :: _ ->\n      let env = Goal.V82.env sigma g in\n      let hint_goal = concl_next_tac sigma g in\n      let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in\n      let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in\n      Some (hint_hyps, hint_goal)\n  with Proof_global.NoCurrentProof -> None\n\n\n(** Other API calls *)\n\nlet status force =\n  (** We remove the initial part of the current [DirPath.t]\n      (usually Top in an interactive session, cf \"coqtop -top\"),\n      and display the other parts (opened sections and modules) *)\n  Stm.finish ();\n  if force then Stm.join ();\n  let path =\n    let l = Names.DirPath.repr (Lib.cwd ()) in\n    List.rev_map Names.Id.to_string l\n  in\n  let proof =\n    try Some (Names.Id.to_string (Proof_global.get_current_proof_name ()))\n    with Proof_global.NoCurrentProof -> None\n  in\n  let allproofs =\n    let l = Proof_global.get_all_proof_names () in\n    List.map Names.Id.to_string l\n  in\n  {\n    Interface.status_path = path;\n    Interface.status_proofname = proof;\n    Interface.status_allproofs = allproofs;\n    Interface.status_proofnum = Stm.current_proof_depth ();\n  }\n\nlet export_coq_object t = {\n  Interface.coq_object_prefix = t.Search.coq_object_prefix;\n  Interface.coq_object_qualid = t.Search.coq_object_qualid;\n  Interface.coq_object_object = t.Search.coq_object_object\n}\n\nlet pattern_of_string ?env s =\n  let env =\n    match env with\n    | None -> Global.env ()\n    | Some e -> e\n  in\n  let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in\n  let (_, pat) = Constrintern.intern_constr_pattern env constr in\n  pat\n\nlet dirpath_of_string_list s =\n  let path = String.concat \".\" s in\n  let m = Pcoq.parse_string Pcoq.Constr.global path in\n  let (_, qid) = Libnames.qualid_of_reference m in\n  let id =\n    try Nametab.full_name_module qid\n    with Not_found ->\n      CErrors.user_err ~hdr:\"Search.interface_search\"\n        (str \"Module \" ++ str path ++ str \" not found.\")\n  in\n  id\n\nlet import_search_constraint = function\n  | Interface.Name_Pattern s    -> Search.Name_Pattern (Str.regexp s)\n  | Interface.Type_Pattern s    -> Search.Type_Pattern (pattern_of_string s)\n  | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s)\n  | Interface.In_Module ms      -> Search.In_Module (dirpath_of_string_list ms)\n  | Interface.Include_Blacklist -> Search.Include_Blacklist\n\nlet search flags =\n  List.map export_coq_object (Search.interface_search (\n    List.map (fun (c, b) -> (import_search_constraint c, b)) flags)\n  )\n\nlet export_option_value = function\n  | Goptions.BoolValue b   -> Interface.BoolValue b\n  | Goptions.IntValue x    -> Interface.IntValue x\n  | Goptions.StringValue s -> Interface.StringValue s\n  | Goptions.StringOptValue s -> Interface.StringOptValue s\n\nlet import_option_value = function\n  | Interface.BoolValue b   -> Goptions.BoolValue b\n  | Interface.IntValue x    -> Goptions.IntValue x\n  | Interface.StringValue s -> Goptions.StringValue s\n  | Interface.StringOptValue s -> Goptions.StringOptValue s\n\nlet export_option_state s = {\n  Interface.opt_sync  = s.Goptions.opt_sync;\n  Interface.opt_depr  = s.Goptions.opt_depr;\n  Interface.opt_name  = s.Goptions.opt_name;\n  Interface.opt_value = export_option_value s.Goptions.opt_value;\n}\n\nlet get_options () =\n  let table = Goptions.get_tables () in\n  let fold key state accu = (key, export_option_state state) :: accu in\n  Goptions.OptionMap.fold fold table []\n\nlet set_options options =\n  let iter (name, value) = match import_option_value value with\n  | BoolValue b -> Goptions.set_bool_option_value name b\n  | IntValue i -> Goptions.set_int_option_value name i\n  | StringValue s -> Goptions.set_string_option_value name s\n  | StringOptValue (Some s) -> Goptions.set_string_option_value name s\n  | StringOptValue None -> Goptions.unset_option_value_gen None name\n  in\n  List.iter iter options\n\nlet about () = {\n  Interface.coqtop_version = Coq_config.version;\n  Interface.protocol_version = Xmlprotocol.protocol_version;\n  Interface.release_date = Coq_config.date;\n  Interface.compile_date = Coq_config.compile_date;\n}\n\nlet handle_exn (e, info) =\n  let dummy = Stateid.dummy in\n  let loc_of e = match Loc.get_loc e with\n    | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)\n    | _ -> None in\n  let mk_msg () = CErrors.print ~info e in\n  match e with\n  | CErrors.Drop -> dummy, None, Pp.str \"Drop is not allowed by coqide!\"\n  | CErrors.Quit -> dummy, None, Pp.str \"Quit is not allowed by coqide!\"\n  | e ->\n      match Stateid.get info with\n      | Some (valid, _) -> valid, loc_of info, mk_msg ()\n      | None -> dummy, loc_of info, mk_msg ()\n\nlet init =\n  let initialized = ref false in\n  fun file ->\n   if !initialized then anomaly (str \"Already initialized\")\n   else begin\n     initialized := true;\n     match file with\n     | None -> Stm.get_current_state ()\n     | Some file ->\n         let dir = Filename.dirname file in\n         let open Loadpath in let open CUnix in\n         let initial_id, _ =\n           if not (is_in_load_paths (physical_path_of_string dir)) then\n             Stm.add false ~ontop:(Stm.get_current_state ())\n               0 (Printf.sprintf \"Add LoadPath \\\"%s\\\". \" dir)\n           else Stm.get_current_state (), `NewTip in\n         if Filename.check_suffix file \".v\" then\n           Stm.set_compilation_hints file;\n         Stm.finish ();\n         initial_id\n   end\n\n(* Retrocompatibility stuff *)\nlet interp ((_raw, verbose), s) =\n  let vernac_parse s =\n    let pa = Pcoq.Gram.parsable (Stream.of_string s) in\n    Flags.with_option Flags.we_are_parsing (fun () ->\n      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with\n      | None -> raise (Invalid_argument \"vernac_parse\")\n      | Some ast -> ast)\n    () in\n  Stm.interp verbose (vernac_parse s);\n  Stm.get_current_state (), CSig.Inl \"\"\n\n(** When receiving the Quit call, we don't directly do an [exit 0],\n    but rather set this reference, in order to send a final answer\n    before exiting. *)\n\nlet quit = ref false\n\n(** Serializes the output of Stm.get_ast  *)\nlet print_ast id =\n  match Stm.get_ast id with\n  | Some (expr, loc) -> begin\n      try  Texmacspp.tmpp expr loc\n      with e -> Xml_datatype.PCData (\"ERROR \" ^ Printexc.to_string e)\n    end\n  | None     -> Xml_datatype.PCData \"ERROR\"\n\n(** Grouping all call handlers together + error handling *)\n\nlet eval_call c =\n  let interruptible f x =\n    catch_break := true;\n    Control.check_for_interrupt ();\n    let r = f x in\n    catch_break := false;\n    r\n  in\n  let handler = {\n    Interface.add = interruptible add;\n    Interface.edit_at = interruptible edit_at;\n    Interface.query = interruptible query;\n    Interface.goals = interruptible goals;\n    Interface.evars = interruptible evars;\n    Interface.hints = interruptible hints;\n    Interface.status = interruptible status;\n    Interface.search = interruptible search;\n    Interface.get_options = interruptible get_options;\n    Interface.set_options = interruptible set_options;\n    Interface.mkcases = interruptible Vernacentries.make_cases;\n    Interface.quit = (fun () -> quit := true);\n    Interface.init = interruptible init;\n    Interface.about = interruptible about;\n    Interface.interp = interruptible interp;\n    Interface.handle_exn = handle_exn;\n    Interface.stop_worker = Stm.stop_worker;\n    Interface.print_ast = print_ast;\n    Interface.annotate = interruptible annotate;\n  } in\n  Xmlprotocol.abstract_eval_call handler c\n\n(** Message dispatching.\n    Since coqtop -ideslave starts 1 thread per slave, and each\n    thread forwards feedback messages from the slave to the GUI on the same\n    xml channel, we need mutual exclusion.  The mutex should be per-channel, but\n    here we only use 1 channel. *)\nlet print_xml =\n  let m = Mutex.create () in\n  fun oc xml ->\n    Mutex.lock m;\n    try Xml_printer.print oc xml; Mutex.unlock m\n    with e -> let e = CErrors.push e in Mutex.unlock m; iraise e\n\nlet slave_feeder fmt xml_oc msg =\n  let xml = Xmlprotocol.(of_feedback fmt msg) in\n  print_xml xml_oc xml\n\n(** The main loop *)\n\n(** Exceptions during eval_call should be converted into [Interface.Fail]\n    messages by [handle_exn] above. Otherwise, we die badly, without\n    trying to answer malformed requests. *)\n\nlet msg_format = ref (fun () ->\n    let margin = Option.default 72 (Topfmt.get_margin ()) in\n    Xmlprotocol.Richpp margin\n)\n\nlet loop () =\n  init_signal_handler ();\n  catch_break := false;\n  let in_ch, out_ch = Spawned.get_channels ()                        in\n  let xml_oc        = Xml_printer.make (Xml_printer.TChannel out_ch) in\n  let in_lb         = Lexing.from_function (fun s len ->\n                      CThread.thread_friendly_read in_ch s ~off:0 ~len) in\n  (* SEXP parser make *)\n  let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in\n  let () = Xml_parser.check_eof xml_ic false in\n  ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));\n  (* We'll handle goal fetching and display in our own way *)\n  Vernacentries.enable_goal_printing := false;\n  Vernacentries.qed_display_script := false;\n  while not !quit do\n    try\n      let xml_query = Xml_parser.parse xml_ic in\n(*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)\n      let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in\n      let () = pr_debug_call q in\n      let r  = eval_call q in\n      let () = pr_debug_answer q r in\n(*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)\n      print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r);\n      flush out_ch\n    with\n      | Xml_parser.Error (Xml_parser.Empty, _) ->\n        pr_debug \"End of input, exiting gracefully.\";\n        exit 0\n      | Xml_parser.Error (err, loc) ->\n        pr_error (\"XML syntax error: \" ^ Xml_parser.error_msg err)\n      | Serialize.Marshal_error (msg,node) ->\n        pr_error \"Unexpected XML message\";\n        pr_error (\"Expected XML node: \" ^ msg);\n        pr_error (\"XML tree received: \" ^ Xml_printer.to_string_fmt node)\n      | any ->\n        pr_debug (\"Fatal exception in coqtop:\\n\" ^ Printexc.to_string any);\n        exit 1\n  done;\n  pr_debug \"Exiting gracefully.\";\n  exit 0\n\nlet rec parse = function\n  | \"--help-XML-protocol\" :: rest ->\n        Xmlprotocol.document Xml_printer.to_string_fmt; exit 0\n  | \"--xml_format=Ppcmds\" :: rest ->\n        msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest\n  | x :: rest -> x :: parse rest\n  | [] -> []\n\nlet () = Coqtop.toploop_init := (fun args ->\n        let args = parse args in\n        Flags.make_silent true;\n        CoqworkmgrApi.(init Flags.High);\n        args)\n\nlet () = Coqtop.toploop_run := loop\n\nlet () = Usage.add_to_usage \"coqidetop\" \"  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\\n\"\n")) #<buffer ide_slave.ml>) merlin--send-command-async-handler)
  (save-current-buffer (set-buffer (merlin-process-buffer)) (if merlin-debug (progn (merlin-debug (format ">%s" string)))) (tq-enqueue merlin-process-queue string "\n" closure (function merlin--send-command-async-handler)) promise)
  (if (not (equal (process-status (merlin-process)) (quote run))) (progn (error "Merlin process not running (try restarting with %s)" (substitute-command-keys "\\[merlin-restart-process]")) nil) (save-current-buffer (set-buffer (merlin-process-buffer)) (if merlin-debug (progn (merlin-debug (format ">%s" string)))) (tq-enqueue merlin-process-queue string "\n" closure (function merlin--send-command-async-handler)) promise))
  (let* ((string (concat (prin1-to-string command) "\n")) (promise (cons nil nil)) (closure (list promise callback-if-success callback-if-exn command (current-buffer)))) (if (not (equal (process-status (merlin-process)) (quote run))) (progn (error "Merlin process not running (try restarting with %s)" (substitute-command-keys "\\[merlin-restart-process]")) nil) (save-current-buffer (set-buffer (merlin-process-buffer)) (if merlin-debug (progn (merlin-debug (format ">%s" string)))) (tq-enqueue merlin-process-queue string "\n" closure (function merlin--send-command-async-handler)) promise)))
  merlin/send-command-async((tell start end "(************************************************************************)\n\n(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)\n(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)\n(*   \\VV/  **************************************************************)\n(*    //   *      This file is distributed under the terms of the       *)\n(*         *       GNU Lesser General Public License Version 2.1        *)\n(************************************************************************)\n\nopen Vernacexpr\nopen CErrors\nopen Util\nopen Pp\nopen Printer\n\nmodule RelDecl = Context.Rel.Declaration\nmodule NamedDecl = Context.Named.Declaration\nmodule CompactedDecl = Context.Compacted.Declaration\n\n(** Ide_slave : an implementation of [Interface], i.e. mainly an interp\n    function and a rewind function. This specialized loop is triggered\n    when the -ideslave option is passed to Coqtop. Currently CoqIDE is\n    the only one using this mode, but we try here to be as generic as\n    possible, so this may change in the future... *)\n\n(** Signal handling: we postpone ^C during input and output phases,\n    but make it directly raise a Sys.Break during evaluation of the request. *)\n\nlet catch_break = ref false\n\nlet init_signal_handler () =\n  let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in\n  Sys.set_signal Sys.sigint (Sys.Signal_handle f)\n\nlet pr_with_pid s = Printf.eprintf \"[pid %d] %s\\n%!\" (Unix.getpid ()) s\n\nlet pr_error s = pr_with_pid s\nlet pr_debug s =\n  if !Flags.debug then pr_with_pid s\nlet pr_debug_call q =\n  if !Flags.debug then pr_with_pid (\"<-- \" ^ Xmlprotocol.pr_call q)\nlet pr_debug_answer q r =\n  if !Flags.debug then pr_with_pid (\"--> \" ^ Xmlprotocol.pr_full_value q r)\n\n(** Categories of commands *)\n\nlet coqide_known_option table = List.mem table [\n  [\"Printing\";\"Implicit\"];\n  [\"Printing\";\"Coercions\"];\n  [\"Printing\";\"Matching\"];\n  [\"Printing\";\"Synth\"];\n  [\"Printing\";\"Notations\"];\n  [\"Printing\";\"All\"];\n  [\"Printing\";\"Records\"];\n  [\"Printing\";\"Existential\";\"Instances\"];\n  [\"Printing\";\"Universes\"]]\n\nlet is_known_option cmd = match cmd with\n  | VernacSetOption (o,BoolValue true)\n  | VernacUnsetOption o -> coqide_known_option o\n  | _ -> false\n\nlet is_debug cmd = match cmd with\n  | VernacSetOption ([\"Ltac\";\"Debug\"], _) -> true\n  | _ -> false\n\nlet is_query cmd = match cmd with\n  | VernacChdir None\n  | VernacMemOption _\n  | VernacPrintOption _\n  | VernacCheckMayEval _\n  | VernacGlobalCheck _\n  | VernacPrint _\n  | VernacSearch _\n  | VernacLocate _ -> true\n  | _ -> false\n\nlet is_undo cmd = match cmd with\n  | VernacUndo _ | VernacUndoTo _ -> true\n  | _ -> false\n\n(** Check whether a command is forbidden by CoqIDE *)\n\nlet coqide_cmd_checks (loc,ast) =\n  let user_error s = CErrors.user_err ~loc ~hdr:\"CoqIde\" (str s) in\n  if is_debug ast then\n    user_error \"Debug mode not available within CoqIDE\";\n  if is_known_option ast then\n    Feedback.msg_warning (strbrk\"This will not work. Use CoqIDE view menu instead\");\n  if Vernac.is_navigation_vernac ast || is_undo ast then\n    Feedback.msg_warning (strbrk \"Rather use CoqIDE navigation instead\");\n  if is_query ast then\n    Feedback.msg_warning (strbrk \"Query commands should not be inserted in scripts\")\n\n(** Interpretation (cf. [Ide_intf.interp]) *)\n\nlet add ((s,eid),(sid,verbose)) =\n  let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in\n  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in\n  newid, (rc, \"\")\n\nlet edit_at id =\n  match Stm.edit_at id with\n  | `NewTip -> CSig.Inl ()\n  | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip))\n\nlet query (s,id) = Stm.query ~at:id s; \"\"\n\nlet annotate phrase =\n  let (loc, ast) =\n    let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in\n    Vernac.parse_sentence (pa,None)\n  in\n  (* XXX: Width should be a parameter of annotate... *)\n  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)\n\n(** Goal display *)\n\nlet hyp_next_tac sigma env decl =\n  let id = NamedDecl.get_id decl in\n  let ast = NamedDecl.get_type decl in\n  let id_s = Names.Id.to_string id in\n  let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in\n  [\n    (\"clear \"^id_s),(\"clear \"^id_s^\".\");\n    (\"apply \"^id_s),(\"apply \"^id_s^\".\");\n    (\"exact \"^id_s),(\"exact \"^id_s^\".\");\n    (\"generalize \"^id_s),(\"generalize \"^id_s^\".\");\n    (\"absurd <\"^id_s^\">\"),(\"absurd \"^type_s^\".\")\n  ] @ [\n    (\"discriminate \"^id_s),(\"discriminate \"^id_s^\".\");\n    (\"injection \"^id_s),(\"injection \"^id_s^\".\")\n  ] @ [\n    (\"rewrite \"^id_s),(\"rewrite \"^id_s^\".\");\n    (\"rewrite <- \"^id_s),(\"rewrite <- \"^id_s^\".\")\n  ] @ [\n    (\"elim \"^id_s), (\"elim \"^id_s^\".\");\n    (\"inversion \"^id_s), (\"inversion \"^id_s^\".\");\n    (\"inversion clear \"^id_s), (\"inversion_clear \"^id_s^\".\")\n  ]\n\nlet concl_next_tac sigma concl =\n  let expand s = (s,s^\".\") in\n  List.map expand ([\n    \"intro\";\n    \"intros\";\n    \"intuition\"\n  ] @ [\n    \"reflexivity\";\n    \"discriminate\";\n    \"symmetry\"\n  ] @ [\n    \"assumption\";\n    \"omega\";\n    \"ring\";\n    \"auto\";\n    \"eauto\";\n    \"tauto\";\n    \"trivial\";\n    \"decide equality\";\n    \"simpl\";\n    \"subst\";\n    \"red\";\n    \"split\";\n    \"left\";\n    \"right\"\n  ])\n\nlet process_goal sigma g =\n  let env = Goal.V82.env sigma g in\n  let min_env = Environ.reset_context env in\n  let id = Goal.uid g in\n  let ccl =\n    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in\n    pr_goal_concl_style_env env sigma norm_constr\n  in\n  let process_hyp d (env,l) =\n    let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in\n    let d' = CompactedDecl.to_named_context d in\n      (List.fold_right Environ.push_named d' env,\n       (pr_compacted_decl env sigma d) :: l) in\n  let (_env, hyps) =\n    Context.Compacted.fold process_hyp\n      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in\n  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }\n\nlet export_pre_goals pgs =\n  {\n    Interface.fg_goals       = pgs.Proof.fg_goals;\n    Interface.bg_goals       = pgs.Proof.bg_goals;\n    Interface.shelved_goals  = pgs.Proof.shelved_goals;\n    Interface.given_up_goals = pgs.Proof.given_up_goals\n  }\n\nlet goals () =\n  Stm.finish ();\n  try\n    let pfts = Proof_global.give_me_the_proof () in\n    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))\n  with Proof_global.NoCurrentProof -> None\n\nlet evars () =\n  try\n    Stm.finish ();\n    let pfts = Proof_global.give_me_the_proof () in\n    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in\n    let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in\n    let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in\n    let el = List.map map_evar exl in\n    Some el\n  with Proof_global.NoCurrentProof -> None\n\nlet hints () =\n  try\n    let pfts = Proof_global.give_me_the_proof () in\n    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in\n    match all_goals with\n    | [] -> None\n    | g :: _ ->\n      let env = Goal.V82.env sigma g in\n      let hint_goal = concl_next_tac sigma g in\n      let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in\n      let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in\n      Some (hint_hyps, hint_goal)\n  with Proof_global.NoCurrentProof -> None\n\n\n(** Other API calls *)\n\nlet status force =\n  (** We remove the initial part of the current [DirPath.t]\n      (usually Top in an interactive session, cf \"coqtop -top\"),\n      and display the other parts (opened sections and modules) *)\n  Stm.finish ();\n  if force then Stm.join ();\n  let path =\n    let l = Names.DirPath.repr (Lib.cwd ()) in\n    List.rev_map Names.Id.to_string l\n  in\n  let proof =\n    try Some (Names.Id.to_string (Proof_global.get_current_proof_name ()))\n    with Proof_global.NoCurrentProof -> None\n  in\n  let allproofs =\n    let l = Proof_global.get_all_proof_names () in\n    List.map Names.Id.to_string l\n  in\n  {\n    Interface.status_path = path;\n    Interface.status_proofname = proof;\n    Interface.status_allproofs = allproofs;\n    Interface.status_proofnum = Stm.current_proof_depth ();\n  }\n\nlet export_coq_object t = {\n  Interface.coq_object_prefix = t.Search.coq_object_prefix;\n  Interface.coq_object_qualid = t.Search.coq_object_qualid;\n  Interface.coq_object_object = t.Search.coq_object_object\n}\n\nlet pattern_of_string ?env s =\n  let env =\n    match env with\n    | None -> Global.env ()\n    | Some e -> e\n  in\n  let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in\n  let (_, pat) = Constrintern.intern_constr_pattern env constr in\n  pat\n\nlet dirpath_of_string_list s =\n  let path = String.concat \".\" s in\n  let m = Pcoq.parse_string Pcoq.Constr.global path in\n  let (_, qid) = Libnames.qualid_of_reference m in\n  let id =\n    try Nametab.full_name_module qid\n    with Not_found ->\n      CErrors.user_err ~hdr:\"Search.interface_search\"\n        (str \"Module \" ++ str path ++ str \" not found.\")\n  in\n  id\n\nlet import_search_constraint = function\n  | Interface.Name_Pattern s    -> Search.Name_Pattern (Str.regexp s)\n  | Interface.Type_Pattern s    -> Search.Type_Pattern (pattern_of_string s)\n  | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s)\n  | Interface.In_Module ms      -> Search.In_Module (dirpath_of_string_list ms)\n  | Interface.Include_Blacklist -> Search.Include_Blacklist\n\nlet search flags =\n  List.map export_coq_object (Search.interface_search (\n    List.map (fun (c, b) -> (import_search_constraint c, b)) flags)\n  )\n\nlet export_option_value = function\n  | Goptions.BoolValue b   -> Interface.BoolValue b\n  | Goptions.IntValue x    -> Interface.IntValue x\n  | Goptions.StringValue s -> Interface.StringValue s\n  | Goptions.StringOptValue s -> Interface.StringOptValue s\n\nlet import_option_value = function\n  | Interface.BoolValue b   -> Goptions.BoolValue b\n  | Interface.IntValue x    -> Goptions.IntValue x\n  | Interface.StringValue s -> Goptions.StringValue s\n  | Interface.StringOptValue s -> Goptions.StringOptValue s\n\nlet export_option_state s = {\n  Interface.opt_sync  = s.Goptions.opt_sync;\n  Interface.opt_depr  = s.Goptions.opt_depr;\n  Interface.opt_name  = s.Goptions.opt_name;\n  Interface.opt_value = export_option_value s.Goptions.opt_value;\n}\n\nlet get_options () =\n  let table = Goptions.get_tables () in\n  let fold key state accu = (key, export_option_state state) :: accu in\n  Goptions.OptionMap.fold fold table []\n\nlet set_options options =\n  let iter (name, value) = match import_option_value value with\n  | BoolValue b -> Goptions.set_bool_option_value name b\n  | IntValue i -> Goptions.set_int_option_value name i\n  | StringValue s -> Goptions.set_string_option_value name s\n  | StringOptValue (Some s) -> Goptions.set_string_option_value name s\n  | StringOptValue None -> Goptions.unset_option_value_gen None name\n  in\n  List.iter iter options\n\nlet about () = {\n  Interface.coqtop_version = Coq_config.version;\n  Interface.protocol_version = Xmlprotocol.protocol_version;\n  Interface.release_date = Coq_config.date;\n  Interface.compile_date = Coq_config.compile_date;\n}\n\nlet handle_exn (e, info) =\n  let dummy = Stateid.dummy in\n  let loc_of e = match Loc.get_loc e with\n    | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)\n    | _ -> None in\n  let mk_msg () = CErrors.print ~info e in\n  match e with\n  | CErrors.Drop -> dummy, None, Pp.str \"Drop is not allowed by coqide!\"\n  | CErrors.Quit -> dummy, None, Pp.str \"Quit is not allowed by coqide!\"\n  | e ->\n      match Stateid.get info with\n      | Some (valid, _) -> valid, loc_of info, mk_msg ()\n      | None -> dummy, loc_of info, mk_msg ()\n\nlet init =\n  let initialized = ref false in\n  fun file ->\n   if !initialized then anomaly (str \"Already initialized\")\n   else begin\n     initialized := true;\n     match file with\n     | None -> Stm.get_current_state ()\n     | Some file ->\n         let dir = Filename.dirname file in\n         let open Loadpath in let open CUnix in\n         let initial_id, _ =\n           if not (is_in_load_paths (physical_path_of_string dir)) then\n             Stm.add false ~ontop:(Stm.get_current_state ())\n               0 (Printf.sprintf \"Add LoadPath \\\"%s\\\". \" dir)\n           else Stm.get_current_state (), `NewTip in\n         if Filename.check_suffix file \".v\" then\n           Stm.set_compilation_hints file;\n         Stm.finish ();\n         initial_id\n   end\n\n(* Retrocompatibility stuff *)\nlet interp ((_raw, verbose), s) =\n  let vernac_parse s =\n    let pa = Pcoq.Gram.parsable (Stream.of_string s) in\n    Flags.with_option Flags.we_are_parsing (fun () ->\n      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with\n      | None -> raise (Invalid_argument \"vernac_parse\")\n      | Some ast -> ast)\n    () in\n  Stm.interp verbose (vernac_parse s);\n  Stm.get_current_state (), CSig.Inl \"\"\n\n(** When receiving the Quit call, we don't directly do an [exit 0],\n    but rather set this reference, in order to send a final answer\n    before exiting. *)\n\nlet quit = ref false\n\n(** Serializes the output of Stm.get_ast  *)\nlet print_ast id =\n  match Stm.get_ast id with\n  | Some (expr, loc) -> begin\n      try  Texmacspp.tmpp expr loc\n      with e -> Xml_datatype.PCData (\"ERROR \" ^ Printexc.to_string e)\n    end\n  | None     -> Xml_datatype.PCData \"ERROR\"\n\n(** Grouping all call handlers together + error handling *)\n\nlet eval_call c =\n  let interruptible f x =\n    catch_break := true;\n    Control.check_for_interrupt ();\n    let r = f x in\n    catch_break := false;\n    r\n  in\n  let handler = {\n    Interface.add = interruptible add;\n    Interface.edit_at = interruptible edit_at;\n    Interface.query = interruptible query;\n    Interface.goals = interruptible goals;\n    Interface.evars = interruptible evars;\n    Interface.hints = interruptible hints;\n    Interface.status = interruptible status;\n    Interface.search = interruptible search;\n    Interface.get_options = interruptible get_options;\n    Interface.set_options = interruptible set_options;\n    Interface.mkcases = interruptible Vernacentries.make_cases;\n    Interface.quit = (fun () -> quit := true);\n    Interface.init = interruptible init;\n    Interface.about = interruptible about;\n    Interface.interp = interruptible interp;\n    Interface.handle_exn = handle_exn;\n    Interface.stop_worker = Stm.stop_worker;\n    Interface.print_ast = print_ast;\n    Interface.annotate = interruptible annotate;\n  } in\n  Xmlprotocol.abstract_eval_call handler c\n\n(** Message dispatching.\n    Since coqtop -ideslave starts 1 thread per slave, and each\n    thread forwards feedback messages from the slave to the GUI on the same\n    xml channel, we need mutual exclusion.  The mutex should be per-channel, but\n    here we only use 1 channel. *)\nlet print_xml =\n  let m = Mutex.create () in\n  fun oc xml ->\n    Mutex.lock m;\n    try Xml_printer.print oc xml; Mutex.unlock m\n    with e -> let e = CErrors.push e in Mutex.unlock m; iraise e\n\nlet slave_feeder fmt xml_oc msg =\n  let xml = Xmlprotocol.(of_feedback fmt msg) in\n  print_xml xml_oc xml\n\n(** The main loop *)\n\n(** Exceptions during eval_call should be converted into [Interface.Fail]\n    messages by [handle_exn] above. Otherwise, we die badly, without\n    trying to answer malformed requests. *)\n\nlet msg_format = ref (fun () ->\n    let margin = Option.default 72 (Topfmt.get_margin ()) in\n    Xmlprotocol.Richpp margin\n)\n\nlet loop () =\n  init_signal_handler ();\n  catch_break := false;\n  let in_ch, out_ch = Spawned.get_channels ()                        in\n  let xml_oc        = Xml_printer.make (Xml_printer.TChannel out_ch) in\n  let in_lb         = Lexing.from_function (fun s len ->\n                      CThread.thread_friendly_read in_ch s ~off:0 ~len) in\n  (* SEXP parser make *)\n  let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in\n  let () = Xml_parser.check_eof xml_ic false in\n  ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));\n  (* We'll handle goal fetching and display in our own way *)\n  Vernacentries.enable_goal_printing := false;\n  Vernacentries.qed_display_script := false;\n  while not !quit do\n    try\n      let xml_query = Xml_parser.parse xml_ic in\n(*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)\n      let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in\n      let () = pr_debug_call q in\n      let r  = eval_call q in\n      let () = pr_debug_answer q r in\n(*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)\n      print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r);\n      flush out_ch\n    with\n      | Xml_parser.Error (Xml_parser.Empty, _) ->\n        pr_debug \"End of input, exiting gracefully.\";\n        exit 0\n      | Xml_parser.Error (err, loc) ->\n        pr_error (\"XML syntax error: \" ^ Xml_parser.error_msg err)\n      | Serialize.Marshal_error (msg,node) ->\n        pr_error \"Unexpected XML message\";\n        pr_error (\"Expected XML node: \" ^ msg);\n        pr_error (\"XML tree received: \" ^ Xml_printer.to_string_fmt node)\n      | any ->\n        pr_debug (\"Fatal exception in coqtop:\\n\" ^ Printexc.to_string any);\n        exit 1\n  done;\n  pr_debug \"Exiting gracefully.\";\n  exit 0\n\nlet rec parse = function\n  | \"--help-XML-protocol\" :: rest ->\n        Xmlprotocol.document Xml_printer.to_string_fmt; exit 0\n  | \"--xml_format=Ppcmds\" :: rest ->\n        msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest\n  | x :: rest -> x :: parse rest\n  | [] -> []\n\nlet () = Coqtop.toploop_init := (fun args ->\n        let args = parse args in\n        Flags.make_silent true;\n        CoqworkmgrApi.(init Flags.High);\n        args)\n\nlet () = Coqtop.toploop_run := loop\n\nlet () = Usage.add_to_usage \"coqidetop\" \"  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\\n\"\n") (lambda (data) data) nil)
  (let ((promise (merlin/send-command-async command (function (lambda (data) data)) callback-if-exn))) (if promise (progn (merlin--process-busy-set (list command)) (unwind-protect (let ((w32-pipe-read-delay 0) (merlin-command-priority nil)) (while (not (car promise)) (accept-process-output (merlin-process) 1.0))) (merlin--process-busy-set nil)) (cdr promise))))
  merlin/send-command((tell start end "(************************************************************************)\n\n(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)\n(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)\n(*   \\VV/  **************************************************************)\n(*    //   *      This file is distributed under the terms of the       *)\n(*         *       GNU Lesser General Public License Version 2.1        *)\n(************************************************************************)\n\nopen Vernacexpr\nopen CErrors\nopen Util\nopen Pp\nopen Printer\n\nmodule RelDecl = Context.Rel.Declaration\nmodule NamedDecl = Context.Named.Declaration\nmodule CompactedDecl = Context.Compacted.Declaration\n\n(** Ide_slave : an implementation of [Interface], i.e. mainly an interp\n    function and a rewind function. This specialized loop is triggered\n    when the -ideslave option is passed to Coqtop. Currently CoqIDE is\n    the only one using this mode, but we try here to be as generic as\n    possible, so this may change in the future... *)\n\n(** Signal handling: we postpone ^C during input and output phases,\n    but make it directly raise a Sys.Break during evaluation of the request. *)\n\nlet catch_break = ref false\n\nlet init_signal_handler () =\n  let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in\n  Sys.set_signal Sys.sigint (Sys.Signal_handle f)\n\nlet pr_with_pid s = Printf.eprintf \"[pid %d] %s\\n%!\" (Unix.getpid ()) s\n\nlet pr_error s = pr_with_pid s\nlet pr_debug s =\n  if !Flags.debug then pr_with_pid s\nlet pr_debug_call q =\n  if !Flags.debug then pr_with_pid (\"<-- \" ^ Xmlprotocol.pr_call q)\nlet pr_debug_answer q r =\n  if !Flags.debug then pr_with_pid (\"--> \" ^ Xmlprotocol.pr_full_value q r)\n\n(** Categories of commands *)\n\nlet coqide_known_option table = List.mem table [\n  [\"Printing\";\"Implicit\"];\n  [\"Printing\";\"Coercions\"];\n  [\"Printing\";\"Matching\"];\n  [\"Printing\";\"Synth\"];\n  [\"Printing\";\"Notations\"];\n  [\"Printing\";\"All\"];\n  [\"Printing\";\"Records\"];\n  [\"Printing\";\"Existential\";\"Instances\"];\n  [\"Printing\";\"Universes\"]]\n\nlet is_known_option cmd = match cmd with\n  | VernacSetOption (o,BoolValue true)\n  | VernacUnsetOption o -> coqide_known_option o\n  | _ -> false\n\nlet is_debug cmd = match cmd with\n  | VernacSetOption ([\"Ltac\";\"Debug\"], _) -> true\n  | _ -> false\n\nlet is_query cmd = match cmd with\n  | VernacChdir None\n  | VernacMemOption _\n  | VernacPrintOption _\n  | VernacCheckMayEval _\n  | VernacGlobalCheck _\n  | VernacPrint _\n  | VernacSearch _\n  | VernacLocate _ -> true\n  | _ -> false\n\nlet is_undo cmd = match cmd with\n  | VernacUndo _ | VernacUndoTo _ -> true\n  | _ -> false\n\n(** Check whether a command is forbidden by CoqIDE *)\n\nlet coqide_cmd_checks (loc,ast) =\n  let user_error s = CErrors.user_err ~loc ~hdr:\"CoqIde\" (str s) in\n  if is_debug ast then\n    user_error \"Debug mode not available within CoqIDE\";\n  if is_known_option ast then\n    Feedback.msg_warning (strbrk\"This will not work. Use CoqIDE view menu instead\");\n  if Vernac.is_navigation_vernac ast || is_undo ast then\n    Feedback.msg_warning (strbrk \"Rather use CoqIDE navigation instead\");\n  if is_query ast then\n    Feedback.msg_warning (strbrk \"Query commands should not be inserted in scripts\")\n\n(** Interpretation (cf. [Ide_intf.interp]) *)\n\nlet add ((s,eid),(sid,verbose)) =\n  let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in\n  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in\n  newid, (rc, \"\")\n\nlet edit_at id =\n  match Stm.edit_at id with\n  | `NewTip -> CSig.Inl ()\n  | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip))\n\nlet query (s,id) = Stm.query ~at:id s; \"\"\n\nlet annotate phrase =\n  let (loc, ast) =\n    let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in\n    Vernac.parse_sentence (pa,None)\n  in\n  (* XXX: Width should be a parameter of annotate... *)\n  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)\n\n(** Goal display *)\n\nlet hyp_next_tac sigma env decl =\n  let id = NamedDecl.get_id decl in\n  let ast = NamedDecl.get_type decl in\n  let id_s = Names.Id.to_string id in\n  let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in\n  [\n    (\"clear \"^id_s),(\"clear \"^id_s^\".\");\n    (\"apply \"^id_s),(\"apply \"^id_s^\".\");\n    (\"exact \"^id_s),(\"exact \"^id_s^\".\");\n    (\"generalize \"^id_s),(\"generalize \"^id_s^\".\");\n    (\"absurd <\"^id_s^\">\"),(\"absurd \"^type_s^\".\")\n  ] @ [\n    (\"discriminate \"^id_s),(\"discriminate \"^id_s^\".\");\n    (\"injection \"^id_s),(\"injection \"^id_s^\".\")\n  ] @ [\n    (\"rewrite \"^id_s),(\"rewrite \"^id_s^\".\");\n    (\"rewrite <- \"^id_s),(\"rewrite <- \"^id_s^\".\")\n  ] @ [\n    (\"elim \"^id_s), (\"elim \"^id_s^\".\");\n    (\"inversion \"^id_s), (\"inversion \"^id_s^\".\");\n    (\"inversion clear \"^id_s), (\"inversion_clear \"^id_s^\".\")\n  ]\n\nlet concl_next_tac sigma concl =\n  let expand s = (s,s^\".\") in\n  List.map expand ([\n    \"intro\";\n    \"intros\";\n    \"intuition\"\n  ] @ [\n    \"reflexivity\";\n    \"discriminate\";\n    \"symmetry\"\n  ] @ [\n    \"assumption\";\n    \"omega\";\n    \"ring\";\n    \"auto\";\n    \"eauto\";\n    \"tauto\";\n    \"trivial\";\n    \"decide equality\";\n    \"simpl\";\n    \"subst\";\n    \"red\";\n    \"split\";\n    \"left\";\n    \"right\"\n  ])\n\nlet process_goal sigma g =\n  let env = Goal.V82.env sigma g in\n  let min_env = Environ.reset_context env in\n  let id = Goal.uid g in\n  let ccl =\n    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in\n    pr_goal_concl_style_env env sigma norm_constr\n  in\n  let process_hyp d (env,l) =\n    let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in\n    let d' = CompactedDecl.to_named_context d in\n      (List.fold_right Environ.push_named d' env,\n       (pr_compacted_decl env sigma d) :: l) in\n  let (_env, hyps) =\n    Context.Compacted.fold process_hyp\n      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in\n  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }\n\nlet export_pre_goals pgs =\n  {\n    Interface.fg_goals       = pgs.Proof.fg_goals;\n    Interface.bg_goals       = pgs.Proof.bg_goals;\n    Interface.shelved_goals  = pgs.Proof.shelved_goals;\n    Interface.given_up_goals = pgs.Proof.given_up_goals\n  }\n\nlet goals () =\n  Stm.finish ();\n  try\n    let pfts = Proof_global.give_me_the_proof () in\n    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))\n  with Proof_global.NoCurrentProof -> None\n\nlet evars () =\n  try\n    Stm.finish ();\n    let pfts = Proof_global.give_me_the_proof () in\n    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in\n    let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in\n    let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in\n    let el = List.map map_evar exl in\n    Some el\n  with Proof_global.NoCurrentProof -> None\n\nlet hints () =\n  try\n    let pfts = Proof_global.give_me_the_proof () in\n    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in\n    match all_goals with\n    | [] -> None\n    | g :: _ ->\n      let env = Goal.V82.env sigma g in\n      let hint_goal = concl_next_tac sigma g in\n      let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in\n      let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in\n      Some (hint_hyps, hint_goal)\n  with Proof_global.NoCurrentProof -> None\n\n\n(** Other API calls *)\n\nlet status force =\n  (** We remove the initial part of the current [DirPath.t]\n      (usually Top in an interactive session, cf \"coqtop -top\"),\n      and display the other parts (opened sections and modules) *)\n  Stm.finish ();\n  if force then Stm.join ();\n  let path =\n    let l = Names.DirPath.repr (Lib.cwd ()) in\n    List.rev_map Names.Id.to_string l\n  in\n  let proof =\n    try Some (Names.Id.to_string (Proof_global.get_current_proof_name ()))\n    with Proof_global.NoCurrentProof -> None\n  in\n  let allproofs =\n    let l = Proof_global.get_all_proof_names () in\n    List.map Names.Id.to_string l\n  in\n  {\n    Interface.status_path = path;\n    Interface.status_proofname = proof;\n    Interface.status_allproofs = allproofs;\n    Interface.status_proofnum = Stm.current_proof_depth ();\n  }\n\nlet export_coq_object t = {\n  Interface.coq_object_prefix = t.Search.coq_object_prefix;\n  Interface.coq_object_qualid = t.Search.coq_object_qualid;\n  Interface.coq_object_object = t.Search.coq_object_object\n}\n\nlet pattern_of_string ?env s =\n  let env =\n    match env with\n    | None -> Global.env ()\n    | Some e -> e\n  in\n  let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in\n  let (_, pat) = Constrintern.intern_constr_pattern env constr in\n  pat\n\nlet dirpath_of_string_list s =\n  let path = String.concat \".\" s in\n  let m = Pcoq.parse_string Pcoq.Constr.global path in\n  let (_, qid) = Libnames.qualid_of_reference m in\n  let id =\n    try Nametab.full_name_module qid\n    with Not_found ->\n      CErrors.user_err ~hdr:\"Search.interface_search\"\n        (str \"Module \" ++ str path ++ str \" not found.\")\n  in\n  id\n\nlet import_search_constraint = function\n  | Interface.Name_Pattern s    -> Search.Name_Pattern (Str.regexp s)\n  | Interface.Type_Pattern s    -> Search.Type_Pattern (pattern_of_string s)\n  | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s)\n  | Interface.In_Module ms      -> Search.In_Module (dirpath_of_string_list ms)\n  | Interface.Include_Blacklist -> Search.Include_Blacklist\n\nlet search flags =\n  List.map export_coq_object (Search.interface_search (\n    List.map (fun (c, b) -> (import_search_constraint c, b)) flags)\n  )\n\nlet export_option_value = function\n  | Goptions.BoolValue b   -> Interface.BoolValue b\n  | Goptions.IntValue x    -> Interface.IntValue x\n  | Goptions.StringValue s -> Interface.StringValue s\n  | Goptions.StringOptValue s -> Interface.StringOptValue s\n\nlet import_option_value = function\n  | Interface.BoolValue b   -> Goptions.BoolValue b\n  | Interface.IntValue x    -> Goptions.IntValue x\n  | Interface.StringValue s -> Goptions.StringValue s\n  | Interface.StringOptValue s -> Goptions.StringOptValue s\n\nlet export_option_state s = {\n  Interface.opt_sync  = s.Goptions.opt_sync;\n  Interface.opt_depr  = s.Goptions.opt_depr;\n  Interface.opt_name  = s.Goptions.opt_name;\n  Interface.opt_value = export_option_value s.Goptions.opt_value;\n}\n\nlet get_options () =\n  let table = Goptions.get_tables () in\n  let fold key state accu = (key, export_option_state state) :: accu in\n  Goptions.OptionMap.fold fold table []\n\nlet set_options options =\n  let iter (name, value) = match import_option_value value with\n  | BoolValue b -> Goptions.set_bool_option_value name b\n  | IntValue i -> Goptions.set_int_option_value name i\n  | StringValue s -> Goptions.set_string_option_value name s\n  | StringOptValue (Some s) -> Goptions.set_string_option_value name s\n  | StringOptValue None -> Goptions.unset_option_value_gen None name\n  in\n  List.iter iter options\n\nlet about () = {\n  Interface.coqtop_version = Coq_config.version;\n  Interface.protocol_version = Xmlprotocol.protocol_version;\n  Interface.release_date = Coq_config.date;\n  Interface.compile_date = Coq_config.compile_date;\n}\n\nlet handle_exn (e, info) =\n  let dummy = Stateid.dummy in\n  let loc_of e = match Loc.get_loc e with\n    | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)\n    | _ -> None in\n  let mk_msg () = CErrors.print ~info e in\n  match e with\n  | CErrors.Drop -> dummy, None, Pp.str \"Drop is not allowed by coqide!\"\n  | CErrors.Quit -> dummy, None, Pp.str \"Quit is not allowed by coqide!\"\n  | e ->\n      match Stateid.get info with\n      | Some (valid, _) -> valid, loc_of info, mk_msg ()\n      | None -> dummy, loc_of info, mk_msg ()\n\nlet init =\n  let initialized = ref false in\n  fun file ->\n   if !initialized then anomaly (str \"Already initialized\")\n   else begin\n     initialized := true;\n     match file with\n     | None -> Stm.get_current_state ()\n     | Some file ->\n         let dir = Filename.dirname file in\n         let open Loadpath in let open CUnix in\n         let initial_id, _ =\n           if not (is_in_load_paths (physical_path_of_string dir)) then\n             Stm.add false ~ontop:(Stm.get_current_state ())\n               0 (Printf.sprintf \"Add LoadPath \\\"%s\\\". \" dir)\n           else Stm.get_current_state (), `NewTip in\n         if Filename.check_suffix file \".v\" then\n           Stm.set_compilation_hints file;\n         Stm.finish ();\n         initial_id\n   end\n\n(* Retrocompatibility stuff *)\nlet interp ((_raw, verbose), s) =\n  let vernac_parse s =\n    let pa = Pcoq.Gram.parsable (Stream.of_string s) in\n    Flags.with_option Flags.we_are_parsing (fun () ->\n      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with\n      | None -> raise (Invalid_argument \"vernac_parse\")\n      | Some ast -> ast)\n    () in\n  Stm.interp verbose (vernac_parse s);\n  Stm.get_current_state (), CSig.Inl \"\"\n\n(** When receiving the Quit call, we don't directly do an [exit 0],\n    but rather set this reference, in order to send a final answer\n    before exiting. *)\n\nlet quit = ref false\n\n(** Serializes the output of Stm.get_ast  *)\nlet print_ast id =\n  match Stm.get_ast id with\n  | Some (expr, loc) -> begin\n      try  Texmacspp.tmpp expr loc\n      with e -> Xml_datatype.PCData (\"ERROR \" ^ Printexc.to_string e)\n    end\n  | None     -> Xml_datatype.PCData \"ERROR\"\n\n(** Grouping all call handlers together + error handling *)\n\nlet eval_call c =\n  let interruptible f x =\n    catch_break := true;\n    Control.check_for_interrupt ();\n    let r = f x in\n    catch_break := false;\n    r\n  in\n  let handler = {\n    Interface.add = interruptible add;\n    Interface.edit_at = interruptible edit_at;\n    Interface.query = interruptible query;\n    Interface.goals = interruptible goals;\n    Interface.evars = interruptible evars;\n    Interface.hints = interruptible hints;\n    Interface.status = interruptible status;\n    Interface.search = interruptible search;\n    Interface.get_options = interruptible get_options;\n    Interface.set_options = interruptible set_options;\n    Interface.mkcases = interruptible Vernacentries.make_cases;\n    Interface.quit = (fun () -> quit := true);\n    Interface.init = interruptible init;\n    Interface.about = interruptible about;\n    Interface.interp = interruptible interp;\n    Interface.handle_exn = handle_exn;\n    Interface.stop_worker = Stm.stop_worker;\n    Interface.print_ast = print_ast;\n    Interface.annotate = interruptible annotate;\n  } in\n  Xmlprotocol.abstract_eval_call handler c\n\n(** Message dispatching.\n    Since coqtop -ideslave starts 1 thread per slave, and each\n    thread forwards feedback messages from the slave to the GUI on the same\n    xml channel, we need mutual exclusion.  The mutex should be per-channel, but\n    here we only use 1 channel. *)\nlet print_xml =\n  let m = Mutex.create () in\n  fun oc xml ->\n    Mutex.lock m;\n    try Xml_printer.print oc xml; Mutex.unlock m\n    with e -> let e = CErrors.push e in Mutex.unlock m; iraise e\n\nlet slave_feeder fmt xml_oc msg =\n  let xml = Xmlprotocol.(of_feedback fmt msg) in\n  print_xml xml_oc xml\n\n(** The main loop *)\n\n(** Exceptions during eval_call should be converted into [Interface.Fail]\n    messages by [handle_exn] above. Otherwise, we die badly, without\n    trying to answer malformed requests. *)\n\nlet msg_format = ref (fun () ->\n    let margin = Option.default 72 (Topfmt.get_margin ()) in\n    Xmlprotocol.Richpp margin\n)\n\nlet loop () =\n  init_signal_handler ();\n  catch_break := false;\n  let in_ch, out_ch = Spawned.get_channels ()                        in\n  let xml_oc        = Xml_printer.make (Xml_printer.TChannel out_ch) in\n  let in_lb         = Lexing.from_function (fun s len ->\n                      CThread.thread_friendly_read in_ch s ~off:0 ~len) in\n  (* SEXP parser make *)\n  let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in\n  let () = Xml_parser.check_eof xml_ic false in\n  ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));\n  (* We'll handle goal fetching and display in our own way *)\n  Vernacentries.enable_goal_printing := false;\n  Vernacentries.qed_display_script := false;\n  while not !quit do\n    try\n      let xml_query = Xml_parser.parse xml_ic in\n(*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)\n      let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in\n      let () = pr_debug_call q in\n      let r  = eval_call q in\n      let () = pr_debug_answer q r in\n(*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)\n      print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r);\n      flush out_ch\n    with\n      | Xml_parser.Error (Xml_parser.Empty, _) ->\n        pr_debug \"End of input, exiting gracefully.\";\n        exit 0\n      | Xml_parser.Error (err, loc) ->\n        pr_error (\"XML syntax error: \" ^ Xml_parser.error_msg err)\n      | Serialize.Marshal_error (msg,node) ->\n        pr_error \"Unexpected XML message\";\n        pr_error (\"Expected XML node: \" ^ msg);\n        pr_error (\"XML tree received: \" ^ Xml_printer.to_string_fmt node)\n      | any ->\n        pr_debug (\"Fatal exception in coqtop:\\n\" ^ Printexc.to_string any);\n        exit 1\n  done;\n  pr_debug \"Exiting gracefully.\";\n  exit 0\n\nlet rec parse = function\n  | \"--help-XML-protocol\" :: rest ->\n        Xmlprotocol.document Xml_printer.to_string_fmt; exit 0\n  | \"--xml_format=Ppcmds\" :: rest ->\n        msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest\n  | x :: rest -> x :: parse rest\n  | [] -> []\n\nlet () = Coqtop.toploop_init := (fun args ->\n        let args = parse args in\n        Flags.make_silent true;\n        CoqworkmgrApi.(init Flags.High);\n        args)\n\nlet () = Coqtop.toploop_run := loop\n\nlet () = Usage.add_to_usage \"coqidetop\" \"  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\\n\"\n"))
  merlin/sync()
  merlin--error-check(t)
  (progn (merlin--error-check t))
  (if merlin-mode (progn (merlin--error-check t)))
  merlin-error-check()
  (progn (merlin-error-check))
  (if (and merlin-mode merlin-error-after-save) (progn (merlin-error-check)))
  merlin--after-save()
  ad-Advice-basic-save-buffer(#[256 "r\306 \203\n\306 q\210\307 \204\203P\310!\204P\311 \312\204P\313\314\315\312\313\316 !#!\310!\203K\317!\203>\320\321\"\210\202K\322\323\324\"!\204K\320\325!\210\326!\266\327p!\204k\310!\203k\330\331\332\333!\"!\204k\334\335!\210\214~\210\212deV\203\261 \204\261dSf\336U\204\261\n\337=\203\217dSf\340U\204\261\337=\204\251\341=\204\251\203\261\322\331\342\316 \"!\203\261\212db\210\336c\210))\343 \210\3441\300\345\346!0\202\306\347\350\"\262\210\351\352!\204\375\351\353!\204\375\351\354!\204\375\355\313!!\310!\204\371\322\323\356\"!\203\365\357\337\"\210\202\371\320\325!\210\360 \266\202\f\203
\202   
;\336\361!\233<\211\203@\3621;\3631%\364@\"0\202-\347\350\"\210\312\262?\2057\365A@\"0\202?\210\202@\210)\366!\210\367 \210\345\370!\266\202\202]=\206]\211?\206]\371\372!)\207" [buffer-file-name find-file-literally selective-display require-final-newline save-buffer-coding-system last-coding-system-used buffer-base-buffer buffer-modified-p file-exists-p recent-auto-save-p nil expand-file-name read-file-name "File to save in: " buffer-name file-directory-p error "%s is a directory" y-or-n-p format-message "File `%s' exists; overwrite? " "Canceled" set-visited-file-name verify-visited-file-modtime yes-or-no-p format "%s has changed since visited or saved.  Save anyway? " file-name-nondirectory user-error "Save not confirmed" 10 t 13 visit-save "Buffer %s does not end in newline.  Add one? " vc-before-save (debug error) run-hooks before-save-hook message "Error: %S" run-hook-with-args-until-success write-contents-functions local-write-file-hooks write-file-functions file-name-directory "Directory `%s' does not exist; create? " make-directory basic-save-buffer-1 file-attributes ...] 9 1979213 (quote (called-interactively))] t)
  apply(ad-Advice-basic-save-buffer #[256 "r\306 \203\n\306 q\210\307 \204\203P\310!\204P\311 \312\204P\313\314\315\312\313\316 !#!\310!\203K\317!\203>\320\321\"\210\202K\322\323\324\"!\204K\320\325!\210\326!\266\327p!\204k\310!\203k\330\331\332\333!\"!\204k\334\335!\210\214~\210\212deV\203\261   \204\261dSf\336U\204\261\n\337=\203\217dSf\340U\204\261\337=\204\251\341=\204\251\203\261\322\331\342\316 \"!\203\261\212db\210\336c\210))\343 \210\3441\300\345\346!0\202\306\347\350\"\262\210\351\352!\204\375\351\353!\204\375\351\354!\204\375\355\313!!\310!\204\371\322\323\356\"!\203\365\357\337\"\210\202\371\320\325!\210\360 \266\202\f\203
\202   
;\336\361!\233<\211\203@\3621;\3631%\364@\"0\202-\347\350\"\210\312\262?\2057\365A@\"0\202?\210\202@\210)\366!\210\367 \210\345\370!\266\202\202]=\206]\211?\206]\371\372!)\207" [buffer-file-name find-file-literally selective-display require-final-newline save-buffer-coding-system last-coding-system-used buffer-base-buffer buffer-modified-p file-exists-p recent-auto-save-p nil expand-file-name read-file-name "File to save in: " buffer-name file-directory-p error "%s is a directory" y-or-n-p format-message "File `%s' exists; overwrite? " "Canceled" set-visited-file-name verify-visited-file-modtime yes-or-no-p format "%s has changed since visited or saved.  Save anyway? " file-name-nondirectory user-error "Save not confirmed" 10 t 13 visit-save "Buffer %s does not end in newline.  Add one? " vc-before-save (debug error) run-hooks before-save-hook message "Error: %S" run-hook-with-args-until-success write-contents-functions local-write-file-hooks write-file-functions file-name-directory "Directory `%s' does not exist; create? " make-directory basic-save-buffer-1 file-attributes ...] 9 1979213 (quote (called-interactively))] t)
  basic-save-buffer(t)
  save-buffer(1)
  funcall-interactively(save-buffer 1)
  call-interactively(save-buffer nil nil)
  command-execute(save-buffer)
proofbot commented 7 years ago

Comment author: @psteckler

It's a name clash between the standard Emacs tq library and the modified version I'm using for PG with Coq. I'll change the names in my version.

proofbot commented 7 years ago

Comment author: @psteckler

I've committed a fix, please try it!

proofbot commented 7 years ago

Comment author: @ejgallego

Problem fixed, thanks a lot Paul!