aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml28
-rw-r--r--ide/coq.mli2
-rw-r--r--ide/coqide.ml4
-rw-r--r--test-suite/ide/undo.v1
-rw-r--r--toplevel/ide_blob.ml580
-rw-r--r--toplevel/ide_blob.mli41
6 files changed, 642 insertions, 14 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 80e2da562..2db5d81b9 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -25,9 +25,15 @@ open Namegen
open Ideutils
open Compat
-type coqtop = unit
+type coqtop = {
+ mutable cout : in_channel ;
+ mutable cin : out_channel ;
+}
-let dummy_coqtop = ()
+let dummy_coqtop = {
+ cout = stdin ;
+ cin = stdout ;
+}
let prerr_endline s = if !debug then prerr_endline s else ()
@@ -77,17 +83,17 @@ let version () =
(if Mltop.is_native then "native" else "bytecode")
(if Coq_config.best="opt" then "native" else "bytecode")
-let is_in_loadpath coqtop = Ide_blob.is_in_loadpath
+let is_in_loadpath coqtop s = Ide_blob.eval_call (Ide_blob.is_in_loadpath s)
let reset_initial = Ide_blob.reinit
-let raw_interp coqtop = Ide_blob.raw_interp
+let raw_interp coqtop s = Ide_blob.eval_call (Ide_blob.raw_interp s)
-let interp coqtop = Ide_blob.interp
+let interp coqtop b s = Ide_blob.eval_call (Ide_blob.interp b s)
-let rewind coqtop = Ide_blob.rewind
+let rewind coqtop i = Ide_blob.eval_call (Ide_blob.rewind i)
-let read_stdout = Ide_blob.read_stdout
+let read_stdout coqtop = Ide_blob.eval_call Ide_blob.read_stdout
module PrintOpt =
struct
@@ -109,7 +115,7 @@ struct
List.iter
(fun cmd ->
let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
- Ide_blob.raw_interp str)
+ raw_interp dummy_coqtop str)
opt
let enforce_hack () = Hashtbl.iter (set ()) state_hack
@@ -154,8 +160,8 @@ type tried_tactic =
let goals coqtop =
PrintOpt.enforce_hack ();
- Ide_blob.current_goals ()
+ Ide_blob.eval_call Ide_blob.current_goals
-let make_cases coqtop = Ide_blob.make_cases
+let make_cases coqtop s = Ide_blob.eval_call (Ide_blob.make_cases s)
-let current_status = Ide_blob.current_status
+let current_status coqtop = Ide_blob.eval_call Ide_blob.current_status
diff --git a/ide/coq.mli b/ide/coq.mli
index 231d2dc63..d50aab280 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -33,7 +33,7 @@ sig
val set : coqtop -> t -> bool -> unit
end
-val reset_initial : coqtop -> unit
+val reset_initial : unit -> unit
val init : unit -> string list
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e49434303..e8e425278 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -974,7 +974,7 @@ object(self)
cmd_stack;
Stack.clear cmd_stack;
self#clear_message)();
- Coq.reset_initial Coq.dummy_coqtop
+ Coq.reset_initial ()
(* backtrack Coq to the phrase preceding iterator [i] *)
method backtrack_to_no_lock i =
@@ -1121,7 +1121,7 @@ object(self)
is_active <- false;
(match act_id with None -> ()
| Some id ->
- reset_initial Coq.dummy_coqtop;
+ reset_initial ();
input_view#misc#disconnect id;
prerr_endline "DISCONNECTED old active : ";
print_id id;
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v
index 84eacc3e3..ea3920551 100644
--- a/test-suite/ide/undo.v
+++ b/test-suite/ide/undo.v
@@ -79,6 +79,7 @@ Definition q := O.
Definition r := O.
(* Bug 2082 : Follow the numbers *)
+(* Broken due to proof engine rewriting *)
Variable A : Prop.
Variable B : Prop.
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
new file mode 100644
index 000000000..450a34282
--- /dev/null
+++ b/toplevel/ide_blob.ml
@@ -0,0 +1,580 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+
+
+(* All this stuff should be integrated inside Coq. Several kittens died during
+ * the operation. Reading this aloud will invoke the Great Cthulhu. *)
+
+open Vernacexpr
+open Names
+open Util
+open Pp
+open Printer
+open Namegen
+
+let prerr_endline _ = ()
+
+let coqide_known_option table = List.mem table [
+ ["Printing";"Implicit"];
+ ["Printing";"Coercions"];
+ ["Printing";"Matching"];
+ ["Printing";"Synth"];
+ ["Printing";"Notations"];
+ ["Printing";"All"];
+ ["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 _ -> []
+ | VernacDeclareInstance _ -> []
+ | VernacDeclareClass _ -> []
+
+ (* Solving *)
+ | VernacSolve _ -> [SolveCommand]
+ | VernacSolveExistential _ -> [SolveCommand]
+
+ (* Auxiliary file and library management *)
+ | VernacRequireFrom _ -> []
+ | VernacAddLoadPath _ -> []
+ | VernacRemoveLoadPath _ -> []
+ | VernacAddMLPath _ -> []
+ | VernacDeclareMLModule _ -> []
+ | VernacChdir _ -> [OtherStatePreservingCommand]
+
+ (* State management *)
+ | VernacWriteState _ -> []
+ | VernacRestoreState _ -> []
+
+ (* Resetting *)
+ | VernacRemoveName _ -> [NavigationCommand]
+ | VernacResetName _ -> [NavigationCommand]
+ | VernacResetInitial -> [NavigationCommand]
+ | VernacBack _ -> [NavigationCommand]
+ | VernacBackTo _ -> [NavigationCommand]
+
+ (* Commands *)
+ | VernacDeclareTacticDefinition _ -> []
+ | VernacCreateHintDb _ -> []
+ | VernacHints _ -> []
+ | VernacSyntacticDefinition _ -> []
+ | VernacDeclareImplicits _ -> []
+ | 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 _ -> [NavigationCommand]
+ | VernacAbortAll -> [NavigationCommand]
+ | VernacRestart -> [NavigationCommand]
+ | VernacSuspend -> [NavigationCommand]
+ | VernacResume _ -> [NavigationCommand]
+ | VernacUndo _ -> [NavigationCommand]
+ | VernacUndoTo _ -> [NavigationCommand]
+ | VernacBacktrack _ -> [NavigationCommand]
+
+ | VernacFocus _ -> [SolveCommand]
+ | VernacUnfocus -> [SolveCommand]
+ | VernacGo _ -> []
+ | VernacShow _ -> [OtherStatePreservingCommand]
+ | VernacCheckGuard -> [OtherStatePreservingCommand]
+ | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
+ | VernacProof _ -> []
+
+ | VernacProofMode _ -> []
+ | VernacSubproof _ -> []
+ | VernacEndSubproof -> []
+
+ (* Toplevel control *)
+ | VernacToplevelControl _ -> []
+
+ (* Extensions *)
+ | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
+ | VernacExtend _ -> []
+
+let is_vernac_goal_starting_command com =
+ List.mem GoalStartingCommand (attribute_of_vernac_command com)
+
+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)
+
+(* End of Necronomicon exerpts *)
+
+type reset_status =
+ | NoReset
+ | ResetToNextMark
+ | ResetAtMark of Libnames.object_name
+
+type reset_info = {
+ status : reset_status;
+ proofs : identifier list;
+ cur_prf : (identifier * int) option;
+ loc_ast : Util.loc * Vernacexpr.vernac_expr;
+}
+
+let com_stk = Stack.create ()
+
+let reinit () =
+ Vernacentries.abort_refine Lib.reset_initial ();
+ Stack.clear com_stk
+
+let compute_reset_info loc_ast =
+ let status,cur_prf = match snd loc_ast with
+ | com when is_vernac_tactic_command com ->
+ NoReset,Some (Pfedit.get_current_proof_name (),Pfedit.current_proof_depth ())
+ | com when is_vernac_state_preserving_command com -> NoReset,None
+ | com when is_vernac_proof_ending_command com -> ResetToNextMark,None
+ | VernacEndSegment _ -> NoReset,None
+ | _ ->
+ (match Lib.has_top_frozen_state () with
+ | Some sp ->
+ prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
+ ResetAtMark sp,None
+ | None -> prerr_endline "No top state"; (NoReset,None))
+ in
+ { status = status;
+ proofs = Pfedit.get_all_proof_names ();
+ cur_prf = cur_prf;
+ loc_ast = loc_ast;
+ }
+
+let parsable_of_string s =
+ Pcoq.Gram.parsable (Stream.of_string s)
+
+let eval_expr loc_ast =
+ let rewind_info = compute_reset_info loc_ast in
+ Vernac.eval_expr loc_ast;
+ Stack.push rewind_info com_stk;
+ Stack.length com_stk
+
+let raw_interp s =
+ Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string s,None))
+
+let user_error_loc l s =
+ raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
+
+let interp verbosely s =
+ prerr_endline "Starting interp...";
+ prerr_endline s;
+ let pa = parsable_of_string s in
+ try
+ let (loc,vernac) = Vernac.parse_sentence (pa,None) in
+ (* Temporary hack to make coqide.byte work (WTF???) - now with
+ * less screen
+ * * pollution *)
+ Pervasives.prerr_string " \r"; Pervasives.flush stderr;
+ if is_vernac_debug_command vernac then
+ user_error_loc loc (str "Debug mode not available within CoqIDE");
+ if is_vernac_navigation_command vernac then
+ user_error_loc loc (str "Use CoqIDE navigation instead");
+ if is_vernac_known_option_command vernac then
+ user_error_loc loc (str "Use CoqIDE display menu instead");
+ if is_vernac_query_command vernac then
+ user_error_loc loc (str "Warning: query commands should not be inserted in scripts");
+ if not (is_vernac_goal_printing_command vernac) then
+ (* Verbose if in small step forward and not a tactic *)
+ Flags.make_silent (not verbosely);
+ let stack_depth = eval_expr (loc,vernac) in
+ Flags.make_silent true;
+ prerr_endline ("...Done with interp of : "^s);
+ stack_depth
+ with Vernac.End_of_input -> assert false
+
+let rewind count =
+ let undo_ops = Hashtbl.create 31 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
+ (* We backtracked at least what we wanted to, we have no
+ * proof to reopen, and we don't need to find a reset mark *)
+ begin
+ Hashtbl.iter
+ (fun id depth ->
+ if List.mem id prev_proofs then begin
+ Pfedit.suspend_proof ();
+ Pfedit.resume_proof (Util.dummy_loc,id);
+ Pfedit.undo_todepth depth
+ end)
+ undo_ops;
+ prerr_endline "OK for undos";
+ Option.iter (fun id -> if List.mem id prev_proofs then
+ Pfedit.suspend_proof ();
+ Pfedit.resume_proof (Util.dummy_loc,id)) curprf;
+ prerr_endline "OK for focusing";
+ List.iter
+ (fun id -> Pfedit.delete_proof (Util.dummy_loc,id))
+ (Util.list_subtract current_proofs prev_proofs);
+ prerr_endline "OK for aborts";
+ (match reset_op with
+ | NoReset -> prerr_endline "No Reset"
+ | ResetAtMark m -> (prerr_endline ("Reset at "^(Libnames.string_of_path (fst m))); Lib.reset_to_state m)
+ | ResetToNextMark -> assert false);
+ prerr_endline "OK for reset"
+ end
+ else
+ begin
+ prerr_endline "pop";
+ let coq = Stack.pop com_stk in
+ let curprf =
+ Option.map
+ (fun (curprf,depth) ->
+ (if Hashtbl.mem undo_ops curprf then Hashtbl.replace else Hashtbl.add)
+ undo_ops curprf depth;
+ curprf)
+ coq.cur_prf in
+ do_rewind (pred count)
+ (if coq.status <> NoReset then coq.status else reset_op) coq.proofs curprf;
+ if count <= 0 then begin
+ (* we had to backtrack further to find a suitable
+ * anchor point, replaying *)
+ prerr_endline "push";
+ ignore (eval_expr coq.loc_ast);
+ end
+ end
+ in
+ do_rewind count NoReset current_proofs None;
+ Stack.length com_stk
+
+let is_in_loadpath dir =
+ Library.is_in_load_paths (System.physical_path_of_string dir)
+
+let string_of_ppcmds c =
+ Pp.msg_with Format.str_formatter c;
+ Format.flush_str_formatter ()
+
+type 'a menu = 'a * (string * string) list
+
+type goals =
+ | Message of string
+ | Goals of ((string menu) list * string menu) list
+
+let hyp_next_tac sigma env (id,_,ast) =
+ let id_s = Names.string_of_id id in
+ let type_s = string_of_ppcmds (pr_ltype_env env ast) in
+ [
+ ("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")
+ ] @ (if Hipattern.is_equality_type ast then [
+ ("discriminate "^id_s),("discriminate "^id_s^".\n");
+ ("injection "^id_s),("injection "^id_s^".\n")
+ ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [
+ ("rewrite "^id_s),("rewrite "^id_s^".\n");
+ ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n")
+ ] else []) @ [
+ ("elim "^id_s), ("elim "^id_s^".\n");
+ ("inversion "^id_s), ("inversion "^id_s^".\n");
+ ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n")
+ ]
+
+let concl_next_tac sigma concl =
+ let expand s = (s,s^".\n") in
+ List.map expand ([
+ "intro";
+ "intros";
+ "intuition"
+ ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [
+ "reflexivity";
+ "discriminate";
+ "symmetry"
+ ] else []) @ [
+ "assumption";
+ "omega";
+ "ring";
+ "auto";
+ "eauto";
+ "tauto";
+ "trivial";
+ "decide equality";
+ "simpl";
+ "subst";
+ "red";
+ "split";
+ "left";
+ "right"
+ ])
+
+let current_goals () =
+ let pfts = Pfedit.get_pftreestate () in
+ let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in
+ if all_goals = [] then
+ begin
+ Message (string_of_ppcmds (
+ let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
+ match bgoals with
+ | [] ->
+ let exl = Evarutil.non_instantiated sigma in
+ (str (if exl = [] then "Proof Completed." else
+ "No more subgoals but non-instantiated existential variables:") ++
+ (fnl ()) ++ (pr_evars_int 1 exl))
+ | _ ->
+ Util.list_fold_left_i
+ (fun i a g ->
+ a ++ (Printer.pr_concl i sigma g) ++ (spc ())) 1
+ (str "This subproof is complete, but there are still unfocused goals:" ++ (fnl ()))
+ bgoals))
+
+ end
+ else
+ begin
+ let process_goal g =
+ let env = Goal.V82.env sigma 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
+ 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), hyp_next_tac sigma h_env d)::acc in
+ let hyps =
+ List.rev (Environ.fold_named_context process_hyp env ~init:[]) in
+ (hyps,(ccl,concl_next_tac sigma g))
+ in
+ Goals (List.map process_goal all_goals)
+ end
+
+(*
+ let pfts = Proof_global.give_me_the_proof () in
+ let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals pfts in
+ if goals = [] then
+ begin
+ Message (string_of_ppcmds (
+ let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
+ match bgoals with
+ | [] ->
+ let exl = Evarutil.non_instantiated sigma in
+ (str (if exl = [] then "Proof Completed." else
+ "No more subgoals but non-instantiated existential variables:") ++
+ (fnl ()) ++ (pr_evars_int 1 exl))
+ | _ ->
+ Util.list_fold_left_i
+ (fun i a g ->
+ a ++ (Printer.pr_concl i sigma g) ++ (spc ())) 1
+ (str "This subproof is complete, but there are still unfocused goals:" ++ (fnl ()))
+ bgoals))
+ end
+ else
+ begin
+ let process_goal gs =
+ let (g,sigma) = Goal.V82.nf_evar sigma gs in
+ let env = Goal.V82.unfiltered_env sigma g in
+ let ccl =
+ string_of_ppcmds (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) in
+ let process_hyp h_env d acc =
+ (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
+ (hyps,(ccl,concl_next_tac gs))
+ in
+ Goals (List.map process_goal all_goals)
+ end
+ *)
+
+
+let id_of_name = function
+ | Names.Anonymous -> id_of_string "x"
+ | Names.Name x -> x
+
+let make_cases s =
+ let qualified_name = Libnames.qualid_of_string s in
+ let glob_ref = Nametab.locate qualified_name in
+ match glob_ref with
+ | Libnames.IndRef i ->
+ let {Declarations.mind_nparams = np},
+ {Declarations.mind_consnames = carr ;
+ Declarations.mind_nf_lc = tarr }
+ = Global.lookup_inductive i
+ in
+ Util.array_fold_right2
+ (fun n t l ->
+ let (al,_) = Term.decompose_prod t in
+ let al,_ = Util.list_chop (List.length al - np) al in
+ let rec rename avoid = function
+ | [] -> []
+ | (n,_)::l ->
+ let n' = next_ident_away_in_goal
+ (id_of_name n)
+ avoid
+ in (string_of_id n')::(rename (n'::avoid) l)
+ in
+ let al' = rename [] (List.rev al) in
+ (string_of_id n :: al') :: l
+ )
+ carr
+ tarr
+ []
+ | _ -> raise Not_found
+
+let current_status () =
+ let path = string_of_ppcmds (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
+ path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
+ with _ -> path
+
+let init_stdout,read_stdout =
+ let out_buff = Buffer.create 100 in
+ let out_ft = Format.formatter_of_buffer out_buff in
+ let deep_out_ft = Format.formatter_of_buffer out_buff in
+ let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in
+ (fun () ->
+ Pp_control.std_ft := out_ft;
+ Pp_control.err_ft := out_ft;
+ Pp_control.deep_ft := deep_out_ft;
+ ),
+ (fun () -> Format.pp_print_flush out_ft ();
+ let r = Buffer.contents out_buff in
+ Buffer.clear out_buff; r)
+
+type 'a call =
+ | In_loadpath of string
+ | Raw_interp of string
+ | Interp of bool * string
+ | Rewind of int
+ | Read_stdout
+ | Cur_goals
+ | Cur_status
+ | Cases of string
+
+
+let eval_call = function
+ | In_loadpath s -> Obj.magic (is_in_loadpath s)
+ | Raw_interp s -> Obj.magic (raw_interp s)
+ | Interp (b,s) -> Obj.magic (interp b s)
+ | Rewind i -> Obj.magic (rewind i)
+ | Read_stdout -> Obj.magic (read_stdout ())
+ | Cur_goals -> Obj.magic (current_goals ())
+ | Cur_status -> Obj.magic (current_status ())
+ | Cases s -> Obj.magic (make_cases s)
+
+
+let is_in_loadpath s : bool call =
+ In_loadpath s
+
+let raw_interp s : unit call =
+ Raw_interp s
+
+let interp b s : int call =
+ Interp (b,s)
+
+let rewind i : int call =
+ Rewind i
+
+let read_stdout : string call =
+ Read_stdout
+
+let current_goals : goals call =
+ Cur_goals
+
+let current_status : string call =
+ Cur_status
+
+let make_cases s : string list list call =
+ Cases s
diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli
new file mode 100644
index 000000000..15fec4523
--- /dev/null
+++ b/toplevel/ide_blob.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+
+type 'a menu = 'a * (string * string) list
+
+type goals =
+ | Message of string
+ | Goals of ((string menu) list * string menu) list
+
+val reinit : unit -> unit
+
+val init_stdout : unit -> unit
+
+type 'a call
+
+val eval_call : 'a call -> 'a
+
+val raw_interp : string -> unit call
+
+val interp : bool -> string -> int call
+
+val rewind : int -> int call
+
+val is_in_loadpath : string -> bool call
+
+val make_cases : string -> string list list call
+
+val current_status : string call
+
+val current_goals : goals call
+
+val read_stdout : string call
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 18:20:40 +0000