aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/fake_ide.ml13
-rw-r--r--ide/idetop.ml47
-rw-r--r--ide/preferences.ml34
3 files changed, 43 insertions, 51 deletions
diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml
index 521aff6bf6..8b0c736f50 100644
--- a/ide/fake_ide.ml
+++ b/ide/fake_ide.ml
@@ -11,7 +11,7 @@
(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *)
let error s =
- prerr_endline ("fake_id: error: "^s);
+ prerr_endline ("fake_ide: error: "^s);
exit 1
let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
@@ -22,7 +22,7 @@ type coqtop = {
}
let print_error msg =
- Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg
+ Format.eprintf "fake_ide: error: @[%a@]\n%!" Pp.pp_with msg
let base_eval_call ?(print=true) ?(fail=true) call coqtop =
if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -257,10 +257,15 @@ let eval_print l coq =
eval_call (wait ()) coq
| [ Tok(_,"JOIN") ] ->
eval_call (status true) coq
+ | [ Tok(_,"FAILJOIN") ] ->
+ after_fail coq (base_eval_call ~fail:false (status true) coq)
| [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
let to_id, _ = get_id id in
if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
else prerr_endline "Good tip"
+ | [ Tok(_,"ABORT") ] ->
+ prerr_endline "Quitting fake_ide";
+ exit 0
| Tok("#[^\n]*",_) :: _ -> ()
| _ -> error "syntax error"
@@ -276,6 +281,8 @@ let grammar =
; Seq [Item (eat_rex "JOIN")]
; Seq [Item (eat_rex "GOALS")]
; Seq [Item (eat_rex "FAILGOALS")]
+ ; Seq [Item (eat_rex "FAILJOIN")]
+ ; Seq [Item (eat_rex "ABORT")]
; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]
; Item (eat_rex "#[^\n]*")
]
@@ -305,6 +312,8 @@ let main =
Array.of_list (def_args @ ct), f
| _ -> usage () in
let inc = if input_file = "-" then stdin else open_in input_file in
+ prerr_endline ("Running: "^idetop_name^" "^
+ (String.concat " " (Array.to_list coqtop_args)));
let coq =
let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in
let ip = Xml_parser.make (Xml_parser.SChannel cin) in
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 6a4c7603ee..716a942d5c 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -196,12 +196,24 @@ let process_goal sigma g =
(Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
{ Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
-let export_pre_goals pgs =
- {
- Interface.fg_goals = pgs.Proof.fg_goals;
- Interface.bg_goals = pgs.Proof.bg_goals;
- Interface.shelved_goals = pgs.Proof.shelved_goals;
- Interface.given_up_goals = pgs.Proof.given_up_goals
+let process_goal_diffs diff_goal_map oldp nsigma ng =
+ let open Evd in
+ let og_s = match oldp with
+ | Some oldp ->
+ let Proof.{ sigma=osigma } = Proof.data oldp in
+ (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma }
+ with Not_found -> None)
+ | None -> None
+ in
+ let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
+ { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
+
+let export_pre_goals Proof.{ sigma; goals; stack; shelf; given_up } process =
+ let process = List.map (process sigma) in
+ { Interface.fg_goals = process goals
+ ; Interface.bg_goals = List.(map (fun (lg,rg) -> process lg, process rg)) stack
+ ; Interface.shelved_goals = process shelf
+ ; Interface.given_up_goals = process given_up
}
let goals () =
@@ -212,22 +224,9 @@ let goals () =
if Proof_diffs.show_diffs () then begin
let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
-
- let process_goal_diffs nsigma ng =
- let open Evd in
- let og_s = match oldp with
- | Some oldp ->
- let (_,_,_,_,osigma) = Proof.proof oldp in
- (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma }
- with Not_found -> None) (* will appear as a new goal *)
- | None -> None
- in
- let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
- { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
- in
- Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
+ Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp))
end else
- Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+ Some (export_pre_goals Proof.(data newp) process_goal)
with Proof_global.NoCurrentProof -> None;;
let evars () =
@@ -235,7 +234,7 @@ let evars () =
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
let pfts = Proof_global.give_me_the_proof () in
- let all_goals, _, _, _, sigma = Proof.proof pfts in
+ let Proof.{ sigma } = Proof.data pfts in
let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
let el = List.map map_evar exl in
@@ -245,8 +244,8 @@ let evars () =
let hints () =
try
let pfts = Proof_global.give_me_the_proof () in
- let all_goals, _, _, _, sigma = Proof.proof pfts in
- match all_goals with
+ let Proof.{ goals; sigma } = Proof.data pfts in
+ match goals with
| [] -> None
| g :: _ ->
let env = Goal.V82.env sigma g in
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 045d650c1c..4aa8c92f73 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -815,33 +815,20 @@ let configure ?(apply=(fun () -> ())) parent =
custom ~label box callback true
in
-(*
- let show_toolbar =
- bool
- ~f:(fun s ->
- current.show_toolbar <- s;
- !show_toolbar s)
- "Show toolbar" current.show_toolbar
- in
let window_height =
string
- ~f:(fun s -> current.window_height <- (try int_of_string s with _ -> 600);
- !resize_window ();
- )
- "Window height"
- (string_of_int current.window_height)
+ ~f:(fun s -> try window_height#set (int_of_string s) with _ -> ())
+ "Default window height at starting time"
+ (string_of_int window_height#get)
in
+
let window_width =
string
- ~f:(fun s -> current.window_width <-
- (try int_of_string s with _ -> 800))
- "Window width"
- (string_of_int current.window_width)
+ ~f:(fun s -> try window_width#set (int_of_string s) with _ -> ())
+ "Default window width at starting time"
+ (string_of_int window_width#get)
in
-*)
-(*
- let config_appearance = [show_toolbar; window_width; window_height] in
-*)
+
let global_auto_revert = pbool "Enable global auto revert" global_auto_revert in
let global_auto_revert_delay =
string
@@ -1049,10 +1036,7 @@ let configure ?(apply=(fun () -> ())) parent =
Section("Project", Some (`STOCK "gtk-page-setup"),
[project_file_name;read_project;
]);
-(*
- Section("Appearance",
- config_appearance);
-*)
+ Section("Appearance", Some `PREFERENCES, [window_width; window_height]);
Section("Externals", None,
[cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
cmd_print;cmd_editor;cmd_browse;doc_url;library_url]);
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:43:16 +0000