1 files changed, 150 insertions, 286 deletions

diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 42ecb75b..93ad052c 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -20,12 +20,6 @@ open Namegen
     the only one using this mode, but we try here to be as generic as
     possible, so this may change in the future... *)
 
-
-(** Comment the next line for displaying some more debug messages *)
-
-let prerr_endline _ = ()
-
-
 (** Signal handling: we postpone ^C during input and output phases,
     but make it directly raise a Sys.Break during evaluation of the request. *)
 
@@ -59,6 +53,8 @@ let init_stdout,read_stdout =
              let r = Buffer.contents out_buff in
              Buffer.clear out_buff; r)
 
+let pr_debug s =
+  if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 (** Categories of commands *)
 
@@ -73,202 +69,29 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Existential";"Instances"];
   ["Printing";"Universes"]]
 
-type command_attribute =
-    NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand
-    | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
-    | ProofEndingCommand
-
-let rec attribute_of_vernac_command = function
-  (* Control *)
-  | VernacTime com -> attribute_of_vernac_command com
-  | VernacTimeout(_,com) -> attribute_of_vernac_command com
-  | VernacFail com -> attribute_of_vernac_command com
-  | VernacList _ -> [] (* unsupported *)
-  | VernacLoad _ -> []
-
-  (* Syntax *)
-  | VernacTacticNotation _ -> []
-  | VernacSyntaxExtension _ -> []
-  | VernacDelimiters _ -> []
-  | VernacBindScope _ -> []
-  | VernacOpenCloseScope _ -> []
-  | VernacArgumentsScope _ -> []
-  | VernacInfix _ -> []
-  | VernacNotation _ -> []
-
-  (* Gallina *)
-  | VernacDefinition (_,_,DefineBody _,_) -> []
-  | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
-  | VernacStartTheoremProof _ -> [GoalStartingCommand]
-  | VernacEndProof _ -> [ProofEndingCommand]
-  | VernacExactProof _ -> [ProofEndingCommand]
-
-  | VernacAssumption _ -> []
-  | VernacInductive _ -> []
-  | VernacFixpoint _ -> []
-  | VernacCoFixpoint _ -> []
-  | VernacScheme _ -> []
-  | VernacCombinedScheme _ -> []
-
-  (* Modules *)
-  | VernacDeclareModule _ -> []
-  | VernacDefineModule _  -> []
-  | VernacDeclareModuleType _ -> []
-  | VernacInclude _ -> []
-
-  (* Gallina extensions *)
-  | VernacBeginSection _ -> []
-  | VernacEndSegment _ -> []
-  | VernacRequire _ -> []
-  | VernacImport _ -> []
-  | VernacCanonical _ -> []
-  | VernacCoercion _ -> []
-  | VernacIdentityCoercion _ -> []
-
-  (* Type classes *)
-  | VernacInstance _ -> []
-  | VernacContext _ -> []
-  | VernacDeclareInstances _ -> []
-  | VernacDeclareClass _ -> []
-
-  (* Solving *)
-  | VernacSolve _ -> [SolveCommand]
-  | VernacSolveExistential _ -> [SolveCommand]
-
-  (* Auxiliary file and library management *)
-  | VernacRequireFrom _ -> []
-  | VernacAddLoadPath _ -> []
-  | VernacRemoveLoadPath _ -> []
-  | VernacAddMLPath _ -> []
-  | VernacDeclareMLModule _ -> []
-  | VernacChdir o ->
-    (* TODO: [Chdir d] is currently not undo-able (not stored in coq state).
-       But if we register [Chdir] in the state, loading [initial.coq] will
-       wrongly cd to the compile-time directory at each coqtop launch. *)
-    if o = None then [QueryCommand] else []
-
-  (* State management *)
-  | VernacWriteState _ -> []
-  | VernacRestoreState _ -> []
-
-  (* Resetting *)
-  | VernacRemoveName _ -> [NavigationCommand]
-  | VernacResetName _ -> [NavigationCommand]
-  | VernacResetInitial -> [NavigationCommand]
-  | VernacBack _ -> [NavigationCommand]
-  | VernacBackTo _ -> [NavigationCommand]
-
-  (* Commands *)
-  | VernacDeclareTacticDefinition _ -> []
-  | VernacCreateHintDb _ -> []
-  | VernacRemoveHints _ -> []
-  | VernacHints _ -> []
-  | VernacSyntacticDefinition _ -> []
-  | VernacDeclareImplicits _ -> []
-  | VernacArguments _ -> [] 
-  | VernacDeclareReduction _ -> []
-  | VernacReserve _ -> []
-  | VernacGeneralizable _ -> []
-  | VernacSetOpacity _ -> []
-  | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
-  | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->
-      if coqide_known_option o then [KnownOptionCommand] else []
-  | VernacSetOption _ -> []
-  | VernacRemoveOption _ -> []
-  | VernacAddOption _ -> []
-  | VernacMemOption _ -> [QueryCommand]
-
-  | VernacPrintOption _ -> [QueryCommand]
-  | VernacCheckMayEval _ -> [QueryCommand]
-  | VernacGlobalCheck _ -> [QueryCommand]
-  | VernacPrint _ -> [QueryCommand]
-  | VernacSearch _ -> [QueryCommand]
-  | VernacLocate _ -> [QueryCommand]
-
-  | VernacComments _ -> [OtherStatePreservingCommand]
-  | VernacNop -> [OtherStatePreservingCommand]
-
-  (* Proof management *)
-  | VernacGoal _ -> [GoalStartingCommand]
-
-  | VernacAbort _ -> []
-  | VernacAbortAll -> [NavigationCommand]
-  | VernacRestart -> [NavigationCommand]
-  | VernacSuspend -> [NavigationCommand]
-  | VernacResume _ -> [NavigationCommand]
-  | VernacUndo _ -> [NavigationCommand]
-  | VernacUndoTo _ -> [NavigationCommand]
-  | VernacBacktrack _ -> [NavigationCommand]
-
-  | VernacFocus _ -> [SolveCommand]
-  | VernacUnfocus -> [SolveCommand]
-  | VernacShow _ -> [OtherStatePreservingCommand]
-  | VernacCheckGuard -> [OtherStatePreservingCommand]
-  | VernacProof (None, None) -> [OtherStatePreservingCommand]
-  | VernacProof _ -> []
-
-  | VernacProofMode _ -> []
-  | VernacBullet _ -> [SolveCommand]
-  | VernacSubproof _ -> [SolveCommand]
-  | VernacEndSubproof -> [SolveCommand]
-
-  (* Toplevel control *)
-  | VernacToplevelControl _ -> []
-
-  (* Extensions *)
-  | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
-  | VernacExtend _ -> []
-
-let is_vernac_navigation_command com =
-  List.mem NavigationCommand (attribute_of_vernac_command com)
-
-let is_vernac_query_command com =
-  List.mem QueryCommand (attribute_of_vernac_command com)
-
-let is_vernac_known_option_command com =
-  List.mem KnownOptionCommand (attribute_of_vernac_command com)
-
-let is_vernac_debug_command com =
-  List.mem DebugCommand (attribute_of_vernac_command com)
-
-let is_vernac_goal_printing_command com =
-  let attribute = attribute_of_vernac_command com in
-  List.mem GoalStartingCommand attribute or
-    List.mem SolveCommand attribute
-
-let is_vernac_state_preserving_command com =
-  let attribute = attribute_of_vernac_command com in
-  List.mem OtherStatePreservingCommand attribute or
-    List.mem QueryCommand attribute
-
-let is_vernac_tactic_command com =
-  List.mem SolveCommand (attribute_of_vernac_command com)
-
-let is_vernac_proof_ending_command com =
-  List.mem ProofEndingCommand (attribute_of_vernac_command com)
-
-
-(** Command history stack
-
-    We maintain a stack of the past states of the system. Each
-    successfully interpreted command adds a [reset_info] element
-    to this stack, storing what were the (label / open proofs /
-    current proof depth) just _before_ the interpretation of this
-    command. A label is just an integer (cf. BackTo and Bactrack
-    vernac commands).
-*)
-
-type reset_info = { label : int; proofs : identifier list; depth : int }
-
-let com_stk = Stack.create ()
-
-let compute_reset_info () =
-  { label = Lib.current_command_label ();
-    proofs = Pfedit.get_all_proof_names ();
-    depth = max 0 (Pfedit.current_proof_depth ()) }
-
-
-(** Interpretation (cf. [Ide_intf.interp]) *)
+let is_known_option cmd = match cmd with
+  | VernacSetOption (_,o,BoolValue true)
+  | VernacUnsetOption (_,o) -> coqide_known_option o
+  | _ -> false
+
+let is_debug cmd = match cmd with
+  | VernacSetOption (_,["Ltac";"Debug"], _) -> true
+  | _ -> false
+
+let is_query cmd = match cmd with
+  | VernacChdir None
+  | VernacMemOption _
+  | VernacPrintOption _
+  | VernacCheckMayEval _
+  | VernacGlobalCheck _
+  | VernacPrint _
+  | VernacSearch _
+  | VernacLocate _ -> true
+  | _ -> false
+
+let is_undo cmd = match cmd with
+  | VernacUndo _ | VernacUndoTo _ -> true
+  | _ -> false
 
 (** Check whether a command is forbidden by CoqIDE *)
 
@@ -276,82 +99,28 @@ let coqide_cmd_checks (loc,ast) =
   let user_error s =
     raise (Loc.Exc_located (loc, Util.UserError ("CoqIde", str s)))
   in
-  if is_vernac_debug_command ast then
+  if is_debug ast then
     user_error "Debug mode not available within CoqIDE";
-  if is_vernac_navigation_command ast then
-    user_error "Use CoqIDE navigation instead";
-  if is_vernac_known_option_command ast then
+  if is_known_option ast then
     user_error "Use CoqIDE display menu instead";
-  if is_vernac_query_command ast then
+  if is_navigation_vernac ast then
+    user_error "Use CoqIDE navigation instead";
+  if is_undo ast then
+    msgerrnl (str "Warning: rather use CoqIDE navigation instead");
+  if is_query ast then
     msgerrnl (str "Warning: query commands should not be inserted in scripts")
 
-let raw_eval_expr = Vernac.eval_expr
-
-let eval_expr loc_ast =
-  let rewind_info = compute_reset_info () in
-  raw_eval_expr loc_ast;
-  Stack.push rewind_info com_stk
+(** Interpretation (cf. [Ide_intf.interp]) *)
 
 let interp (raw,verbosely,s) =
-  if not raw then (prerr_endline "Starting interp..."; prerr_endline s);
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   let loc_ast = Vernac.parse_sentence (pa,None) in
   if not raw then coqide_cmd_checks loc_ast;
-  (* We run tactics silently, since we will query the goal state later.
-     Otherwise, we honor the IDE verbosity flag. *)
-  Flags.make_silent
-    (is_vernac_goal_printing_command (snd loc_ast) || not verbosely);
-  if raw then raw_eval_expr loc_ast else eval_expr loc_ast;
+  Flags.make_silent (not verbosely);
+  Vernac.eval_expr ~preserving:raw loc_ast;
   Flags.make_silent true;
-  if not raw then prerr_endline ("...Done with interp of : "^s);
   read_stdout ()
 
-
-(** Backtracking (cf. [Ide_intf.rewind]).
-    We now rely on the [Backtrack] command just as ProofGeneral. *)
-
-let rewind count =
-  if count = 0 then 0
-  else
-    let current_proofs = Pfedit.get_all_proof_names ()
-    in
-    (* 1) First, let's pop the history stack exactly [count] times.
-       NB: Normally, the IDE will not rewind by more than the numbers
-       of already interpreted commands, hence no risk of [Stack.Empty].
-    *)
-    let initial_target =
-      for i = 1 to count - 1 do ignore (Stack.pop com_stk) done;
-      Stack.pop com_stk
-    in
-    (* 2) Backtrack by enough additional steps to avoid re-opening proofs.
-       Typically, when a Qed has been crossed, we backtrack to the proof start.
-       NB: We cannot reach the empty stack, since the oldest [reset_info]
-       in the history cannot have opened proofs.
-    *)
-    let already_opened p = List.mem p current_proofs in
-    let rec extra_back n target =
-      if List.for_all already_opened target.proofs then n,target
-      else extra_back (n+1) (Stack.pop com_stk)
-    in
-    let extra_count, target = extra_back 0 initial_target
-    in
-    (* 3) Now that [target.proofs] is a subset of the opened proofs before
-       the rewind, we simply abort the extra proofs (if any).
-       NB: It is critical here that proofs are nested in a regular way
-       (i.e. no Resume or Suspend, as enforced above). This way, we can simply
-       count the extra proofs to abort instead of taking care of their names.
-    *)
-    let naborts = List.length current_proofs - List.length target.proofs
-    in
-    (* 4) We are now ready to call [Backtrack] *)
-    prerr_endline ("Rewind to state "^string_of_int target.label^
-		   ", proof depth "^string_of_int target.depth^
-		   ", num of aborts "^string_of_int naborts);
-    Vernacentries.vernac_backtrack target.label target.depth naborts;
-    Lib.mark_end_of_command (); (* We've short-circuited Vernac.eval_expr *)
-    extra_count
-
-
 (** Goal display *)
 
 let hyp_next_tac sigma env (id,_,ast) =
@@ -404,16 +173,17 @@ let concl_next_tac sigma concl =
 
 let process_goal sigma g =
   let env = Goal.V82.env sigma g in
+  let id = Goal.uid g in
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in
+    string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in
   let process_hyp h_env d acc =
     let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
     (string_of_ppcmds (pr_var_decl h_env d)) :: acc in
 (*           (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *)
   let hyps =
     List.rev (Environ.fold_named_context process_hyp env ~init: []) in
-  { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl }
+  { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 (*         hyps,(ccl,concl_next_tac sigma g)) *)
 
 let goals () =
@@ -472,6 +242,82 @@ let status () =
   in
   { Interface.status_path = path; Interface.status_proofname = proof }
 
+(** This should be elsewhere... *)
+let search flags =
+  let env = Global.env () in
+  let rec extract_flags name tpe subtpe mods blacklist = function
+  | [] -> (name, tpe, subtpe, mods, blacklist)
+  | (Interface.Name_Pattern s, b) :: l ->
+    let regexp =
+      try Str.regexp s
+      with _ -> Util.error ("Invalid regexp: " ^ s)
+    in
+    extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
+  | (Interface.Type_Pattern s, b) :: l ->
+    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
+    extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
+  | (Interface.SubType_Pattern s, b) :: l ->
+    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
+    extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
+  | (Interface.In_Module m, b) :: l ->
+    let path = String.concat "." m in
+    let m = Pcoq.parse_string Pcoq.Constr.global path in
+    let (_, qid) = Libnames.qualid_of_reference m in
+    let id =
+      try Nametab.full_name_module qid
+      with Not_found ->
+        Util.error ("Module " ^ path ^ " not found.")
+    in
+    extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
+  | (Interface.Include_Blacklist, b) :: l ->
+    extract_flags name tpe subtpe mods b l
+  in
+  let (name, tpe, subtpe, mods, blacklist) =
+    extract_flags [] [] [] [] false flags
+  in
+  let filter_function ref env constr =
+    let id = Names.string_of_id (Nametab.basename_of_global ref) in
+    let path = Libnames.dirpath (Nametab.path_of_global ref) in
+    let toggle x b = if x then b else not b in
+    let match_name (regexp, flag) =
+      toggle (Str.string_match regexp id 0) flag
+    in
+    let match_type (pat, flag) =
+      toggle (Matching.is_matching pat constr) flag
+    in
+    let match_subtype (pat, flag) =
+      toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag
+    in
+    let match_module (mdl, flag) =
+      toggle (Libnames.is_dirpath_prefix_of mdl path) flag
+    in
+    let in_blacklist =
+      blacklist || (Search.filter_blacklist ref env constr)
+    in
+    List.for_all match_name name &&
+    List.for_all match_type tpe &&
+    List.for_all match_subtype subtpe &&
+    List.for_all match_module mods && in_blacklist
+  in
+  let ans = ref [] in
+  let print_function ref env constr =
+    let name = Names.string_of_id (Nametab.basename_of_global ref) in
+    let make_path = Names.string_of_id in
+    let path =
+      List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref))
+    in
+    let answer = {
+      Interface.search_answer_full_path = path;
+      Interface.search_answer_base_name = name;
+      Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr);
+    } in
+    ans := answer :: !ans;
+  in
+  let () = Search.gen_filtered_search filter_function print_function in
+  !ans
+
 let get_options () =
   let table = Goptions.get_tables () in
   let fold key state accu = (key, state) :: accu in
@@ -485,13 +331,31 @@ let set_options options =
   in
   List.iter iter options
 
+let about () = {
+  Interface.coqtop_version = Coq_config.version;
+  Interface.protocol_version = Ide_intf.protocol_version;
+  Interface.release_date = Coq_config.date;
+  Interface.compile_date = Coq_config.compile_date;
+}
+
 (** Grouping all call handlers together + error handling *)
 
+exception Quit
+
 let eval_call c =
   let rec handle_exn e =
     catch_break := false;
-    let pr_exn e = string_of_ppcmds (Errors.print e) in
+    let pr_exn e = (read_stdout ())^("\n"^(string_of_ppcmds (Errors.print e))) in
     match e with
+      | Quit ->
+        (* Here we do send an acknowledgement message to prove everything went 
+          OK. *)
+        let dummy = Interface.Good () in
+        let xml_answer = Ide_intf.of_answer Ide_intf.quit dummy in
+        let () = Xml_utils.print_xml !orig_stdout xml_answer in
+        let () = flush !orig_stdout in
+        let () = pr_debug "Exiting gracefully." in
+        exit 0
       | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!"
       | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!"
       | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
@@ -508,17 +372,20 @@ let eval_call c =
     r
   in
   let handler = {
-    Interface.interp = interruptible interp;
-    Interface.rewind = interruptible rewind;
-    Interface.goals = interruptible goals;
-    Interface.evars = interruptible evars;
-    Interface.hints = interruptible hints;
-    Interface.status = interruptible status;
-    Interface.inloadpath = interruptible inloadpath;
-    Interface.get_options = interruptible get_options;
-    Interface.set_options = interruptible set_options;
-    Interface.mkcases = interruptible Vernacentries.make_cases;
-    Interface.handle_exn = handle_exn; }
+    Ide_intf.interp = interruptible interp;
+    Ide_intf.rewind = interruptible Backtrack.back;
+    Ide_intf.goals = interruptible goals;
+    Ide_intf.evars = interruptible evars;
+    Ide_intf.hints = interruptible hints;
+    Ide_intf.status = interruptible status;
+    Ide_intf.search = interruptible search;
+    Ide_intf.inloadpath = interruptible inloadpath;
+    Ide_intf.get_options = interruptible get_options;
+    Ide_intf.set_options = interruptible set_options;
+    Ide_intf.mkcases = interruptible Vernacentries.make_cases;
+    Ide_intf.quit = (fun () -> raise Quit);
+    Ide_intf.about = interruptible about;
+    Ide_intf.handle_exn = handle_exn; }
   in
   (* If the messages of last command are still there, we remove them *)
   ignore (read_stdout ());
@@ -534,9 +401,6 @@ let eval_call c =
     between coqtop and ide. With marshalling, reading an answer to
     a different request could hang the ide... *)
 
-let pr_debug s =
-  if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
-
 let fail err =
   Ide_intf.of_value (fun _ -> assert false) (Interface.Fail (None, err))
 
@@ -545,9 +409,9 @@ let loop () =
   let () = Xml_parser.check_eof p false in
   init_signal_handler ();
   catch_break := false;
-  (* ensure we have a command separator object (DOT) so that the first
-     command can be reseted. *)
-  Lib.mark_end_of_command();
+  (* We'll handle goal fetching and display in our own way *)
+  Vernacentries.enable_goal_printing := false;
+  Vernacentries.qed_display_script := false;
   try
     while true do
       let xml_answer =