summaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/.merlin.in (renamed from ide/.merlin)2
-rw-r--r--ide/MacOS/default_accel_map1
-rwxr-xr-xide/MacOS/relatify_with-respect-to_.sh15
-rw-r--r--ide/configwin.ml (renamed from ide/utils/configwin.ml)0
-rw-r--r--ide/configwin.mli (renamed from ide/utils/configwin.mli)0
-rw-r--r--ide/configwin_ihm.ml (renamed from ide/utils/configwin_ihm.ml)0
-rw-r--r--ide/configwin_ihm.mli (renamed from ide/utils/configwin_ihm.mli)0
-rw-r--r--ide/configwin_messages.ml (renamed from ide/utils/configwin_messages.ml)0
-rw-r--r--ide/configwin_types.ml (renamed from ide/utils/configwin_types.mli)0
-rw-r--r--ide/coq.ml51
-rw-r--r--ide/coq.mli10
-rw-r--r--ide/coq_commands.ml1
-rw-r--r--ide/coq_lex.mll6
-rw-r--r--ide/coqide.ml25
-rw-r--r--ide/coqide_ui.ml5
-rw-r--r--ide/gtk_parsing.ml7
-rw-r--r--ide/ide.mllib8
-rw-r--r--ide/ide_common.mllib (renamed from ide/coqidetop.mllib)1
-rw-r--r--ide/ide_slave.mli12
-rw-r--r--ide/idetop.ml (renamed from ide/ide_slave.ml)84
-rw-r--r--ide/ideutils.ml61
-rw-r--r--ide/nanoPG.ml6
-rw-r--r--ide/preferences.ml28
-rw-r--r--ide/preferences.mli2
-rw-r--r--ide/protocol/ideprotocol.mllib7
-rw-r--r--ide/protocol/interface.ml (renamed from ide/interface.mli)0
-rw-r--r--ide/protocol/richpp.ml (renamed from ide/richpp.ml)0
-rw-r--r--ide/protocol/richpp.mli (renamed from ide/richpp.mli)0
-rw-r--r--ide/protocol/serialize.ml (renamed from ide/serialize.ml)0
-rw-r--r--ide/protocol/serialize.mli (renamed from ide/serialize.mli)0
-rw-r--r--ide/protocol/xml_lexer.mli (renamed from ide/xml_lexer.mli)0
-rw-r--r--ide/protocol/xml_lexer.mll (renamed from ide/xml_lexer.mll)0
-rw-r--r--ide/protocol/xml_parser.ml (renamed from ide/xml_parser.ml)0
-rw-r--r--ide/protocol/xml_parser.mli (renamed from ide/xml_parser.mli)0
-rw-r--r--ide/protocol/xml_printer.ml (renamed from ide/xml_printer.ml)0
-rw-r--r--ide/protocol/xml_printer.mli (renamed from ide/xml_printer.mli)0
-rw-r--r--ide/protocol/xmlprotocol.ml (renamed from ide/xmlprotocol.ml)0
-rw-r--r--ide/protocol/xmlprotocol.mli (renamed from ide/xmlprotocol.mli)0
-rw-r--r--ide/wg_Command.ml8
39 files changed, 220 insertions, 120 deletions
diff --git a/ide/.merlin b/ide/.merlin.in
index 953b5dce..4dc6f455 100644
--- a/ide/.merlin
+++ b/ide/.merlin.in
@@ -2,5 +2,7 @@ PKG unix laglgtk2 lablgtk2.sourceview2
S utils
B utils
+S protocol
+B protocol
REC
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
index 47612cdf..54a592a0 100644
--- a/ide/MacOS/default_accel_map
+++ b/ide/MacOS/default_accel_map
@@ -217,7 +217,6 @@
; (gtk_accel_path "<Actions>/Tactics/Tactic casetype" "")
; (gtk_accel_path "<Actions>/Tactics/Tactic cbv in" "")
; (gtk_accel_path "<Actions>/Templates/Template Load" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fourier" "")
; (gtk_accel_path "<Actions>/Templates/Template Goal" "")
; (gtk_accel_path "<Actions>/Tactics/Tactic exists" "")
; (gtk_accel_path "<Actions>/Tactics/Tactic decompose record" "")
diff --git a/ide/MacOS/relatify_with-respect-to_.sh b/ide/MacOS/relatify_with-respect-to_.sh
deleted file mode 100755
index a24af939..00000000
--- a/ide/MacOS/relatify_with-respect-to_.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-#!/bin/sh
-
-set -e
-
-for i in "$3/"*.dylib
-do install_name_tool -change "$2"/$(basename $i) @executable_path/../Resources/lib/$(basename $i) "$1"
-done
-case "$1" in
- *.dylib)
- install_name_tool -id @executable_path/../Resources/lib/$(basename $1) $1
- for i in "$3"/*.dylib
- do install_name_tool -change "$2/"$(basename $1) @executable_path/../Resources/lib/$(basename $1) $i
- done;;
- *)
-esac
diff --git a/ide/utils/configwin.ml b/ide/configwin.ml
index 69e8b647..69e8b647 100644
--- a/ide/utils/configwin.ml
+++ b/ide/configwin.ml
diff --git a/ide/utils/configwin.mli b/ide/configwin.mli
index 7616e471..7616e471 100644
--- a/ide/utils/configwin.mli
+++ b/ide/configwin.mli
diff --git a/ide/utils/configwin_ihm.ml b/ide/configwin_ihm.ml
index d16efa60..d16efa60 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
diff --git a/ide/utils/configwin_ihm.mli b/ide/configwin_ihm.mli
index c867ad91..c867ad91 100644
--- a/ide/utils/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
diff --git a/ide/utils/configwin_messages.ml b/ide/configwin_messages.ml
index de1b4721..de1b4721 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/configwin_messages.ml
diff --git a/ide/utils/configwin_types.mli b/ide/configwin_types.ml
index 9e339d13..9e339d13 100644
--- a/ide/utils/configwin_types.mli
+++ b/ide/configwin_types.ml
diff --git a/ide/coq.ml b/ide/coq.ml
index 65456d68..e9483601 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -152,7 +152,7 @@ let print_status = function
let check_connection args =
let lines = ref [] in
let argstr = String.concat " " (List.map Filename.quote args) in
- let cmd = Filename.quote (coqtop_path ()) ^ " -batch -ideslave " ^ argstr in
+ let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
let cmd = requote cmd in
try
let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
@@ -377,7 +377,7 @@ let spawn_handle args respawner feedback_processor =
else
"on"
in
- let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in
+ let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: args) in
let env =
match !ideslave_coqtop_flags with
| None -> None
@@ -530,20 +530,31 @@ let break_coqtop coqtop workers =
module PrintOpt =
struct
- type t = string list
+ type _ t =
+ | BoolOpt : string list -> bool t
+ | StringOpt : string list -> string t
+
+ let opt_name (type a) : a t -> string list = function
+ | BoolOpt l -> l
+ | StringOpt l -> l
+
+ let opt_data (type a) (key : a t) (v : a) = match key with
+ | BoolOpt l -> Interface.BoolValue v
+ | StringOpt l -> Interface.StringValue v
(* Boolean options *)
- let implicit = ["Printing"; "Implicit"]
- let coercions = ["Printing"; "Coercions"]
- let raw_matching = ["Printing"; "Matching"]
- let notations = ["Printing"; "Notations"]
- let all_basic = ["Printing"; "All"]
- let existential = ["Printing"; "Existential"; "Instances"]
- let universes = ["Printing"; "Universes"]
- let unfocused = ["Printing"; "Unfocused"]
+ let implicit = BoolOpt ["Printing"; "Implicit"]
+ let coercions = BoolOpt ["Printing"; "Coercions"]
+ let raw_matching = BoolOpt ["Printing"; "Matching"]
+ let notations = BoolOpt ["Printing"; "Notations"]
+ let all_basic = BoolOpt ["Printing"; "All"]
+ let existential = BoolOpt ["Printing"; "Existential"; "Instances"]
+ let universes = BoolOpt ["Printing"; "Universes"]
+ let unfocused = BoolOpt ["Printing"; "Unfocused"]
+ let diff = StringOpt ["Diffs"]
- type bool_descr = { opts : t list; init : bool; label : string }
+ type 'a descr = { opts : 'a t list; init : 'a; label : string }
let bool_items = [
{ opts = [implicit]; init = false; label = "Display _implicit arguments" };
@@ -561,24 +572,32 @@ struct
{ opts = [unfocused]; init = false; label = "Display _unfocused goals" }
]
+ let diff_item = { opts = [diff]; init = "off"; label = "Display _proof diffs" }
+
(** The current status of the boolean options *)
let current_state = Hashtbl.create 11
- let set opt v = Hashtbl.replace current_state opt v
+ let set (type a) (opt : a t) (v : a) =
+ Hashtbl.replace current_state (opt_name opt) (opt_data opt v)
let reset () =
let init_descr d = List.iter (fun o -> set o d.init) d.opts in
- List.iter init_descr bool_items
+ List.iter init_descr bool_items;
+ List.iter (fun o -> set o diff_item.init) diff_item.opts
let _ = reset ()
- let printing_unfocused () = Hashtbl.find current_state unfocused
+ let printing_unfocused () =
+ let BoolOpt unfocused = unfocused in
+ match Hashtbl.find current_state unfocused with
+ | Interface.BoolValue b -> b
+ | _ -> assert false
(** Transmitting options to coqtop *)
let enforce h k =
- let mkopt o v acc = (o, Interface.BoolValue v) :: acc in
+ let mkopt o v acc = (o, v) :: acc in
let opts = Hashtbl.fold mkopt current_state [] in
eval_call (Xmlprotocol.set_options opts) h
(function
diff --git a/ide/coq.mli b/ide/coq.mli
index 40a6dea8..3af0aa69 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -134,13 +134,15 @@ val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query
module PrintOpt :
sig
- type t (** Representation of an option *)
+ type 'a t (** Representation of an option *)
- type bool_descr = { opts : t list; init : bool; label : string }
+ type 'a descr = { opts : 'a t list; init : 'a; label : string }
- val bool_items : bool_descr list
+ val bool_items : bool descr list
- val set : t -> bool -> unit
+ val diff_item : string descr
+
+ val set : 'a t -> 'a -> unit
val printing_unfocused: unit -> bool
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index f5dba208..b0bafb79 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -311,7 +311,6 @@ let tactics =
"fix __ with";
"fold";
"fold __ in";
- "fourier";
"functional induction";
];
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 1fdd7317..b6654f6d 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -23,7 +23,11 @@ let number = [ '0'-'9' ]+
let string = "\"" _+ "\""
-let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
+let alpha = ['a'-'z' 'A'-'Z']
+
+let ident = alpha (alpha | number | '_' | "'")*
+
+let undotted_sep = ((number | '[' ident ']') space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number
diff --git a/ide/coqide.ml b/ide/coqide.ml
index f5ff0899..a4d45c6d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -826,6 +826,7 @@ let refresh_notebook_pos () =
let menu = GAction.add_actions
let item = GAction.add_action
+let radio = GAction.add_radio_action
(** Toggle items in menus for printing options *)
@@ -1003,8 +1004,6 @@ let build_ui () =
item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP
~accel:"<Shift>F3"
~callback:(cb_on_current_term (fun t -> t.finder#find_backward ()));
- item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash"
- ~callback:(fun _ -> ());
item "External editor" ~label:"External editor" ~stock:`EDIT
~callback:External.editor;
item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
@@ -1043,7 +1042,27 @@ let build_ui () =
~callback:(fun _ -> show_toolbar#set (not show_toolbar#get));
item "Query Pane" ~label:"_Query Pane"
~accel:"F1"
- ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane)
+ ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane);
+ GAction.group_radio_actions
+ ~init_value:(
+ let v = diffs#get in
+ List.iter (fun o -> Opt.set o v) Opt.diff_item.Opt.opts;
+ if v = "on" then 1
+ else if v = "removed" then 2
+ else 0)
+ ~callback:begin fun n ->
+ (match n with
+ | 0 -> List.iter (fun o -> Opt.set o "off"; diffs#set "off") Opt.diff_item.Opt.opts
+ | 1 -> List.iter (fun o -> Opt.set o "on"; diffs#set "on") Opt.diff_item.Opt.opts
+ | 2 -> List.iter (fun o -> Opt.set o "removed"; diffs#set "removed") Opt.diff_item.Opt.opts
+ | _ -> assert false);
+ send_to_coq (fun sn -> sn.coqops#show_goals)
+ end
+ [
+ radio "Unset diff" 0 ~label:"_Don't show diffs";
+ radio "Set diff" 1 ~label:"Show diffs: only _added";
+ radio "Set removed diff" 2 ~label:"Show diffs: added and _removed";
+ ];
];
toggle_items view_menu Coq.PrintOpt.bool_items;
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 717c4000..c994898a 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -60,7 +60,6 @@ let init () =
\n <menuitem action='Find' />\
\n <menuitem action='Find Next' />\
\n <menuitem action='Find Previous' />\
-\n <menuitem action='Complete Word' />\
\n <separator />\
\n <menuitem action='External editor' />\
\n <separator />\
@@ -86,6 +85,10 @@ let init () =
\n <menuitem action='Display universe levels' />\
\n <menuitem action='Display all low-level contents' />\
\n <menuitem action='Display unfocused goals' />\
+\n <separator/>\
+\n <menuitem action='Unset diff' />\
+\n <menuitem action='Set diff' />\
+\n <menuitem action='Set removed diff' />\
\n </menu>\
\n <menu action='Navigation'>\
\n <menuitem action='Forward' />\
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 9f5c9924..d554bebd 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -35,8 +35,11 @@ let find_word_start (it:GText.iter) =
(Minilib.log "find_word_start: cannot backward"; it)
else if is_word_char it#char
then step_to_start it
- else (it#nocopy#forward_char;
- Minilib.log ("Word start at: "^(string_of_int it#offset));it)
+ else begin
+ ignore(it#nocopy#forward_char);
+ Minilib.log ("Word start at: "^(string_of_int it#offset));
+ it
+ end
in
step_to_start it#copy
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 96ea8c41..a7ade713 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,15 +9,7 @@ Config_lexer
Utf8_convert
Preferences
Project_file
-Serialize
-Richprinter
-Xml_lexer
-Xml_parser
-Xml_printer
-Serialize
-Richpp
Topfmt
-Xmlprotocol
Ideutils
Coq
Coq_lex
diff --git a/ide/coqidetop.mllib b/ide/ide_common.mllib
index df988d8f..050c282e 100644
--- a/ide/coqidetop.mllib
+++ b/ide/ide_common.mllib
@@ -5,4 +5,3 @@ Serialize
Richpp
Xmlprotocol
Document
-Ide_slave
diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli
deleted file mode 100644
index 9db9ecd1..00000000
--- a/ide/ide_slave.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(* This empty file avoids a race condition that occurs when compiling a .ml file
- that does not have a corresponding .mli file *)
diff --git a/ide/ide_slave.ml b/ide/idetop.ml
index 6b7efc83..8a221a93 100644
--- a/ide/ide_slave.ml
+++ b/ide/idetop.ml
@@ -18,9 +18,8 @@ open Printer
module NamedDecl = Context.Named.Declaration
module CompactedDecl = Context.Compacted.Declaration
-(** Ide_slave : an implementation of [Interface], i.e. mainly an interp
- function and a rewind function. This specialized loop is triggered
- when the -ideslave option is passed to Coqtop. *)
+(** Idetop : an implementation of [Interface], i.e. mainly an interp
+ function and a rewind function. *)
(** Signal handling: we postpone ^C during input and output phases,
@@ -54,10 +53,12 @@ let coqide_known_option table = List.mem table [
["Printing";"Records"];
["Printing";"Existential";"Instances"];
["Printing";"Universes"];
- ["Printing";"Unfocused"]]
+ ["Printing";"Unfocused"];
+ ["Diffs"]]
let is_known_option cmd = match Vernacprop.under_control cmd with
| VernacSetOption (_, o, BoolValue true)
+ | VernacSetOption (_, o, StringValue _)
| VernacUnsetOption (_, o) -> coqide_known_option o
| _ -> false
@@ -81,7 +82,7 @@ let set_doc doc = ide_doc := Some doc
let add ((s,eid),(sid,verbose)) =
let doc = get_doc () in
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
let loc_ast = Stm.parse_sentence ~doc sid pa in
let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
set_doc doc;
@@ -114,14 +115,14 @@ let edit_at id =
* be removed in the next version of the protocol.
*)
let query (route, (s,id)) =
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
let doc = get_doc () in
Stm.query ~at:id ~doc ~route pa
let annotate phrase =
let doc = get_doc () in
let {CAst.loc;v=ast} =
- let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
+ let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
in
(* XXX: Width should be a parameter of annotate... *)
@@ -152,7 +153,7 @@ let hyp_next_tac sigma env decl =
("inversion clear "^id_s), ("inversion_clear "^id_s^".")
]
-let concl_next_tac sigma concl =
+let concl_next_tac =
let expand s = (s,s^".") in
List.map expand ([
"intro";
@@ -207,9 +208,32 @@ let goals () =
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
try
- let pfts = Proof_global.give_me_the_proof () in
- Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
- with Proof_global.NoCurrentProof -> None
+ let newp = Proof_global.give_me_the_proof () in
+ 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 map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
+ try Evar.Map.find ng diff_goal_map with Not_found -> ng
+ in
+
+ let process_goal_diffs nsigma ng =
+ let open Evd in
+ let og = map_goal_for_diff ng in
+ let og_s = match oldp with
+ | Some oldp ->
+ let (_,_,_,_,osigma) = Proof.proof oldp in
+ Some { it = og; sigma = osigma }
+ | 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
+ try
+ Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
+ with Pp_diff.Diff_Failure _ -> Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+ end else
+ Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+ with Proof_global.NoCurrentProof -> None;;
let evars () =
try
@@ -231,10 +255,9 @@ let hints () =
| [] -> None
| g :: _ ->
let env = Goal.V82.env sigma g in
- let hint_goal = concl_next_tac sigma g in
let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
- Some (hint_hyps, hint_goal)
+ Some (hint_hyps, concl_next_tac)
with Proof_global.NoCurrentProof -> None
@@ -273,7 +296,10 @@ let status force =
let export_coq_object t = {
Interface.coq_object_prefix = t.Search.coq_object_prefix;
Interface.coq_object_qualid = t.Search.coq_object_qualid;
- Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
+ Interface.coq_object_object =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Pp.string_of_ppcmds (pr_lconstr_env env sigma t.Search.coq_object_object)
}
let pattern_of_string ?env s =
@@ -283,13 +309,12 @@ let pattern_of_string ?env s =
| Some e -> e
in
let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
- let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in
+ let (_, pat) = Constrintern.intern_constr_pattern env (Evd.from_env env) constr in
pat
let dirpath_of_string_list s =
let path = String.concat "." s in
- let m = Pcoq.parse_string Pcoq.Constr.global path in
- let {CAst.v=qid} = Libnames.qualid_of_reference m in
+ let qid = Pcoq.parse_string Pcoq.Constr.global path in
let id =
try Nametab.full_name_module qid
with Not_found ->
@@ -352,15 +377,12 @@ let about () = {
}
let handle_exn (e, info) =
- let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in
let dummy = Stateid.dummy in
let loc_of e = match Loc.get_loc e with
| Some loc -> Some (Loc.unloc loc)
| _ -> None in
let mk_msg () = CErrors.print ~info e in
match e with
- | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
- | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!"
| e ->
match Stateid.get info with
| Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -432,7 +454,7 @@ let eval_call c =
Xmlprotocol.abstract_eval_call handler c
(** Message dispatching.
- Since coqtop -ideslave starts 1 thread per slave, and each
+ Since [coqidetop] starts 1 thread per slave, and each
thread forwards feedback messages from the slave to the GUI on the same
xml channel, we need mutual exclusion. The mutex should be per-channel, but
here we only use 1 channel. *)
@@ -460,7 +482,7 @@ let msg_format = ref (fun () ->
(* The loop ignores the command line arguments as the current model delegates
its handing to the toplevel container. *)
-let loop _args ~state =
+let loop ~opts:_ ~state =
let open Vernac.State in
set_doc state.doc;
init_signal_handler ();
@@ -509,14 +531,16 @@ let rec parse = function
| x :: rest -> x :: parse rest
| [] -> []
-let () = Coqtop.toploop_init := (fun coq_args extra_args ->
- let args = parse extra_args in
- Flags.quiet := true;
- CoqworkmgrApi.(init High);
- args)
-
-let () = Coqtop.toploop_run := loop
-
let () = Usage.add_to_usage "coqidetop"
" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\
\n --help-XML-protocol print documentation of the Coq XML protocol\n"
+
+let islave_init ~opts extra_args =
+ let args = parse extra_args in
+ CoqworkmgrApi.(init High);
+ opts, args
+
+let () =
+ let open Coqtop in
+ let custom = { init = islave_init; run = loop; } in
+ start_coq custom
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index bdb39e94..03396a5a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,6 +37,11 @@ let flash_info =
let flash_context = status#new_context ~name:"Flash" in
(fun ?(delay=5000) s -> flash_context#flash ~delay s)
+(* Note: Setting the same attribute with two separate tags appears to use
+the first value applied and not the second. I saw this trying to set the background
+color on Windows. A clean fix, if ever needed, would be to combine the attributes
+of the tags into a single composite tag before applying. This is left as an
+exercise for the reader. *)
let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
(** FIXME: LablGTK2 does not export the C insert_with_tags function, so that
it has to reimplement its own helper function. Unluckily, it relies on
@@ -50,21 +55,51 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
let start = buf#get_iter_at_mark mark in
let stop = buf#get_iter_at_mark rmark in
let iter tag = buf#apply_tag tag ~start ~stop in
- List.iter iter tags
+ List.iter iter (List.rev tags)
+
+let nl_white_regex = Str.regexp "^\\( *\n *\\)"
+let diff_regex = Str.regexp "^diff."
let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
let open Xml_datatype in
+ let dtags = ref [] in
let tag name =
match GtkText.TagTable.lookup buf#tag_table name with
| None -> raise Not_found
| Some tag -> new GText.tag tag
in
let rmark = `MARK (buf#create_mark buf#start_iter) in
+ (* insert the string, but don't apply diff highlights to white space at the begin/end of line *)
+ let rec insert_str tags s =
+ let etags = try List.hd !dtags :: tags with hd -> tags in
+ try
+ let start = Str.search_forward nl_white_regex s 0 in
+ insert_with_tags buf mark rmark etags (String.sub s 0 start);
+ insert_with_tags buf mark rmark tags (Str.matched_group 1 s);
+ let mend = Str.match_end () in
+ insert_str tags (String.sub s mend (String.length s - mend))
+ with Not_found ->
+ insert_with_tags buf mark rmark etags s
+ in
let rec insert tags = function
- | PCData s -> insert_with_tags buf mark rmark tags s
+ | PCData s -> insert_str tags s
| Element (t, _, children) ->
- let tags = try tag t :: tags with Not_found -> tags in
- List.iter (fun xml -> insert tags xml) children
+ let (pfx, tname) = Pp.split_tag t in
+ let is_diff = try let _ = Str.search_forward diff_regex tname 0 in true with Not_found -> false in
+ let (tags, have_tag) =
+ try
+ let t = tag tname in
+ if is_diff && pfx <> Pp.end_pfx then
+ dtags := t :: !dtags;
+ if pfx = "" then
+ ((if is_diff then tags else t :: tags), true)
+ else
+ (tags, true)
+ with Not_found -> (tags, false)
+ in
+ List.iter (fun xml -> insert tags xml) children;
+ if have_tag && is_diff && pfx <> Pp.start_pfx then
+ dtags := (try List.tl !dtags with tl -> []);
in
let () = try insert tags msg with _ -> () in
buf#delete_mark rmark
@@ -289,16 +324,10 @@ let coqtop_path () =
| Some s -> s
| None ->
match cmd_coqtop#get with
- | Some s -> s
- | None ->
- try
- let old_prog = Sys.executable_name in
- let pos = String.length old_prog - 6 in
- let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos
- in
- let new_prog = Bytes.of_string old_prog in
- Bytes.blit_string "coqtop" 0 new_prog i 6;
- let new_prog = Bytes.to_string new_prog in
+ | Some s -> s
+ | None ->
+ try
+ let new_prog = System.get_toplevel_path "coqidetop" in
if Sys.file_exists new_prog then new_prog
else
let in_macos_bundle =
@@ -306,8 +335,8 @@ let coqtop_path () =
(Filename.dirname new_prog)
(Filename.concat "../Resources/bin" (Filename.basename new_prog))
in if Sys.file_exists in_macos_bundle then in_macos_bundle
- else "coqtop"
- with Not_found -> "coqtop"
+ else "coqidetop"
+ with Not_found -> "coqidetop"
in file
(* In win32, when a command-line is to be executed via cmd.exe
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index 2be5dce4..f2913b1d 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -153,13 +153,13 @@ let emacs = insert emacs "Emacs" [] [
i#forward_sentence_end, { s with move = None }));
mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i ->
i#backward_sentence_start, { s with move = None }));
- mkE _n "n" "Move to next line" ~alias:[[],_Down,"DOWN"] (Motion(fun s i ->
+ mkE _n "n" "Move to next line" (Motion(fun s i ->
let orig_off = Option.default i#line_offset s.move in
let i = i#forward_line in
let new_off = min (i#chars_in_line - 1) orig_off in
(if new_off > 0 then i#set_line_offset new_off else i),
{ s with move = Some orig_off }));
- mkE _p "p" "Move to previous line" ~alias:[[],_Up,"UP"] (Motion(fun s i ->
+ mkE _p "p" "Move to previous line" (Motion(fun s i ->
let orig_off = Option.default i#line_offset s.move in
let i = i#backward_line in
let new_off = min (i#chars_in_line - 1) orig_off in
@@ -189,7 +189,7 @@ let emacs = insert emacs "Emacs" [] [
run "Edit" "Cut";
{ s with kill = Some(txt,false); sel = false }
else s));
- mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ ->
+ mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ ->
let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
let k =
if i#ends_line then begin
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 11aaf6e8..955ee878 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -25,6 +25,7 @@ type tag = {
tag_bold : bool;
tag_italic : bool;
tag_underline : bool;
+ tag_strikethrough : bool;
}
(** Generic preferences *)
@@ -215,15 +216,17 @@ object
string_of_bool tag.tag_bold;
string_of_bool tag.tag_italic;
string_of_bool tag.tag_underline;
+ string_of_bool tag.tag_strikethrough;
]
method into = function
- | [fg; bg; bd; it; ul] ->
+ | [fg; bg; bd; it; ul; st] ->
(try Some {
tag_fg_color = _to fg;
tag_bg_color = _to bg;
tag_bold = bool_of_string bd;
tag_italic = bool_of_string it;
tag_underline = bool_of_string ul;
+ tag_strikethrough = bool_of_string st;
}
with _ -> None)
| _ -> None
@@ -429,12 +432,13 @@ let tags = ref Util.String.Map.empty
let list_tags () = !tags
-let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = {
+let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) ?(strikethrough = false) () = {
tag_fg_color = fg;
tag_bg_color = bg;
tag_bold = bold;
tag_italic = italic;
tag_underline = underline;
+ tag_strikethrough = strikethrough;
}
let create_tag name default =
@@ -470,6 +474,12 @@ let create_tag name default =
tag#set_property (`UNDERLINE_SET true);
tag#set_property (`UNDERLINE `SINGLE)
end;
+ begin match pref#get.tag_strikethrough with
+ | false -> tag#set_property (`STRIKETHROUGH_SET false)
+ | true ->
+ tag#set_property (`STRIKETHROUGH_SET true);
+ tag#set_property (`STRIKETHROUGH true)
+ end;
in
let iter table =
let tag = GText.tag ~name () in
@@ -480,6 +490,8 @@ let create_tag name default =
List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
tags := Util.String.Map.add name pref !tags
+(* note these appear to only set the defaults; they don't override
+the user selection from the Edit/Preferences/Tags dialog *)
let () =
let iter (name, tag) = create_tag name tag in
List.iter iter [
@@ -498,6 +510,10 @@ let () =
("tactic.keyword", make_tag ());
("tactic.primitive", make_tag ());
("tactic.string", make_tag ());
+ ("diff.added", make_tag ~bg:"#b6f1c0" ~underline:true ());
+ ("diff.removed", make_tag ~bg:"#f6b9c1" ~strikethrough:true ());
+ ("diff.added.bg", make_tag ~bg:"#e9feee" ());
+ ("diff.removed.bg", make_tag ~bg:"#fce9eb" ());
]
let processed_color =
@@ -549,6 +565,9 @@ let nanoPG =
let user_queries =
new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$')
+let diffs =
+ new preference ~name:["diffs"] ~init:"off" ~repr:Repr.(string)
+
class tag_button (box : Gtk.box Gtk.obj) =
object (self)
@@ -561,6 +580,7 @@ object (self)
val bold = GButton.toggle_button ()
val italic = GButton.toggle_button ()
val underline = GButton.toggle_button ()
+ val strikethrough = GButton.toggle_button ()
method set_tag tag =
let track c but set = match c with
@@ -574,6 +594,7 @@ object (self)
bold#set_active tag.tag_bold;
italic#set_active tag.tag_italic;
underline#set_active tag.tag_underline;
+ strikethrough#set_active tag.tag_strikethrough;
method tag =
let get but set =
@@ -586,6 +607,7 @@ object (self)
tag_bold = bold#active;
tag_italic = italic#active;
tag_underline = underline#active;
+ tag_strikethrough = strikethrough#active;
}
initializer
@@ -599,6 +621,7 @@ object (self)
set_stock bold `BOLD;
set_stock italic `ITALIC;
set_stock underline `UNDERLINE;
+ set_stock strikethrough `STRIKETHROUGH;
box#pack fg_color#coerce;
box#pack fg_unset#coerce;
box#pack bg_color#coerce;
@@ -606,6 +629,7 @@ object (self)
box#pack bold#coerce;
box#pack italic#coerce;
box#pack underline#coerce;
+ box#pack strikethrough#coerce;
let cb but obj = obj#set_sensitive (not but#active) in
let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in
let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index ccf028ae..dd2976ef 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -21,6 +21,7 @@ type tag = {
tag_bold : bool;
tag_italic : bool;
tag_underline : bool;
+ tag_strikethrough : bool;
}
class type ['a] repr =
@@ -101,6 +102,7 @@ val tab_length : int preference
val highlight_current_line : bool preference
val nanoPG : bool preference
val user_queries : (string * string) list preference
+val diffs : string preference
val save_pref : unit -> unit
val load_pref : unit -> unit
diff --git a/ide/protocol/ideprotocol.mllib b/ide/protocol/ideprotocol.mllib
new file mode 100644
index 00000000..8317a086
--- /dev/null
+++ b/ide/protocol/ideprotocol.mllib
@@ -0,0 +1,7 @@
+Xml_lexer
+Xml_parser
+Xml_printer
+Serialize
+Richpp
+Interface
+Xmlprotocol
diff --git a/ide/interface.mli b/ide/protocol/interface.ml
index debbc830..debbc830 100644
--- a/ide/interface.mli
+++ b/ide/protocol/interface.ml
diff --git a/ide/richpp.ml b/ide/protocol/richpp.ml
index 19e9799c..19e9799c 100644
--- a/ide/richpp.ml
+++ b/ide/protocol/richpp.ml
diff --git a/ide/richpp.mli b/ide/protocol/richpp.mli
index 31fc7b56..31fc7b56 100644
--- a/ide/richpp.mli
+++ b/ide/protocol/richpp.mli
diff --git a/ide/serialize.ml b/ide/protocol/serialize.ml
index 86074d44..86074d44 100644
--- a/ide/serialize.ml
+++ b/ide/protocol/serialize.ml
diff --git a/ide/serialize.mli b/ide/protocol/serialize.mli
index af082f25..af082f25 100644
--- a/ide/serialize.mli
+++ b/ide/protocol/serialize.mli
diff --git a/ide/xml_lexer.mli b/ide/protocol/xml_lexer.mli
index e61cb055..e61cb055 100644
--- a/ide/xml_lexer.mli
+++ b/ide/protocol/xml_lexer.mli
diff --git a/ide/xml_lexer.mll b/ide/protocol/xml_lexer.mll
index 4a52147e..4a52147e 100644
--- a/ide/xml_lexer.mll
+++ b/ide/protocol/xml_lexer.mll
diff --git a/ide/xml_parser.ml b/ide/protocol/xml_parser.ml
index 8db3f9e8..8db3f9e8 100644
--- a/ide/xml_parser.ml
+++ b/ide/protocol/xml_parser.ml
diff --git a/ide/xml_parser.mli b/ide/protocol/xml_parser.mli
index ac2eab35..ac2eab35 100644
--- a/ide/xml_parser.mli
+++ b/ide/protocol/xml_parser.mli
diff --git a/ide/xml_printer.ml b/ide/protocol/xml_printer.ml
index 488ef7bf..488ef7bf 100644
--- a/ide/xml_printer.ml
+++ b/ide/protocol/xml_printer.ml
diff --git a/ide/xml_printer.mli b/ide/protocol/xml_printer.mli
index 178f7c80..178f7c80 100644
--- a/ide/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
diff --git a/ide/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e1821921..e1821921 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
diff --git a/ide/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli
index ba6000f0..ba6000f0 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/protocol/xmlprotocol.mli
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 8eddfb31..06281d62 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -98,7 +98,7 @@ object(self)
~packing:(vbox#pack ~fill:true ~expand:true) () in
let result = Wg_MessageView.message_view () in
router#register_route route_id result;
- r_bin#add (result :> GObj.widget);
+ r_bin#add_with_viewport (result :> GObj.widget);
views <- (frame#coerce, result, combo#entry) :: views;
let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
let _ = background_color#connect#changed ~callback:cb in
@@ -152,9 +152,9 @@ object(self)
method show =
frame#show;
let cur_page = notebook#get_nth_page notebook#current_page in
- let _, _, e =
- List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views in
- e#misc#grab_focus ()
+ match List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views with
+ | (_, _, e) -> e#misc#grab_focus ()
+ | exception Not_found -> ()
method hide =
frame#hide
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 12:01:07 +0000