Changing types to reflect futur separation between toplevel and ide.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12880 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 45 insertions, 102 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index ee07b3fb81..f6ef42221c 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -106,7 +106,7 @@ object(self)
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
       try
-	ignore(Coq.interp false phrase);
+	ignore(Coq.interp Coq.dummy_coqtop false phrase);
 	result#buffer#set_text
 	  ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ())
       with e ->
diff --git a/ide/coq.ml b/ide/coq.ml
index 954fbfa02b..87f0c35e65 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -27,6 +27,10 @@ open Termops
 open Namegen
 open Ideutils
 
+type coqtop = unit
+
+let dummy_coqtop = ()
+
 let prerr_endline s = if !debug then prerr_endline s else ()
 
 let output = ref (Format.formatter_of_out_channel stdout)
@@ -83,33 +87,9 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
-let is_in_coq_lib dir =
-  prerr_endline ("Is it a coq theory ? : "^dir);
-  let is_same_file = same_file dir in
-  List.exists
-    (fun s ->
-      let fdir =
-        Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in
-      prerr_endline (" Comparing to: "^fdir);
-      if is_same_file fdir then (prerr_endline " YES";true)
-      else (prerr_endline"NO";false))
-    Coq_config.theories_dirs
-
-let is_in_loadpath dir =
+let is_in_loadpath coqtop dir =
   Library.is_in_load_paths (System.physical_path_of_string dir)
 
-let is_in_coq_path f =
-  try
-  let base = Filename.chop_extension (Filename.basename f) in
-  let _ = Library.locate_qualified_library false
-	    (Libnames.make_qualid Names.empty_dirpath
-	       (Names.id_of_string base)) in
-  prerr_endline (f ^ " is in coq path");
-  true
-  with _ ->
-    prerr_endline (f ^ " is NOT in coq path");
-    false
-
 let is_in_proof_mode () =
   match Decl_mode.get_current_mode () with
       Decl_mode.Mode_none -> false
@@ -118,7 +98,6 @@ let is_in_proof_mode () =
 let user_error_loc l s =
   raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
 
-
 let known_options = ref []
 
 let prepare_option (l,dft) =
@@ -300,10 +279,6 @@ let is_vernac_tactic_command com =
 let is_vernac_proof_ending_command com =
   List.mem ProofEndingCommand (attribute_of_vernac_command com)
 
-type annotated_vernac =
-  | ControlVernac of vernac_expr * string (* navigation, debug, process control, print opts *)
-  | PureVernac of vernac_expr
- 
 type reset_status =
   | NoReset
   | ResetToNextMark
@@ -321,18 +296,11 @@ let com_stk = Stack.create ()
 let parsable_of_string s =
   Pcoq.Gram.parsable (Stream.of_string s)
 
-let reset_initial () =
+let reset_initial coqtop =
   prerr_endline "Reset initial called"; flush stderr;
   Stack.clear com_stk;
   Vernacentries.abort_refine Lib.reset_initial ()
 
-let reset_to sp =
-      prerr_endline
-        ("Reset called with state "^(Libnames.string_of_path (fst sp)));
-      Lib.reset_to_state sp
-
-let undo_info () = Pfedit.get_all_proof_names ()
-
 let compute_reset_info loc_ast = 
   let status,cur_prf = match snd loc_ast with
     | com when is_vernac_tactic_command com ->
@@ -359,7 +327,7 @@ let eval_expr cmd_stk loc_ast =
   Stack.push rewind_info cmd_stk;
   Stack.length cmd_stk
 
-let interp_with_options verbosely s =
+let interp coqtop verbosely s =
   prerr_endline "Starting interp...";
   prerr_endline s;
   let pa = parsable_of_string s in
@@ -386,9 +354,9 @@ let interp_with_options verbosely s =
     stack_depth
   with Vernac.End_of_input -> assert false
 
-let rewind count =
+let rewind coqtop count =
   let undo_ops = Hashtbl.create 31 in
-  let current_proofs = undo_info () in
+  let current_proofs = Pfedit.get_all_proof_names () in
   let rec do_rewind count reset_op prev_proofs curprf =
     if (count <= 0) && (reset_op <> ResetToNextMark) &&
        (Util.list_subset prev_proofs current_proofs) then
@@ -456,7 +424,7 @@ struct
   let _ = List.iter (fun opt -> Hashtbl.add state_hack opt false)
             [ implicit; coercions; raw_matching; notations; all_basic; existential; universes ]
 
-  let set opt value =
+  let set coqtop opt value =
     Hashtbl.replace state_hack opt value;
     List.iter
       (fun cmd -> 
@@ -464,7 +432,7 @@ struct
          Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string str,None)))
       opt
 
-  let enforce_hack () = Hashtbl.iter set state_hack 
+  let enforce_hack () = Hashtbl.iter (set ()) state_hack 
 end
 
 (*
@@ -472,15 +440,6 @@ let forbid_vernac blacklist (loc,vernac) =
   List.map (fun (test,err) -> if test vernac then err loc
  *)
 
-
-let interp verbosely phrase =
-  interp_with_options verbosely phrase
-
-let interp_and_replace s =
-  let result = interp false s in
-  let msg = read_stdout () in
-  result,msg
-
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e
@@ -576,7 +535,7 @@ let concl_next_tac concl =
     "right"
   ])
 
-let goals () =
+let goals coqtop =
   PrintOpt.enforce_hack ();
   let pfts = Pfedit.get_pftreestate () in
   let sigma = Tacmach.evc_of_pftreestate pfts in
@@ -612,7 +571,7 @@ let id_of_name = function
   | Names.Anonymous -> id_of_string "x"
   | Names.Name x -> x
 
-let make_cases s =
+let make_cases coqtop s =
   let qualified_name = Libnames.qualid_of_string s in
   let glob_ref = Nametab.locate qualified_name in
   match glob_ref with
@@ -642,7 +601,7 @@ let make_cases s =
 	  []
     | _ -> raise Not_found
 
-let current_status () =
+let current_status coqtop =
   let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
   let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
   try
diff --git a/ide/coq.mli b/ide/coq.mli
index 173bd75f7b..d30f7168f9 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -16,6 +16,10 @@ open Evd
 val short_version : unit -> string
 val version : unit -> string
 
+type coqtop
+
+val dummy_coqtop : coqtop
+
 module PrintOpt :
 sig
   type t
@@ -27,33 +31,21 @@ sig
   val existential : t
   val universes : t
 
-  val set : t -> bool -> unit
+  val set : coqtop -> t -> bool -> unit
 end
 
-
-val reset_initial : unit -> unit
+val reset_initial : coqtop -> unit
 
 val init : unit -> string list
-val interp : bool -> string -> int
-val interp_and_replace : string ->
-  int * string
-
-val rewind : int -> int
-
-val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
-val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
-val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool
-val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool
+val interp : coqtop -> bool -> string -> int
 
-(* type hyp = (identifier * constr option * constr) * string *)
+val rewind : coqtop -> int -> int
 
 val process_exn : exn -> string*(Util.loc option)
 
-val is_in_coq_lib : string -> bool
-val is_in_coq_path : string -> bool
-val is_in_loadpath : string -> bool
+val is_in_loadpath : coqtop -> string -> bool
 
-val make_cases : string -> string list list
+val make_cases : coqtop -> string -> string list list
 
 type tried_tactic =
   | Interrupted
@@ -62,7 +54,7 @@ type tried_tactic =
 
 (* Message to display in lower status bar. *)
 
-val current_status : unit -> string
+val current_status : coqtop -> string
 
 type 'a menu = 'a * (string * string) list
 
@@ -70,4 +62,4 @@ type goals =
   | Message of string
   | Goals of ((string menu) list * string menu) list
 
-val goals : unit -> goals
+val goals : coqtop -> goals
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 7f878646e2..6e80c9ae68 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -735,9 +735,9 @@ object(self)
       match Decl_mode.get_current_mode () with
           Decl_mode.Mode_none -> ()
         | Decl_mode.Mode_tactic ->
-            Proof.display (Proof.mode_tactic (fun _ _ -> ())) proof_view (Coq.goals ())
+            Proof.display (Proof.mode_tactic (fun _ _ -> ())) proof_view (Coq.goals Coq.dummy_coqtop)
         | Decl_mode.Mode_proof ->
-            Proof.display Proof.mode_cesar proof_view (Coq.goals ())
+            Proof.display Proof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop)
     with e ->
       prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
 
@@ -753,9 +753,9 @@ object(self)
                 Proof.display
                   (Proof.mode_tactic (fun s () -> ignore (self#insert_this_phrase_on_success
                                                             true true false ("progress "^s) s)))
-                  proof_view (Coq.goals ())
+                  proof_view (Coq.goals Coq.dummy_coqtop)
             | Decl_mode.Mode_proof ->
-                Proof.display Proof.mode_cesar proof_view (Coq.goals ())
+                Proof.display Proof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop)
         with e -> prerr_endline (Printexc.to_string e)
       end
 
@@ -788,19 +788,11 @@ object(self)
         full_goal_done <- false;
         prerr_endline "Send_to_coq starting now";
         Decl_mode.clear_daimon_flag ();
-        if replace then begin
-          let r,info = Coq.interp_and_replace ("info " ^ phrase) in
-          let is_complete = not (Decl_mode.get_daimon_flag ()) in
-          let msg = read_stdout () in
-            sync display_output msg;
-            Some (is_complete,r)
-        end else begin
-          let r = Coq.interp verbosely phrase in
-          let is_complete = not (Decl_mode.get_daimon_flag ()) in
-          let msg = read_stdout () in
-            sync display_output msg;
-            Some (is_complete,r)
-        end
+        let r = Coq.interp Coq.dummy_coqtop verbosely phrase in
+        let is_complete = not (Decl_mode.get_daimon_flag ()) in
+        let msg = read_stdout () in
+        sync display_output msg;
+        Some (is_complete,r)
       with e ->
         if show_error then sync display_error e;
         None
@@ -994,7 +986,7 @@ object(self)
               cmd_stack;
             Stack.clear cmd_stack;
             self#clear_message)();
-    Coq.reset_initial ()
+    Coq.reset_initial Coq.dummy_coqtop
 
   (* backtrack Coq to the phrase preceding iterator [i] *)
   method backtrack_to_no_lock i =
@@ -1010,7 +1002,7 @@ object(self)
     in
     begin
       try
-        prerr_endline (string_of_int (rewind (n_step 0)));
+        prerr_endline (string_of_int (rewind Coq.dummy_coqtop (n_step 0)));
         prerr_endline (string_of_int (Stack.length cmd_stack));
         sync (fun _ ->
                 let start =
@@ -1074,7 +1066,7 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          ignore ((rewind 1));
+          ignore ((rewind Coq.dummy_coqtop 1));
           sync update_input ()
         with
           | Stack.Empty -> (* flash_info "Nothing to Undo"*)()
@@ -1142,7 +1134,7 @@ object(self)
     is_active <- false;
     (match act_id with None -> ()
        | Some id ->
-           reset_initial ();
+           reset_initial Coq.dummy_coqtop;
            input_view#misc#disconnect id;
            prerr_endline "DISCONNECTED old active : ";
            print_id id;
@@ -1169,9 +1161,9 @@ object(self)
     with
       | None -> ()
       | Some f -> let dir = Filename.dirname f in
-          if not (is_in_loadpath dir) then
+          if not (is_in_loadpath Coq.dummy_coqtop dir) then
             begin
-              ignore (Coq.interp false
+              ignore (Coq.interp Coq.dummy_coqtop false
                         (Printf.sprintf "Add LoadPath \"%s\". "  dir))
             end
 
@@ -2242,7 +2234,7 @@ let main files =
 				    (_do_or_activate
 				       (fun av -> f av;
                                           pop_info ();
-                                          push_info (Coq.current_status())
+                                          push_info (Coq.current_status Coq.dummy_coqtop)
                                        )
                                     )
 				in
@@ -2472,7 +2464,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					let callback () =
 					  let w = get_current_word () in
 					    try
-					      let cases = Coq.make_cases w
+					      let cases = Coq.make_cases Coq.dummy_coqtop w
 					      in
 					      let print c = function
 						| [x] -> Format.fprintf c "  | %s => _@\n" x
@@ -2632,7 +2624,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
                ([universes],"Display _universe levels",GdkKeysyms._u,false);
                ([all_basic;existential;universes],"Display all _low-level contents",GdkKeysyms._l,false)
              ] in
-             let setopts opts v = List.iter (fun o -> set o v) opts in
+             let setopts opts v = List.iter (fun o -> set Coq.dummy_coqtop o v) opts in
              let _ =
                List.map
                        (fun (opts,text,key,dflt) ->