aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/command_windows.ml7
-rw-r--r--ide/command_windows.mli2
-rw-r--r--ide/coq.ml53
-rw-r--r--ide/coq.mli10
-rw-r--r--ide/coqide.ml96
-rw-r--r--ide/typed_notebook.ml4
-rw-r--r--lib/lib.mllib1
-rw-r--r--lib/safe_marshal.ml11
-rw-r--r--toplevel/coqtop.ml16
-rw-r--r--toplevel/ide_blob.ml25
-rw-r--r--toplevel/ide_blob.mli3
11 files changed, 158 insertions, 70 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index beb8ebb526..1b768de9a2 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+let get_current_toplevel = ref (fun () -> Coq.dummy_coqtop)
+
class command_window () =
(* let window = GWindow.window
~allow_grow:true ~allow_shrink:true
@@ -104,9 +106,10 @@ object(self)
then com ^ " " else com ^ " " ^ entry#text ^" . "
in
try
- Coq.raw_interp Coq.dummy_coqtop phrase;
+ let curtop = !get_current_toplevel () in
+ Coq.raw_interp curtop phrase;
result#buffer#set_text
- ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout Coq.dummy_coqtop))
+ ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout curtop))
with e ->
let (s,loc) = Coq.process_exn e in
assert (Glib.Utf8.validate s);
diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index b211afabdc..24e79cb933 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -17,4 +17,4 @@ class command_window :
val command_window : unit -> command_window
-
+val get_current_toplevel : (unit -> Coq.coqtop) ref
diff --git a/ide/coq.ml b/ide/coq.ml
index f385ae0489..fecd3f2922 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -47,9 +47,8 @@ let msg m =
let msgnl m =
(msg m)^"\n"
-let init () =
- Coqtop.init_ide (List.tl (Array.to_list Sys.argv))
-
+let init () = List.tl (Array.to_list Sys.argv)
+(* Coqtop.init_ide (List.tl (Array.to_list Sys.argv))*)
let i = ref 0
@@ -83,22 +82,40 @@ let version () =
(if Mltop.is_native then "native" else "bytecode")
(if Coq_config.best="opt" then "native" else "bytecode")
-let eval_call c =
- match Ide_blob.eval_call c with
+exception Coq_failure of (Util.loc * Pp.std_ppcmds)
+
+let eval_call coqtop (c:'a Ide_blob.call) =
+ Safe_marshal.send coqtop.cin c;
+ let res = (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout in
+ match res with
| Ide_blob.Good v -> v
- | Ide_blob.Fail e -> raise e
+ | Ide_blob.Fail (l,pp) -> prerr_endline (msg pp); raise (Coq_failure (l,pp))
-let is_in_loadpath coqtop s = eval_call (Ide_blob.is_in_loadpath s)
+let is_in_loadpath coqtop s = eval_call coqtop (Ide_blob.is_in_loadpath s)
let reset_initial = Ide_blob.reinit
-let raw_interp coqtop s = eval_call (Ide_blob.raw_interp s)
+let raw_interp coqtop s = eval_call coqtop (Ide_blob.raw_interp s)
-let interp coqtop b s = eval_call (Ide_blob.interp b s)
+let interp coqtop b s = eval_call coqtop (Ide_blob.interp b s)
-let rewind coqtop i = eval_call (Ide_blob.rewind i)
+let rewind coqtop i = eval_call coqtop (Ide_blob.rewind i)
-let read_stdout coqtop = eval_call Ide_blob.read_stdout
+let read_stdout coqtop = eval_call coqtop Ide_blob.read_stdout
+
+let spawn_coqtop () =
+ let prog = Sys.argv.(0) in
+ let dir = Filename.dirname prog in
+ let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave") in
+ { cin = ic; cout = oc }
+
+let kill_coqtop coqtop = raw_interp coqtop "Quit."
+
+let reset_coqtop coqtop =
+ kill_coqtop coqtop;
+ let ni = spawn_coqtop () in
+ coqtop.cin <- ni.cin;
+ coqtop.cout <- ni.cout
module PrintOpt =
struct
@@ -120,10 +137,10 @@ struct
List.iter
(fun cmd ->
let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
- raw_interp dummy_coqtop str)
+ raw_interp coqtop str)
opt
- let enforce_hack () = Hashtbl.iter (set ()) state_hack
+ let enforce_hack coqtop = Hashtbl.iter (set coqtop) state_hack
end
let rec is_pervasive_exn = function
@@ -158,15 +175,15 @@ let print_toplevel_error exc =
let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
-type tried_tactic =
+type tried_tactic =
| Interrupted
| Success of int (* nb of goals after *)
| Failed
let goals coqtop =
- PrintOpt.enforce_hack ();
- eval_call Ide_blob.current_goals
+ PrintOpt.enforce_hack coqtop;
+ eval_call coqtop Ide_blob.current_goals
-let make_cases coqtop s = eval_call (Ide_blob.make_cases s)
+let make_cases coqtop s = eval_call coqtop (Ide_blob.make_cases s)
-let current_status coqtop = eval_call Ide_blob.current_status
+let current_status coqtop = eval_call coqtop Ide_blob.current_status
diff --git a/ide/coq.mli b/ide/coq.mli
index d50aab2802..914eb708a5 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -19,6 +19,14 @@ type coqtop
val dummy_coqtop : coqtop
+val spawn_coqtop : unit -> coqtop
+
+val kill_coqtop : coqtop -> unit
+
+val reset_coqtop : coqtop -> unit
+
+exception Coq_failure of (Util.loc * Pp.std_ppcmds)
+
module PrintOpt :
sig
type t
@@ -61,3 +69,5 @@ type tried_tactic =
val current_status : coqtop -> string
val goals : coqtop -> goals
+
+val msgnl : Pp.std_ppcmds -> string
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e8e4252780..e8198ec6fe 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -101,6 +101,7 @@ type viewable_script =
proof_view : GText.view;
message_view : GText.view;
analyzed_view : analyzed_views;
+ toplvl : Coq.coqtop;
}
@@ -181,7 +182,7 @@ let set_active_view i =
prerr_endline "entering set_active_view";
(try on_active_view (fun {tab_label=lbl} -> lbl#set_text lbl#text) with _ -> ());
session_notebook#goto_page i;
- let s = session_notebook#current_term in
+ let s = session_notebook#get_nth_term i in
s.tab_label#set_use_markup true;
s.tab_label#set_label ("<span background=\"light green\">"^s.tab_label#text^"</span>");
active_view := i;
@@ -279,6 +280,7 @@ let kill_input_view i =
v.tab_label#destroy ();
v.proof_view#destroy ();
v.message_view#destroy ();
+ Coq.kill_coqtop v.toplvl;
session_notebook#remove_page i
(*
(* XXX - beaucoups d'appels, a garder *)
@@ -289,6 +291,19 @@ let remove_current_view_page () =
let c = session_notebook#current_page in
kill_input_view c
+let print_items = [
+ ([implicit],"Display _implicit arguments",GdkKeysyms._i,false);
+ ([coercions],"Display _coercions",GdkKeysyms._c,false);
+ ([raw_matching],"Display raw _matching expressions",GdkKeysyms._m,true);
+ ([notations],"Display _notations",GdkKeysyms._n,true);
+ ([all_basic],"Display _all basic low-level contents",GdkKeysyms._a,false);
+ ([existential],"Display _existential variable instances",GdkKeysyms._e,false);
+ ([universes],"Display _universe levels",GdkKeysyms._u,false);
+ ([all_basic;existential;universes],"Display all _low-level contents",GdkKeysyms._l,false)
+]
+
+let setopts ct opts v =
+ List.iter (fun o -> set ct o v) opts
(* Reset this to None on page change ! *)
let (last_completion:(string*int*int*bool) option ref) = ref None
@@ -375,9 +390,9 @@ exception Stop of int
(* XXX *)
let activate_input i =
prerr_endline "entering activate_input";
- (try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ())
+(* (try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ())
with _ -> ());
- (session_notebook#get_nth_term i).analyzed_view#activate ();
+ (session_notebook#get_nth_term i).analyzed_view#activate (); *)
set_active_view i;
prerr_endline "exiting activate_input"
@@ -514,7 +529,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
-class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs =
+class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct =
object(self)
val input_view = _script
val input_buffer = _script#buffer
@@ -523,6 +538,7 @@ object(self)
val message_view = _mv
val message_buffer = _mv#buffer
val cmd_stack = _cs
+ val mycoqtop = _ct
val mutable is_active = false
val mutable read_only = false
val mutable filename = None
@@ -742,8 +758,9 @@ object(self)
try
Ideproof.display
(Ideproof.mode_tactic menu_callback)
- proof_view (Coq.goals Coq.dummy_coqtop)
- with e -> prerr_endline (Printexc.to_string e)
+ proof_view (Coq.goals mycoqtop)
+ with
+ | e -> prerr_endline (Printexc.to_string e)
end
method show_goals = self#show_goals_full
@@ -776,12 +793,14 @@ object(self)
try
full_goal_done <- false;
prerr_endline "Send_to_coq starting now";
- let r = Coq.interp Coq.dummy_coqtop verbosely phrase in
+ let r = Coq.interp mycoqtop verbosely phrase in
let is_complete = true in
- let msg = Coq.read_stdout Coq.dummy_coqtop in
+ let msg = Coq.read_stdout mycoqtop in
sync display_output msg;
Some (is_complete,r)
- with e ->
+ with
+ | Coq_failure (l,pp) -> Pervasives.prerr_endline (Coq.msgnl pp); None
+ | e ->
if show_error then sync display_error e;
None
@@ -974,7 +993,7 @@ object(self)
cmd_stack;
Stack.clear cmd_stack;
self#clear_message)();
- Coq.reset_initial ()
+ Coq.reset_coqtop mycoqtop
(* backtrack Coq to the phrase preceding iterator [i] *)
method backtrack_to_no_lock i =
@@ -990,7 +1009,7 @@ object(self)
in
begin
try
- prerr_endline (string_of_int (rewind Coq.dummy_coqtop (n_step 0)));
+ prerr_endline (string_of_int (Coq.rewind mycoqtop (n_step 0)));
prerr_endline (string_of_int (Stack.length cmd_stack));
sync (fun _ ->
let start =
@@ -1053,7 +1072,7 @@ object(self)
self#show_goals;
self#clear_message
in
- ignore ((rewind Coq.dummy_coqtop 1));
+ ignore ((Coq.rewind mycoqtop 1));
sync update_input ()
with
| Stack.Empty -> (* flash_info "Nothing to Undo"*)()
@@ -1117,7 +1136,7 @@ object(self)
val mutable deact_id = None
val mutable act_id = None
- method deactivate () =
+ method deactivate () = () (*
is_active <- false;
(match act_id with None -> ()
| Some id ->
@@ -1125,14 +1144,14 @@ object(self)
input_view#misc#disconnect id;
prerr_endline "DISCONNECTED old active : ";
print_id id;
- )(*;
+ );
deact_id <- Some
(input_view#event#connect#key_press self#disconnected_keypress_handler);
prerr_endline "CONNECTED inactive : ";
print_id (Option.get deact_id)*)
(* XXX *)
- method activate () =
+ method activate () = if not is_active then begin
is_active <- true;(*
(match deact_id with None -> ()
| Some id -> input_view#misc#disconnect id;
@@ -1148,11 +1167,12 @@ object(self)
with
| None -> ()
| Some f -> let dir = Filename.dirname f in
- if not (is_in_loadpath Coq.dummy_coqtop dir) then
+ if not (is_in_loadpath mycoqtop dir) then
begin
- ignore (Coq.interp Coq.dummy_coqtop false
+ ignore (Coq.interp mycoqtop false
(Printf.sprintf "Add LoadPath \"%s\". " dir))
end
+ end
method electric_handler =
input_buffer#connect#insert_text ~callback:
@@ -1340,8 +1360,10 @@ let create_session () =
GMisc.label ~text:"*scratch*" () in
let stack =
Stack.create () in
+ let ct =
+ spawn_coqtop () in
let legacy_av =
- new analyzed_view script proof message stack in
+ new analyzed_view script proof message stack ct in
let _ =
script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in
let _ =
@@ -1349,6 +1371,9 @@ let create_session () =
let _ =
GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in
let _ =
+ List.map (fun (opts,_,_,dflt) -> setopts ct opts dflt) print_items in
+ let _ = legacy_av#activate () in
+ let _ =
proof#event#connect#motion_notify ~callback:
(fun e ->
let win = match proof#get_window `WIDGET with
@@ -1376,7 +1401,8 @@ let create_session () =
proof_view=proof;
message_view=message;
analyzed_view=legacy_av;
- encoding=""
+ encoding="";
+ toplvl=ct
}
(* XXX - to be used later
@@ -2193,17 +2219,17 @@ let main files =
in
let _do_or_activate f () =
let current = session_notebook#current_term in
- let analyzed_view = current.analyzed_view in
+ let analyzed_view = current.analyzed_view in (*
if analyzed_view#is_active then begin
- prerr_endline ("view "^current.tab_label#text^"already active");
- ignore (f analyzed_view)
+ prerr_endline ("view "^current.tab_label#text^"already active"); *)
+ ignore (f analyzed_view) (*
end else
begin
flash_info "New proof started";
prerr_endline ("activating view "^current.tab_label#text);
activate_input session_notebook#current_page;
ignore (f analyzed_view)
- end
+ end *)
in
let do_or_activate f =
@@ -2211,7 +2237,8 @@ let main files =
(_do_or_activate
(fun av -> f av;
pop_info ();
- push_info (Coq.current_status Coq.dummy_coqtop)
+ let cur_ct = session_notebook#current_term.toplvl in
+ push_info (Coq.current_status cur_ct)
)
)
in
@@ -2440,8 +2467,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
(* Template for match *)
let callback () =
let w = get_current_word () in
+let cur_ct = session_notebook#current_term.toplvl in
try
- let cases = Coq.make_cases Coq.dummy_coqtop w
+ let cases = Coq.make_cases cur_ct w
in
let print c = function
| [x] -> Format.fprintf c " | %s => _@\n" x
@@ -2590,25 +2618,12 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
~accel_group
~accel_modi:!current.modifier_for_display
in
-
- let print_items = [
- ([implicit],"Display _implicit arguments",GdkKeysyms._i,false);
- ([coercions],"Display _coercions",GdkKeysyms._c,false);
- ([raw_matching],"Display raw _matching expressions",GdkKeysyms._m,true);
- ([notations],"Display _notations",GdkKeysyms._n,true);
- ([all_basic],"Display _all basic low-level contents",GdkKeysyms._a,false);
- ([existential],"Display _existential variable instances",GdkKeysyms._e,false);
- ([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 Coq.dummy_coqtop o v) opts in
let _ =
List.map
(fun (opts,text,key,dflt) ->
- setopts opts dflt;
view_factory#add_check_item ~key ~active:dflt text
~callback:(fun v -> do_or_activate (fun a ->
- setopts opts v;
+ setopts session_notebook#current_term.toplvl opts v;
a#show_goals) ()))
print_items
in
@@ -3068,7 +3083,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let f = if Filename.check_suffix f ".v" then f else f^".v" in
load_file (fun s -> print_endline s; exit 1) f)
files;
- activate_input 0
+ activate_input 0
end
else
begin
@@ -3078,6 +3093,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
end;
initial_about session_notebook#current_term.proof_view#buffer;
!show_toolbar !current.show_toolbar;
+ Command_windows.get_current_toplevel := (fun () -> session_notebook#current_term.toplvl);
session_notebook#current_term.script#misc#grab_focus ()
;;
diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index bd26bab273..ad122ee2bd 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -54,7 +54,9 @@ object(self)
method pages = term_list
- method current_term = List.nth term_list super#current_page
+ method current_term =
+ List.nth term_list super#current_page
+
end
let create build =
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 86d29c4be6..b5db04d213 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -25,3 +25,4 @@ Heap
Option
Dnet
Store
+Safe_marshal
diff --git a/lib/safe_marshal.ml b/lib/safe_marshal.ml
index e9ba81b499..0ae5245d7f 100644
--- a/lib/safe_marshal.ml
+++ b/lib/safe_marshal.ml
@@ -5,6 +5,15 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(*
+let uuencode s =
+ let norm_s = s ^ (String.make (String.length s mod 3) '\000') in
+ let rec y f x = f (y f) x in
+ let chop rem = function
+ | "" -> []
+ | s -> String.sub s 0 3 :: (rem (String.sub s 3 (String.length (s - 3)))) in
+ let chunks = y chop norm_s in
+ *)
let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i)
let bohcnv = Array.init 256 (fun i -> i -
@@ -13,7 +22,7 @@ let bohcnv = Array.init 256 (fun i -> i -
(if 0x61 <= i then 0x20 else 0))
let hex_of_bin ch = hobcnv.(int_of_char ch)
-let bin_of_hex s = bohcnv.(char_of_int s[0]) * 16 + bohcnv.(char_of_int s[1])
+let bin_of_hex s = char_of_int (bohcnv.(int_of_char s.[0]) * 16 + bohcnv.(int_of_char s.[1]))
let send cout expr =
let mshl_expr = Marshal.to_string expr [] in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 74c4ff3db8..440d362807 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -150,6 +150,7 @@ let usage () =
let warning s = msg_warning (str s)
+let ide_slave = ref false
let ide_args = ref []
let parse_args arglist =
@@ -287,6 +288,8 @@ let parse_args arglist =
| "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
+ | "-ideslave" :: rem -> ide_slave := true; parse rem
+
| s :: rem ->
ide_args := s :: !ide_args;
parse rem
@@ -308,6 +311,12 @@ let init arglist =
begin
try
parse_args arglist;
+ if !ide_args <> [] then usage ();
+ if !ide_slave then begin
+ Flags.make_silent true;
+ Pfedit.set_undo (Some 5000);
+ Ide_blob.init_stdout ()
+ end;
if_verbose print_header ();
init_load_path ();
inputstate ();
@@ -342,13 +351,14 @@ let init_ide arglist =
Flags.make_silent true;
Pfedit.set_undo (Some 5000);
Ide_blob.init_stdout ();
- init arglist;
List.rev !ide_args
let start () =
init_toplevel (List.tl (Array.to_list Sys.argv));
- if !ide_args <> [] then usage ();
- Toplevel.loop();
+ if !ide_slave then
+ Ide_blob.loop ()
+ else
+ Toplevel.loop();
(* Initialise and launch the Ocaml toplevel *)
Coqinit.init_ocaml_path();
Mltop.ocaml_toploop();
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index a312b0037b..899cee1e46 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -403,7 +403,9 @@ let concl_next_tac sigma concl =
])
let current_goals () =
- let pfts = Pfedit.get_pftreestate () in
+ let pfts =
+ Proof_global.give_me_the_proof ()
+ in
let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in
if all_goals = [] then
begin
@@ -524,12 +526,14 @@ type 'a call =
type 'a value =
| Good of 'a
- | Fail of exn
+ | Fail of (Util.loc * Pp.std_ppcmds)
let eval_call c =
+ let null_formatter = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in
let filter_compat_exn = function
| Vernac.DuringCommandInterp (loc,inner)
| Vernacexpr.DuringSyntaxChecking (loc,inner) -> inner
+ | Vernacexpr.Quit -> raise Vernacexpr.Quit
| e -> e
in
try Good (match c with
@@ -541,7 +545,11 @@ let eval_call c =
| Cur_goals -> Obj.magic (current_goals ())
| Cur_status -> Obj.magic (current_status ())
| Cases s -> Obj.magic (make_cases s))
- with e -> Fail (filter_compat_exn e)
+ with e ->
+ let (l,pp) = explain_exn (filter_compat_exn e) in
+ (* force evaluation of format stream *)
+ Pp.msg_with null_formatter pp;
+ Fail (l,pp)
let is_in_loadpath s : bool call =
In_loadpath s
@@ -568,3 +576,14 @@ let make_cases s : string list list call =
Cases s
(* End of wrappers *)
+
+let loop () =
+ try
+ while true do
+ let q = (Safe_marshal.receive: in_channel -> 'a call) stdin in
+ let r = eval_call q in
+ Safe_marshal.send stdout r
+ done
+ with
+ | Vernacexpr.Quit -> exit 0
+ | _ -> exit 1
diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli
index c74d67f2ce..561821b563 100644
--- a/toplevel/ide_blob.mli
+++ b/toplevel/ide_blob.mli
@@ -23,7 +23,7 @@ type 'a call
type 'a value =
| Good of 'a
- | Fail of exn
+ | Fail of (Util.loc * Pp.std_ppcmds)
val eval_call : 'a call -> 'a value
@@ -43,3 +43,4 @@ val current_goals : goals call
val read_stdout : string call
+val loop : unit -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:39:53 +0000