aboutsummaryrefslogtreecommitdiff
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)4
-rw-r--r--ide/configwin.mli (renamed from ide/utils/configwin.mli)1
-rw-r--r--ide/configwin_ihm.ml (renamed from ide/utils/configwin_ihm.ml)42
-rw-r--r--ide/configwin_ihm.mli (renamed from ide/utils/configwin_ihm.mli)10
-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.ml56
-rw-r--r--ide/coq.mli10
-rw-r--r--ide/coqOps.ml6
-rw-r--r--ide/coq_commands.ml1
-rw-r--r--ide/coq_lex.mll6
-rw-r--r--ide/coqide.ml149
-rw-r--r--ide/coqide.mli4
-rw-r--r--ide/coqide_QUARTZ.ml.in37
-rw-r--r--ide/coqide_WIN32.ml.in50
-rw-r--r--ide/coqide_X11.ml.in (renamed from ide/ide_slave.mli)3
-rw-r--r--ide/coqide_main.ml (renamed from ide/coqide_main.ml4)88
-rw-r--r--ide/coqide_os_specific.mli11
-rw-r--r--ide/coqide_ui.ml5
-rw-r--r--ide/dune56
-rw-r--r--ide/fake_ide.ml334
-rw-r--r--ide/fileOps.ml14
-rw-r--r--ide/fileOps.mli4
-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/idetop.ml (renamed from ide/ide_slave.ml)77
-rw-r--r--ide/ideutils.ml66
-rw-r--r--ide/nanoPG.ml6
-rw-r--r--ide/preferences.ml59
-rw-r--r--ide/preferences.mli4
-rw-r--r--ide/protocol/dune7
-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)5
-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
-rw-r--r--ide/wg_ProofView.ml4
51 files changed, 883 insertions, 285 deletions
diff --git a/ide/.merlin b/ide/.merlin.in
index 953b5dce4c..4dc6f45550 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 47612cdf72..54a592a04d 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 a24af93958..0000000000
--- 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 69e8b647ae..24be721631 100644
--- a/ide/utils/configwin.ml
+++ b/ide/configwin.ml
@@ -46,6 +46,6 @@ let modifiers = Configwin_ihm.modifiers
let edit
?(apply=(fun () -> ()))
- title ?width ?height
+ title ?parent ?width ?height
conf_struct_list =
- Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list
+ Configwin_ihm.edit ~with_apply: true ~apply title ?parent ?width ?height conf_struct_list
diff --git a/ide/utils/configwin.mli b/ide/configwin.mli
index 7616e471db..0ee77d69b5 100644
--- a/ide/utils/configwin.mli
+++ b/ide/configwin.mli
@@ -158,6 +158,7 @@ val custom : ?label: string -> GPack.box -> (unit -> unit) -> bool -> parameter_
val edit :
?apply: (unit -> unit) ->
string ->
+ ?parent:GWindow.window ->
?width:int ->
?height:int ->
configuration_structure list ->
diff --git a/ide/utils/configwin_ihm.ml b/ide/configwin_ihm.ml
index d16efa603d..91695e944e 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -662,12 +662,13 @@ class configuration_box (tt : GData.tooltips) conf_struct =
to configure the various parameters. *)
let edit ?(with_apply=true)
?(apply=(fun () -> ()))
- title ?width ?height
+ title ?parent ?width ?height
conf_struct =
let dialog = GWindow.dialog
~position:`CENTER
~modal: true ~title: title
- ?height ?width
+ ~type_hint:`DIALOG
+ ?parent ?height ?width
()
in
let tooltips = GData.tooltips () in
@@ -807,3 +808,40 @@ let custom ?label box f expand =
custom_expand = expand ;
custom_framed = label ;
}
+
+(* Copying lablgtk question_box + forbidding hiding *)
+
+let question_box ~title ~buttons ?(default=1) ?icon ?parent message =
+ let button_nb = ref 0 in
+ let window = GWindow.dialog ~position:`CENTER ~modal:true ?parent ~type_hint:`DIALOG ~title () in
+ let hbox = GPack.hbox ~border_width:10 ~packing:window#vbox#add () in
+ let bbox = window#action_area in
+ begin match icon with
+ None -> ()
+ | Some i -> hbox#pack i#coerce ~padding:4
+ end;
+ ignore (GMisc.label ~text: message ~packing: hbox#add ());
+ (* the function called to create each button by iterating *)
+ let rec iter_buttons n = function
+ [] ->
+ ()
+ | button_label :: q ->
+ let b = GButton.button ~label: button_label
+ ~packing:(bbox#pack ~expand:true ~padding:4) ()
+ in
+ ignore (b#connect#clicked ~callback:
+ (fun () -> button_nb := n; window#destroy ()));
+ (* If it's the first button then give it the focus *)
+ if n = default then b#grab_default () else ();
+
+ iter_buttons (n+1) q
+ in
+ iter_buttons 1 buttons;
+ ignore (window#connect#destroy ~callback: GMain.Main.quit);
+ window#set_position `CENTER;
+ window#show ();
+ GMain.Main.main ();
+ !button_nb
+
+let message_box ~title ?icon ?parent ?(ok="Ok") message =
+ ignore (question_box ?icon ?parent ~title message ~buttons:[ ok ])
diff --git a/ide/utils/configwin_ihm.mli b/ide/configwin_ihm.mli
index c867ad9127..772a0958ff 100644
--- a/ide/utils/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
@@ -60,7 +60,17 @@ val edit :
?with_apply:bool ->
?apply:(unit -> unit) ->
string ->
+ ?parent:GWindow.window ->
?width:int ->
?height:int ->
configuration_structure list ->
return_button
+
+val question_box : title:string ->
+ buttons:string list ->
+ ?default:int -> ?icon:#GObj.widget ->
+ ?parent:GWindow.window -> string -> int
+
+val message_box :
+ title:string -> ?icon:#GObj.widget ->
+ ?parent:GWindow.window -> ?ok:string -> string -> unit
diff --git a/ide/utils/configwin_messages.ml b/ide/configwin_messages.ml
index de1b4721d0..de1b4721d0 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 9e339d135d..9e339d135d 100644
--- a/ide/utils/configwin_types.mli
+++ b/ide/configwin_types.ml
diff --git a/ide/coq.ml b/ide/coq.ml
index 65456d685a..88ffb4f0b7 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -42,14 +42,11 @@ let version () =
"The Coq Proof Assistant, version %s (%s)\
\nArchitecture %s running %s operating system\
\nGtk version is %s\
- \nThis is %s (%s is the best one for this architecture and OS)\
- \n"
+ \nThis is %s \n"
ver date
Coq_config.arch Sys.os_type
(let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
(Filename.basename Sys.executable_name)
- Coq_config.best
-
(** * Initial checks by launching test coqtop processes *)
@@ -152,7 +149,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 +374,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 +527,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 +569,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 40a6dea8d3..3af0aa697e 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/coqOps.ml b/ide/coqOps.ml
index 78fbce5c81..6c3438a4b0 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -362,7 +362,12 @@ object(self)
let query = Coq.query (route_id,(phrase,sid)) in
Coq.bind (Coq.seq action query) next
+ method private still_valid { edit_id = id } =
+ try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true
+ with Not_found -> false
+
method private mark_as_needed sentence =
+ if self#still_valid sentence then begin
Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence);
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
@@ -383,6 +388,7 @@ object(self)
in
List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags;
List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags
+ end
method private attach_tooltip ?loc sentence text =
let start_sentence, stop_sentence, phrase = self#get_sentence sentence in
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index f5dba2085a..b0bafb7930 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 1fdd7317b5..b6654f6d7a 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 aa816f2b8b..40b8d2f484 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -89,21 +89,30 @@ let make_coqtop_args fname =
| Ignore_args -> !sup_args
| Append_args -> !sup_args
| Subst_args -> [] in
- if read_project#get = Ignore_args then "", base_args
- else
- match !custom_project_file, fname with
- | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args
- | None, None -> "", base_args
- | None, Some the_file ->
- match
- CoqProject_file.find_project_file
- ~from:(Filename.dirname the_file)
- ~projfile_name:project_file_name#get
- with
- | None -> "", base_args
- | Some proj ->
- proj, coqtop_args_from_project (read_project_file proj) @ base_args
-;;
+ let proj, args =
+ if read_project#get = Ignore_args then "", base_args
+ else
+ match !custom_project_file, fname with
+ | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args
+ | None, None -> "", base_args
+ | None, Some the_file ->
+ match
+ CoqProject_file.find_project_file
+ ~from:(Filename.dirname the_file)
+ ~projfile_name:project_file_name#get
+ with
+ | None -> "", base_args
+ | Some proj ->
+ let warning_fn x = Feedback.msg_warning Pp.(str x) in
+ proj, coqtop_args_from_project (read_project_file ~warning_fn proj) @ base_args
+ in
+ let args = match fname with
+ | None -> args
+ | Some fname ->
+ if List.exists (String.equal "-top") args then args
+ else "-topfile"::fname::args
+ in
+ proj, args
(** Setting drag & drop on widgets *)
@@ -181,8 +190,8 @@ let load_file ?(maycreate=false) f =
let confirm_save ok =
if ok then flash_info "Saved" else warning "Save Failed"
-let select_and_save ~saveas ?filename sn =
- let do_save = if saveas then sn.fileops#saveas else sn.fileops#save in
+let select_and_save ?parent ~saveas ?filename sn =
+ let do_save = if saveas then sn.fileops#saveas ?parent else sn.fileops#save in
let title = if saveas then "Save file as" else "Save file" in
match select_file_for_save ~title ?filename () with
|None -> false
@@ -192,9 +201,9 @@ let select_and_save ~saveas ?filename sn =
if ok then sn.tab_label#set_text (Filename.basename f);
ok
-let check_save ~saveas sn =
+let check_save ?parent ~saveas sn =
try match sn.fileops#filename with
- |None -> select_and_save ~saveas sn
+ |None -> select_and_save ?parent ~saveas sn
|Some f ->
let ok = sn.fileops#save f in
confirm_save ok;
@@ -203,16 +212,17 @@ let check_save ~saveas sn =
exception DontQuit
-let check_quit saveall =
+let check_quit ?parent saveall =
(try save_pref () with _ -> flash_info "Cannot save preferences");
let is_modified sn = sn.buffer#modified in
if List.exists is_modified notebook#pages then begin
- let answ = GToolbox.question_box ~title:"Quit"
+ let answ = Configwin_ihm.question_box ~title:"Quit"
~buttons:["Save Named Buffers and Quit";
"Quit without Saving";
"Don't Quit"]
~default:0
~icon:(warn_image ())#coerce
+ ?parent
"There are unsaved buffers"
in
match answ with
@@ -269,15 +279,15 @@ let load _ =
| None -> ()
| Some f -> FileAux.load_file f
-let save _ = on_current_term (FileAux.check_save ~saveas:false)
+let save ?parent _ = on_current_term (FileAux.check_save ?parent ~saveas:false)
-let saveas sn =
+let saveas ?parent sn =
try
let filename = sn.fileops#filename in
- ignore (FileAux.select_and_save ~saveas:true ?filename sn)
+ ignore (FileAux.select_and_save ?parent ~saveas:true ?filename sn)
with _ -> warning "Save Failed"
-let saveas = cb_on_current_term saveas
+let saveas ?parent = cb_on_current_term (saveas ?parent)
let saveall _ =
List.iter
@@ -288,33 +298,34 @@ let saveall _ =
let () = Coq.save_all := saveall
-let revert_all _ =
+let revert_all ?parent _ =
List.iter
- (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert)
+ (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert ?parent ())
notebook#pages
-let quit _ =
- try FileAux.check_quit saveall; exit 0
+let quit ?parent _ =
+ try FileAux.check_quit ?parent saveall; exit 0
with FileAux.DontQuit -> ()
-let close_buffer sn =
+let close_buffer ?parent sn =
let do_remove () = notebook#remove_page notebook#current_page in
if not sn.buffer#modified then do_remove ()
else
- let answ = GToolbox.question_box ~title:"Close"
+ let answ = Configwin_ihm.question_box ~title:"Close"
~buttons:["Save Buffer and Close";
"Close without Saving";
"Don't Close"]
~default:0
~icon:(warn_image ())#coerce
+ ?parent
"This buffer has unsaved modifications"
in
match answ with
- | 1 when FileAux.check_save ~saveas:true sn -> do_remove ()
+ | 1 when FileAux.check_save ?parent ~saveas:true sn -> do_remove ()
| 2 -> do_remove ()
| _ -> ()
-let close_buffer = cb_on_current_term close_buffer
+let close_buffer ?parent = cb_on_current_term (close_buffer ?parent)
let export kind sn =
match sn.fileops#filename with
@@ -425,16 +436,16 @@ let coq_makefile sn =
let coq_makefile = cb_on_current_term coq_makefile
-let editor sn =
+let editor ?parent sn =
match sn.fileops#filename with
|None -> warning "Call to external editor available only on named files"
|Some f ->
File.save ();
let f = Filename.quote f in
let cmd = Util.subst_command_placeholder cmd_editor#get f in
- run_command ignore (fun _ -> sn.fileops#revert) cmd
+ run_command ignore (fun _ -> sn.fileops#revert ?parent ()) cmd
-let editor = cb_on_current_term editor
+let editor ?parent = cb_on_current_term (editor ?parent)
let compile sn =
File.save ();
@@ -769,7 +780,7 @@ let coqtop_arguments sn =
let box = dialog#action_area in
let ok = GButton.button ~stock:`OK ~packing:box#add () in
let ok_cb () =
- let nargs = CString.split ' ' entry#text in
+ let nargs = String.split_on_char ' ' entry#text in
if nargs <> args then
let failed = Coq.filter_coq_opts nargs in
match failed with
@@ -826,6 +837,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 *)
@@ -935,7 +947,7 @@ let build_ui () =
try w#set_icon (Some (GdkPixbuf.from_file (MiscMenu.coq_icon ())))
with _ -> ()
in
- let _ = w#event#connect#delete ~callback:(fun _ -> File.quit (); true) in
+ let _ = w#event#connect#delete ~callback:(fun _ -> File.quit ~parent:w (); true) in
let _ = set_drag w#drag in
let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
@@ -961,18 +973,18 @@ let build_ui () =
item "File" ~label:"_File";
item "New" ~callback:File.newfile ~stock:`NEW;
item "Open" ~callback:File.load ~stock:`OPEN;
- item "Save" ~callback:File.save ~stock:`SAVE ~tooltip:"Save current buffer";
- item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:File.saveas;
+ item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer";
+ item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w);
item "Save all" ~label:"Sa_ve all" ~callback:File.saveall;
item "Revert all buffers" ~label:"_Revert all buffers"
- ~callback:File.revert_all ~stock:`REVERT_TO_SAVED;
+ ~callback:(File.revert_all ~parent:w) ~stock:`REVERT_TO_SAVED;
item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE
- ~callback:File.close_buffer ~tooltip:"Close current buffer";
+ ~callback:(File.close_buffer ~parent:w) ~tooltip:"Close current buffer";
item "Print..." ~label:"_Print..."
~callback:File.print ~stock:`PRINT ~accel:"<Ctrl>p";
item "Rehighlight" ~label:"Reh_ighlight" ~accel:"<Ctrl>l"
~callback:File.highlight ~stock:`REFRESH;
- item "Quit" ~stock:`QUIT ~callback:File.quit;
+ item "Quit" ~stock:`QUIT ~callback:(File.quit ~parent:w);
];
menu export_menu [
@@ -1003,14 +1015,12 @@ 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;
+ ~callback:(External.editor ~parent:w);
item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
~callback:(fun _ ->
begin
- try Preferences.configure ~apply:refresh_notebook_pos ()
+ try Preferences.configure ~apply:refresh_notebook_pos w
with _ -> flash_info "Cannot save preferences"
end;
reset_revert_timer ());
@@ -1043,7 +1053,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;
@@ -1106,15 +1136,15 @@ let build_ui () =
];
alpha_items templates_menu "Template" Coq_commands.commands;
- let qitem s sc ?(dots = true) =
- let query = if dots then s ^ "..." else s in
+ let qitem s sc =
+ let query = s ^ "..." in
item s ~label:("_"^s)
~accel:(modifier_for_queries#get^sc)
~callback:(Query.query query)
in
menu queries_menu [
item "Queries" ~label:"_Queries";
- qitem "Search" "K" ~dots:false;
+ qitem "Search" "K";
qitem "Check" "C";
qitem "Print" "P";
qitem "About" "A";
@@ -1279,8 +1309,8 @@ let build_ui () =
(Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
(* Showtime ! *)
- w#show ()
-
+ w#show ();
+ w
(** {2 Coqide main function } *)
@@ -1295,7 +1325,7 @@ let make_scratch_buffer () =
()
let main files =
- build_ui ();
+ let w = build_ui () in
reset_revert_timer ();
reset_autosave_timer ();
(match files with
@@ -1304,8 +1334,8 @@ let main files =
notebook#goto_page 0;
MiscMenu.initial_about ();
on_current_term (fun t -> t.script#misc#grab_focus ());
- Minilib.log "End of Coqide.main"
-
+ Minilib.log "End of Coqide.main";
+ w
(** {2 Argument parsing } *)
@@ -1325,7 +1355,8 @@ let read_coqide_args argv =
if project_files <> None then
(output_string stderr "Error: multiple -f options"; exit 1);
let d = CUnix.canonical_path_name (Filename.dirname file) in
- let p = CoqProject_file.read_project_file file in
+ let warning_fn x = Format.eprintf "%s@\n%!" x in
+ let p = CoqProject_file.read_project_file ~warning_fn file in
filter_coqtop coqtop (Some (d,p)) out args
|"-f" :: [] ->
output_string stderr "Error: missing project file name"; exit 1
@@ -1361,9 +1392,9 @@ let signals_to_crash =
[Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
Sys.sigill; Sys.sigpipe; Sys.sigquit; Sys.sigusr1; Sys.sigusr2]
-let set_signal_handlers () =
+let set_signal_handlers ?parent () =
try
- Sys.set_signal Sys.sigint (Sys.Signal_handle File.quit);
+ Sys.set_signal Sys.sigint (Sys.Signal_handle (File.quit ?parent));
List.iter
(fun i -> Sys.set_signal i (Sys.Signal_handle FileAux.crash_save))
signals_to_crash
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 03e8545377..1d438ec381 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -22,7 +22,7 @@ val logfile : string option ref
val read_coqide_args : string list -> string list
(** Prepare the widgets, load the given files in tabs *)
-val main : string list -> unit
+val main : string list -> GWindow.window
(** Function to save anything and kill all coqtops
@return [false] if you're allowed to quit. *)
@@ -37,7 +37,7 @@ val do_load : string -> unit
(** Set coqide to perform a clean quit at Ctrl-C, while launching
[crash_save] and exiting for others received signals *)
-val set_signal_handlers : unit -> unit
+val set_signal_handlers : ?parent:GWindow.window -> unit -> unit
(** Emergency saving of opened files as "foo.v.crashcoqide",
and exit (if the integer isn't 127). *)
diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in
new file mode 100644
index 0000000000..a08bac5772
--- /dev/null
+++ b/ide/coqide_QUARTZ.ml.in
@@ -0,0 +1,37 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+let osx = GosxApplication.osxapplication ()
+
+let () =
+ let _ = osx#connect#ns_application_open_file
+ ~callback:(fun x -> Coqide.do_load x; true)
+ in
+ let _ = osx#connect#ns_application_block_termination
+ ~callback:Coqide.forbid_quit
+ in
+ let _ = osx#connect#ns_application_will_terminate
+ ~callback:Coqide.close_and_quit
+ in ()
+
+let init () =
+ let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication
+ (GtkMenu.MenuShell.cast
+ (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget)
+ in
+ let () = GtkosxApplication.Application.insert_app_menu_item
+ osx#as_osxapplication
+ (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1
+ in
+ let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication
+ (Some (GtkMenu.MenuItem.cast
+ (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget))
+ in
+ osx#ready ()
diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in
new file mode 100644
index 0000000000..8c4649fc39
--- /dev/null
+++ b/ide/coqide_WIN32.ml.in
@@ -0,0 +1,50 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(* On win32, we add the directory of coqide to the PATH at launch-time
+ (this used to be done in a .bat script). *)
+
+let set_win32_path () =
+ Unix.putenv "PATH"
+ (Filename.dirname Sys.executable_name ^ ";" ^
+ (try Sys.getenv "PATH" with _ -> ""))
+
+(* On win32, since coqide is now console-free, we re-route stdout/stderr
+ to avoid Sys_error if someone writes to them. We write to a pipe which
+ is never read (by default) or to a temp log file (when in debug mode).
+*)
+
+let reroute_stdout_stderr () =
+ (* We anticipate a bit the argument parsing and look for -debug *)
+ let debug = List.mem "-debug" (Array.to_list Sys.argv) in
+ Minilib.debug := debug;
+ let out_descr =
+ if debug then
+ let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
+ Coqide.logfile := Some name;
+ Unix.descr_of_out_channel chan
+ else
+ snd (Unix.pipe ())
+ in
+ Unix.set_close_on_exec out_descr;
+ Unix.dup2 out_descr Unix.stdout;
+ Unix.dup2 out_descr Unix.stderr
+
+(* We also provide specific kill and interrupt functions. *)
+
+external win32_kill : int -> unit = "win32_kill"
+external win32_interrupt : int -> unit = "win32_interrupt"
+let () =
+ Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket;
+ set_win32_path ();
+ Coq.interrupter := win32_interrupt;
+ reroute_stdout_stderr ()
+
+let init () = ()
diff --git a/ide/ide_slave.mli b/ide/coqide_X11.ml.in
index 9db9ecd12e..6a5784eac3 100644
--- a/ide/ide_slave.mli
+++ b/ide/coqide_X11.ml.in
@@ -8,5 +8,4 @@
(* * (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 *)
+let init () = ()
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml
index 3a92e1bc91..21f513b8f4 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-let _ = Coqide.set_signal_handlers ()
let _ = GtkMain.Main.init ()
(* We handle Gtk warning messages ourselves :
@@ -49,88 +48,6 @@ let catch_gtk_messages () =
let () = catch_gtk_messages ()
-
-
-(** System-dependent settings *)
-
-let os_specific_init () = ()
-
-(** Win32 *)
-
-IFDEF WIN32 THEN
-
-(* On win32, we add the directory of coqide to the PATH at launch-time
- (this used to be done in a .bat script). *)
-
-let set_win32_path () =
- Unix.putenv "PATH"
- (Filename.dirname Sys.executable_name ^ ";" ^
- (try Sys.getenv "PATH" with _ -> ""))
-
-(* On win32, since coqide is now console-free, we re-route stdout/stderr
- to avoid Sys_error if someone writes to them. We write to a pipe which
- is never read (by default) or to a temp log file (when in debug mode).
-*)
-
-let reroute_stdout_stderr () =
- (* We anticipate a bit the argument parsing and look for -debug *)
- let debug = List.mem "-debug" (Array.to_list Sys.argv) in
- Minilib.debug := debug;
- let out_descr =
- if debug then
- let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
- Coqide.logfile := Some name;
- Unix.descr_of_out_channel chan
- else
- snd (Unix.pipe ())
- in
- Unix.set_close_on_exec out_descr;
- Unix.dup2 out_descr Unix.stdout;
- Unix.dup2 out_descr Unix.stderr
-
-(* We also provide specific kill and interrupt functions. *)
-
-external win32_kill : int -> unit = "win32_kill"
-external win32_interrupt : int -> unit = "win32_interrupt"
-let () =
- Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket;
- set_win32_path ();
- Coq.interrupter := win32_interrupt;
- reroute_stdout_stderr ()
-END
-
-(** MacOSX *)
-
-IFDEF QUARTZ THEN
-let osx = GosxApplication.osxapplication ()
-
-let () =
- let _ = osx#connect#ns_application_open_file
- ~callback:(fun x -> Coqide.do_load x; true)
- in
- let _ = osx#connect#ns_application_block_termination
- ~callback:Coqide.forbid_quit
- in
- let _ = osx#connect#ns_application_will_terminate
- ~callback:Coqide.close_and_quit
- in ()
-
-let os_specific_init () =
- let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication
- (GtkMenu.MenuShell.cast
- (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget)
- in
- let () = GtkosxApplication.Application.insert_app_menu_item
- osx#as_osxapplication
- (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1
- in
- let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication
- (Some (GtkMenu.MenuItem.cast
- (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget))
- in
- osx#ready ()
-END
-
let load_prefs () =
try Preferences.load_pref ()
with e -> Ideutils.flash_info
@@ -144,8 +61,9 @@ let () =
let args = List.filter (fun x -> not (List.mem x files)) argl in
Coq.check_connection args;
Coqide.sup_args := args;
- Coqide.main files;
- os_specific_init ();
+ let w = Coqide.main files in
+ Coqide.set_signal_handlers ~parent:w ();
+ Coqide_os_specific.init ();
try
GMain.main ();
failwith "Gtk loop ended"
diff --git a/ide/coqide_os_specific.mli b/ide/coqide_os_specific.mli
new file mode 100644
index 0000000000..ebd09099f0
--- /dev/null
+++ b/ide/coqide_os_specific.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+val init : unit -> unit
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 717c4000f5..c994898a4f 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/dune b/ide/dune
new file mode 100644
index 0000000000..5e3886624c
--- /dev/null
+++ b/ide/dune
@@ -0,0 +1,56 @@
+; IDE Server
+(ocamllex utf8_convert config_lexer coq_lex)
+
+(library
+ (name core)
+ (public_name coqide-server.core)
+ (wrapped false)
+ (modules document)
+ (libraries coq.lib))
+
+(executable
+ (name fake_ide)
+ (public_name fake_ide)
+ (package coqide-server)
+ (modules fake_ide)
+ (libraries coqide-server.protocol coqide-server.core))
+
+(executable
+ (name idetop)
+ (public_name coqidetop.opt)
+ (package coqide-server)
+ (modules idetop)
+ (libraries coq.toplevel coqide-server.protocol)
+ (link_flags -linkall))
+
+; IDE Client
+(library
+ (name gui)
+ (public_name coqide.gui)
+ (wrapped false)
+ (modules (:standard \ document fake_ide idetop coqide_main))
+ (optional)
+ (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2))
+
+(rule
+ (targets coqide_os_specific.ml)
+ (deps (:in-file coqide_X11.ml.in)) ; TODO support others
+ (action (copy# %{in-file} %{targets})))
+
+(executable
+ (name coqide_main)
+ (public_name coqide)
+ (package coqide)
+ (modules coqide_main)
+ (libraries coqide.gui))
+
+; FIXME: we should install those in share/coqide. We better do this
+; once the make-based system has been phased out.
+(install
+ (section share_root)
+ (package coqide)
+ (files
+ (coq.png as coq/coq.png)
+ (coq_style.xml as coq/coq_style.xml)
+ (coq.lang as coq/coq.lang)
+ (coq-ssreflect.lang as coq/coq-ssreflect.lang)))
diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml
new file mode 100644
index 0000000000..521aff6bf6
--- /dev/null
+++ b/ide/fake_ide.ml
@@ -0,0 +1,334 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *)
+
+let error s =
+ prerr_endline ("fake_id: error: "^s);
+ exit 1
+
+let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
+
+type coqtop = {
+ xml_printer : Xml_printer.t;
+ xml_parser : Xml_parser.t;
+}
+
+let print_error msg =
+ Format.eprintf "fake_id: 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);
+ let xml_query = Xmlprotocol.of_call call in
+ Xml_printer.print coqtop.xml_printer xml_query;
+ let rec loop () =
+ let xml = Xml_parser.parse coqtop.xml_parser in
+ if Xmlprotocol.is_feedback xml then
+ loop ()
+ else Xmlprotocol.to_answer call xml
+ in
+ let res = loop () in
+ if print then prerr_endline (Xmlprotocol.pr_full_value call res);
+ match res with
+ | Interface.Fail (_,_,s) when fail -> print_error s; exit 1
+ | Interface.Fail (_,_,s) as x -> print_error s; x
+ | x -> x
+
+let eval_call c q = ignore(base_eval_call c q)
+
+module Parser = struct (* {{{ *)
+
+ exception Err of string
+ exception More
+
+ type token =
+ | Tok of string * string
+ | Top of token list
+
+ type grammar =
+ | Alt of grammar list
+ | Seq of grammar list
+ | Opt of grammar
+ | Item of (string * (string -> token * int))
+
+ let eat_rex x = x, fun s ->
+ if Str.string_match (Str.regexp x) s 0 then begin
+ let m = Str.match_end () in
+ let w = String.sub s 0 m in
+ Tok(x,w), m
+ end else raise (Err ("Regexp "^x^" not found in: "^s))
+
+ let eat_balanced c =
+ let c' = match c with
+ | '{' -> '}' | '(' -> ')' | '[' -> ']' | _ -> assert false in
+ let sc, sc' = String.make 1 c, String.make 1 c' in
+ let name = sc ^ "..." ^ sc' in
+ let unescape s =
+ Str.global_replace (Str.regexp ("\\\\"^sc)) sc
+ (Str.global_replace (Str.regexp ("\\\\"^sc')) sc' s) in
+ name, fun s ->
+ if s.[0] = c then
+ let rec find n m =
+ if String.length s <= m then raise More;
+ if s.[m] = c' then
+ if n = 0 then Tok (name, unescape (String.sub s 1 (m-1))), m+1
+ else find (n-1) (m+1)
+ else if s.[m] = c then find (n+1) (m+1)
+ else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c then
+ find n (m+2)
+ else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c' then
+ find n (m+2)
+ else find n (m+1)
+ in find ~-1 0
+ else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s))
+
+ let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s
+
+ let s = ref ""
+
+ let parse g ic =
+ let read_more () = s := !s ^ input_line ic ^ "\n" in
+ let ensure_non_empty n = if n = String.length !s then read_more () in
+ let cut_after s n = String.sub s n (String.length s - n) in
+ let rec wrap f n =
+ try
+ ensure_non_empty n;
+ let _, n' = eat_blanks (cut_after !s n) in
+ ensure_non_empty n';
+ let t, m = f (cut_after !s (n+n')) in
+ let _, m' = eat_blanks (cut_after !s (n+n'+m)) in
+ t, n+n'+m+m'
+ with More -> read_more (); wrap f n in
+ let rec aux n g res : token list * int =
+ match g with
+ | Item (_,f) ->
+ let t, n = wrap f n in
+ t :: res, n
+ | Opt g ->
+ (try let res', n = aux n g [] in Top (List.rev res') :: res, n
+ with Err _ -> Top [] :: res, n)
+ | Alt gl ->
+ let rec fst = function
+ | [] -> raise (Err ("No more alternatives for: "^cut_after !s n))
+ | g :: gl ->
+ try aux n g res
+ with Err s -> fst gl in
+ fst gl
+ | Seq gl ->
+ let rec all (res,n) = function
+ | [] -> res, n
+ | g :: gl -> all (aux n g res) gl in
+ all (res,n) gl in
+ let res, n = aux 0 g [] in
+ s := cut_after !s n;
+ List.rev res
+
+ let clean s = Str.global_replace (Str.regexp "\n") "\\n" s
+
+ let rec print g =
+ match g with
+ | Item (s,_) -> Printf.sprintf "%s" (clean s)
+ | Opt g -> Printf.sprintf "[%s]" (print g)
+ | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs))
+ | Seq gs -> String.concat " " (List.map print gs)
+
+ let rec print_toklist = function
+ | [] -> ""
+ | Tok(k,v) :: rest when k = v -> clean k ^ " " ^ print_toklist rest
+ | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest
+ | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest
+
+end (* }}} *)
+
+type sentence = {
+ name : string;
+ text : string;
+ edit_id : int;
+}
+
+let doc : sentence Document.document = Document.create ()
+
+let tip_id () =
+ try Document.tip doc
+ with
+ | Document.Empty -> Stateid.initial
+ | Invalid_argument _ -> error "add_sentence on top of non assigned tip"
+
+let add_sentence =
+ let edit_id = ref 0 in
+ fun ?(name="") text ->
+ let tip_id = tip_id () in
+ decr edit_id;
+ Document.push doc { name; text; edit_id = !edit_id };
+ !edit_id, tip_id
+
+let print_document () =
+ let ellipsize s =
+ Str.global_replace (Str.regexp "^[\n ]*") ""
+ (if String.length s > 20 then String.sub s 0 17 ^ "..."
+ else s) in
+ pperr_endline (
+ (Document.print doc
+ (fun b state_id { name; text } ->
+ Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
+ (if b then "*" else " ")
+ name
+ (Stateid.to_string (Option.default Stateid.dummy state_id))
+ (ellipsize text)))))
+
+(* This module is the logic a GUI has to implement *)
+module GUILogic = struct
+
+ let after_add = function
+ | Interface.Fail (_,_,s) -> print_error s; exit 1
+ | Interface.Good (id, (Util.Inl (), _)) ->
+ Document.assign_tip_id doc id
+ | Interface.Good (id, (Util.Inr tip, _)) ->
+ Document.assign_tip_id doc id;
+ Document.unfocus doc;
+ ignore(Document.cut_at doc tip);
+ print_document ()
+
+ let at id id' _ = Stateid.equal id' id
+
+ let after_edit_at (id,need_unfocus) = function
+ | Interface.Fail (_,_,s) -> print_error s; exit 1
+ | Interface.Good (Util.Inl ()) ->
+ if need_unfocus then Document.unfocus doc;
+ ignore(Document.cut_at doc id);
+ print_document ()
+ | Interface.Good (Util.Inr (stop_id,(start_id,tip))) ->
+ if need_unfocus then Document.unfocus doc;
+ ignore(Document.cut_at doc tip);
+ Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id);
+ ignore(Document.cut_at doc id);
+ print_document ()
+
+ let get_id_pred pred =
+ try Document.find_id doc pred
+ with Not_found -> error "No state found"
+
+ let get_id id = get_id_pred (fun _ { name } -> name = id)
+
+ let after_fail coq = function
+ | Interface.Fail (safe_id,_,s) ->
+ prerr_endline "The command failed as expected";
+ let to_id, need_unfocus =
+ get_id_pred (fun id _ -> Stateid.equal id safe_id) in
+ after_edit_at (to_id, need_unfocus)
+ (base_eval_call (Xmlprotocol.edit_at to_id) coq)
+ | Interface.Good _ -> error "The command was expected to fail but did not"
+
+end
+
+open GUILogic
+
+let eval_print l coq =
+ let open Parser in
+ let open Xmlprotocol in
+ (* prerr_endline ("Interpreting: " ^ print_toklist l); *)
+ match l with
+ | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] ->
+ let eid, tip = add_sentence phrase in
+ after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
+ | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] ->
+ let eid, tip = add_sentence ~name phrase in
+ after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
+ | [ Tok(_,"GOALS"); ] ->
+ eval_call (goals ()) coq
+ | [ Tok(_,"FAILGOALS"); ] ->
+ after_fail coq (base_eval_call ~fail:false (goals ()) coq)
+ | [ Tok(_,"EDIT_AT"); Tok(_,id) ] ->
+ let to_id, need_unfocus = get_id id in
+ after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
+ | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
+ eval_call (query (0,(phrase,tip_id()))) coq
+ | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
+ let to_id, _ = get_id id in
+ eval_call (query (0,(phrase, to_id))) coq
+ | [ Tok(_,"WAIT") ] ->
+ eval_call (wait ()) coq
+ | [ Tok(_,"JOIN") ] ->
+ eval_call (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("#[^\n]*",_) :: _ -> ()
+ | _ -> error "syntax error"
+
+let grammar =
+ let open Parser in
+ let eat_id = eat_rex "[a-zA-Z_][a-zA-Z0-9_]*" in
+ let eat_phrase = eat_balanced '{' in
+ Alt
+ [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase]
+ ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
+ ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
+ ; Seq [Item (eat_rex "WAIT")]
+ ; Seq [Item (eat_rex "JOIN")]
+ ; Seq [Item (eat_rex "GOALS")]
+ ; Seq [Item (eat_rex "FAILGOALS")]
+ ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]
+ ; Item (eat_rex "#[^\n]*")
+ ]
+
+let read_command inc = Parser.parse grammar inc
+
+let usage () =
+ error (Printf.sprintf
+ "A fake coqide process talking to a coqtop -toploop coqidetop.\n\
+ Usage: %s (file|-) [<coqtop>]\n\
+ Input syntax is the following:\n%s\n"
+ (Filename.basename Sys.argv.(0))
+ (Parser.print grammar))
+
+module Coqide = Spawn.Sync ()
+
+let main =
+ if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
+ (Sys.Signal_handle
+ (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
+ let def_args = ["--xml_format=Ppcmds"] in
+ let idetop_name = System.get_toplevel_path "coqidetop" in
+ let coqtop_args, input_file = match Sys.argv with
+ | [| _; f |] -> Array.of_list def_args, f
+ | [| _; f; ct |] ->
+ let ct = Str.split (Str.regexp " ") ct in
+ Array.of_list (def_args @ ct), f
+ | _ -> usage () in
+ let inc = if input_file = "-" then stdin else open_in input_file in
+ let coq =
+ let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in
+ let ip = Xml_parser.make (Xml_parser.SChannel cin) in
+ let op = Xml_printer.make (Xml_printer.TChannel cout) in
+ Xml_parser.check_eof ip false;
+ { xml_printer = op; xml_parser = ip } in
+ let init () =
+ match base_eval_call ~print:false (Xmlprotocol.init None) coq with
+ | Interface.Good id ->
+ let dir = Filename.dirname input_file in
+ let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in
+ let eid, tip = add_sentence ~name:"initial" phrase in
+ after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq)
+ | Interface.Fail _ -> error "init call failed" in
+ let finish () =
+ match base_eval_call (Xmlprotocol.status true) coq with
+ | Interface.Good _ -> exit 0
+ | Interface.Fail (_,_,s) -> print_error s; exit 1 in
+ (* The main loop *)
+ init ();
+ while true do
+ let cmd = try read_command inc with End_of_file -> finish () in
+ try eval_print cmd coq
+ with e -> error ("Uncaught exception " ^ Printexc.to_string e)
+ done
+
+(* vim:set foldmethod=marker: *)
diff --git a/ide/fileOps.ml b/ide/fileOps.ml
index 7acd2c37a9..e4c8942cf1 100644
--- a/ide/fileOps.ml
+++ b/ide/fileOps.ml
@@ -18,10 +18,10 @@ object
method filename : string option
method update_stats : unit
method changed_on_disk : bool
- method revert : unit
+ method revert : ?parent:GWindow.window -> unit -> unit
method auto_save : unit
method save : string -> bool
- method saveas : string -> bool
+ method saveas : ?parent:GWindow.window -> string -> bool
end
class fileops (buffer:GText.buffer) _fn (reset_handler:unit->unit) =
@@ -48,7 +48,7 @@ object(self)
false
|_ -> false
- method revert =
+ method revert ?parent () =
let do_revert f =
push_info "Reverting buffer";
try
@@ -72,13 +72,14 @@ object(self)
| Some f ->
if not buffer#modified then do_revert f
else
- let answ = GToolbox.question_box
+ let answ = Configwin_ihm.question_box
~title:"Modified buffer changed on disk"
~buttons:["Revert from File";
"Overwrite File";
"Disable Auto Revert"]
~default:0
~icon:(stock_to_widget `DIALOG_WARNING)
+ ?parent
"Some unsaved buffers changed on disk"
in
match answ with
@@ -102,13 +103,14 @@ object(self)
end
else false
- method saveas f =
+ method saveas ?parent f =
if not (Sys.file_exists f) then self#save f
else
- let answ = GToolbox.question_box ~title:"File exists on disk"
+ let answ = Configwin_ihm.question_box ~title:"File exists on disk"
~buttons:["Overwrite"; "Cancel";]
~default:1
~icon:(warn_image ())#coerce
+ ?parent
("File "^f^" already exists")
in
match answ with
diff --git a/ide/fileOps.mli b/ide/fileOps.mli
index 9a1f0cb738..44a19f9981 100644
--- a/ide/fileOps.mli
+++ b/ide/fileOps.mli
@@ -16,10 +16,10 @@ object
method filename : string option
method update_stats : unit
method changed_on_disk : bool
- method revert : unit
+ method revert : ?parent:GWindow.window -> unit -> unit
method auto_save : unit
method save : string -> bool
- method saveas : string -> bool
+ method saveas : ?parent:GWindow.window -> string -> bool
end
class fileops : GText.buffer -> string option -> (unit -> unit) -> ops
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 9f5c992444..d554bebdd3 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 96ea8c410e..a7ade71307 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 df988d8f11..050c282ef6 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.ml b/ide/idetop.ml
index 2e552b60bb..a2b85041e8 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,27 @@ 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 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 -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (6)"))
+ | 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))
+ end else
+ Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+ with Proof_global.NoCurrentProof -> None;;
let evars () =
try
@@ -231,10 +250,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 +291,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 +304,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,7 +372,6 @@ 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)
@@ -430,7 +449,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. *)
@@ -458,7 +477,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 ();
@@ -507,14 +526,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; opts = Coqargs.default_opts } in
+ start_coq custom
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index bdb39e94a1..7044263b94 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,25 +324,22 @@ 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
- if Sys.file_exists new_prog then new_prog
+ | Some s -> s
+ | None ->
+ try
+ let new_prog = System.get_toplevel_path "coqidetop" in
+ (* The file exists or it is to be found by path *)
+ if Sys.file_exists new_prog ||
+ CString.equal Filename.(basename new_prog) new_prog
+ then new_prog
else
let in_macos_bundle =
Filename.concat
(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.opt"
+ with Not_found -> "coqidetop.opt"
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 2be5dce426..f2913b1d1d 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 11aaf6e8cc..045d650c1c 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 *)
@@ -166,7 +167,7 @@ object
method into l =
try
Some (CList.map (fun s ->
- let split = CString.split sep s in
+ let split = String.split_on_char sep s in
CList.nth split 0, CList.nth split 1) l)
with Failure _ -> None
end
@@ -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
@@ -342,8 +345,15 @@ let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/"
let modifiers_valid =
new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
+let browser_cmd_fmt =
+ try
+ let coq_netscape_remote_var = "COQREMOTEBROWSER" in
+ Sys.getenv coq_netscape_remote_var
+ with
+ Not_found -> Coq_config.browser
+
let cmd_browse =
- new preference ~name:["cmd_browse"] ~init:Flags.browser_cmd_fmt ~repr:Repr.(string)
+ new preference ~name:["cmd_browse"] ~init:browser_cmd_fmt ~repr:Repr.(string)
let cmd_editor =
let init = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s" in
@@ -356,6 +366,14 @@ let text_font =
in
new preference ~name:["text_font"] ~init ~repr:Repr.(string)
+let is_standard_doc_url url =
+ let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
+ let n = String.length Coq_config.wwwcoq in
+ let n' = String.length Coq_config.wwwrefman in
+ url = Coq_config.localwwwrefman ||
+ url = Coq_config.wwwrefman ||
+ url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
+
let doc_url =
object
inherit [string] preference
@@ -363,7 +381,7 @@ object
as super
method! set v =
- if not (Flags.is_standard_doc_url v) &&
+ if not (is_standard_doc_url v) &&
v <> use_default_doc_url &&
(* Extra hack to support links to last released doc version *)
v <> Coq_config.wwwcoq ^ "doc" &&
@@ -429,12 +447,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 +489,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 +505,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 +525,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 +580,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 +595,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 +609,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 +622,7 @@ object (self)
tag_bold = bold#active;
tag_italic = italic#active;
tag_underline = underline#active;
+ tag_strikethrough = strikethrough#active;
}
initializer
@@ -599,6 +636,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 +644,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
@@ -649,11 +688,7 @@ let pmodifiers ?(all = false) name p = modifiers
name
(str_to_mod_list p#get)
-[@@@ocaml.warning "-3"] (* String.uppercase_ascii since 4.03.0 GPR#124 *)
-let uppercase = String.uppercase
-[@@@ocaml.warning "+3"]
-
-let configure ?(apply=(fun () -> ())) () =
+let configure ?(apply=(fun () -> ())) parent =
let cmd_coqtop =
string
~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s))
@@ -979,7 +1014,7 @@ let configure ?(apply=(fun () -> ())) () =
let k =
if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k
else "" in
- let k = uppercase k in
+ let k = String.uppercase_ascii k in
[q, k]
in
@@ -1033,7 +1068,7 @@ let configure ?(apply=(fun () -> ())) () =
(*
Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font);
*)
- let x = edit ~apply "Customizations" cmds in
+ let x = edit ~apply "Customizations" ~parent cmds in
(*
Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string current.text_font);
*)
diff --git a/ide/preferences.mli b/ide/preferences.mli
index ccf028aee4..7ed6a40bdb 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,11 +102,12 @@ 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
-val configure : ?apply:(unit -> unit) -> unit -> unit
+val configure : ?apply:(unit -> unit) -> GWindow.window -> unit
val stick : 'a preference ->
(#GObj.widget as 'obj) -> ('a -> unit) -> unit
diff --git a/ide/protocol/dune b/ide/protocol/dune
new file mode 100644
index 0000000000..801ceb20ec
--- /dev/null
+++ b/ide/protocol/dune
@@ -0,0 +1,7 @@
+(library
+ (name protocol)
+ (public_name coqide-server.protocol)
+ (wrapped false)
+ (libraries coq.lib))
+
+(ocamllex xml_lexer)
diff --git a/ide/protocol/ideprotocol.mllib b/ide/protocol/ideprotocol.mllib
new file mode 100644
index 0000000000..8317a08681
--- /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 debbc8301e..debbc8301e 100644
--- a/ide/interface.mli
+++ b/ide/protocol/interface.ml
diff --git a/ide/richpp.ml b/ide/protocol/richpp.ml
index 19e9799c19..19e9799c19 100644
--- a/ide/richpp.ml
+++ b/ide/protocol/richpp.ml
diff --git a/ide/richpp.mli b/ide/protocol/richpp.mli
index 31fc7b56f1..31fc7b56f1 100644
--- a/ide/richpp.mli
+++ b/ide/protocol/richpp.mli
diff --git a/ide/serialize.ml b/ide/protocol/serialize.ml
index 86074d44d5..86074d44d5 100644
--- a/ide/serialize.ml
+++ b/ide/protocol/serialize.ml
diff --git a/ide/serialize.mli b/ide/protocol/serialize.mli
index af082f25b1..af082f25b1 100644
--- a/ide/serialize.mli
+++ b/ide/protocol/serialize.mli
diff --git a/ide/xml_lexer.mli b/ide/protocol/xml_lexer.mli
index e61cb055f7..e61cb055f7 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 4a52147e17..e8bf7e16ae 100644
--- a/ide/xml_lexer.mll
+++ b/ide/protocol/xml_lexer.mll
@@ -83,9 +83,6 @@ let error lexbuf e =
last_pos := lexeme_start lexbuf;
raise (Error e)
-[@@@ocaml.warning "-3"] (* String.lowercase_ascii since 4.03.0 GPR#124 *)
-let lowercase = String.lowercase
-[@@@ocaml.warning "+3"]
}
let newline = ['\n']
@@ -222,7 +219,7 @@ and entity = parse
{
let ident = lexeme lexbuf in
try
- Hashtbl.find idents (lowercase ident)
+ Hashtbl.find idents (String.lowercase_ascii ident)
with
Not_found -> "&" ^ ident
}
diff --git a/ide/xml_parser.ml b/ide/protocol/xml_parser.ml
index 8db3f9e8ba..8db3f9e8ba 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 ac2eab352f..ac2eab352f 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 488ef7bf57..488ef7bf57 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 178f7c808f..178f7c808f 100644
--- a/ide/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
diff --git a/ide/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e18219210f..e18219210f 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
diff --git a/ide/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli
index ba6000f0a0..ba6000f0a0 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/protocol/xmlprotocol.mli
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 8eddfb3149..06281d6287 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
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index b3088ee288..9be562d3ed 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -103,7 +103,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat
else []
in
proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt);
- insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal);
+ insert_xml ~tags:[Tags.Proof.goal] proof#buffer (Richpp.richpp_of_pp width cur_goal);
proof#buffer#insert "\n"
in
(* Insert remaining goals (no hypotheses) *)
@@ -128,7 +128,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat
ignore(proof#buffer#place_cursor
~where:(proof#buffer#end_iter#backward_to_tag_toggle
(Some Tags.Proof.goal)));
- ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT)
+ ignore(proof#scroll_to_mark `INSERT)
let rec flatten = function
| [] -> []
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 13:18:18 +0000