aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build8
-rw-r--r--Makefile.common10
-rw-r--r--_tags2
-rw-r--r--ide/config_lexer.mll2
-rw-r--r--ide/config_parser.mly4
-rw-r--r--ide/coq.ml28
-rw-r--r--ide/coq.mli3
-rw-r--r--ide/coqide.ml13
-rw-r--r--ide/coqide_main.ml45
-rw-r--r--ide/ide.mllib1
-rw-r--r--ide/ideproof.ml2
-rw-r--r--ide/ideutils.ml5
-rw-r--r--ide/minilib.ml63
-rw-r--r--ide/minilib.mli24
-rw-r--r--ide/preferences.ml19
-rw-r--r--ide/typed_notebook.ml12
-rw-r--r--myocamlbuild.ml10
17 files changed, 137 insertions, 74 deletions
diff --git a/Makefile.build b/Makefile.build
index 529238d674..eefafb0cb2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -313,16 +313,16 @@ coqide-byte: $(COQIDEBYTE) $(COQIDE)
coqide-opt: $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
coqide-files: $(IDEFILES)
-$(COQIDEOPT): $(LINKIDEOPT) $(LIBCOQRUN) $(COQTOPOPT)
+$(COQIDEOPT): $(LINKIDEOPT)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa\
- gtkThread.cmx dynlink.cmxa str.cmxa $(CAMLP4MOD).cmxa $(LIBCOQRUN) $(LINKIDEOPT)
+ gtkThread.cmx str.cmxa $(LINKIDEOPT)
$(STRIP) $@
-$(COQIDEBYTE): $(LINKIDE) $(LIBCOQRUN) $(COQTOPBYTE)
+$(COQIDEBYTE): $(LINKIDE)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\
- dynlink.cma str.cma $(CAMLP4MOD).cma $(COQRUNBYTEFLAGS) $(LIBCOQRUN) $(LINKIDE)
+ str.cma $(COQRUNBYTEFLAGS) $(LINKIDE)
$(COQIDE):
cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
diff --git a/Makefile.common b/Makefile.common
index c51ca4011a..ce99603fee 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -217,15 +217,11 @@ INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS))
LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS)
LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
-LIBCMA:=lib/lib.cma
+IDEDEPS:=$(CONFIG) lib/flags.cmo toplevel/ide_intf.cmo
IDECMA:=ide/ide.cma
-IDEINTF:=toplevel/ide_intf.cmo
-IDELIBS:=$(CONFIG) $(LIBCMA) $(IDEINTF) $(IDECMA)
-IDELIBSOPT:=$(subst .cmo,.cmx,$(IDELIBS:.cma=.cmxa))
-
-LINKIDE:=$(IDELIBS) ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTDEPS) $(IDELIBSOPT) ide/coqide_main_opt.ml
+LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml
+LINKIDEOPT:=$(IDEDEPS:.cmo=.cmx) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml
# modules known by the toplevel of Coq
diff --git a/_tags b/_tags
index dafce3b300..e6ac5e6d0a 100644
--- a/_tags
+++ b/_tags
@@ -8,7 +8,7 @@
<tools/coq_tex.{native,byte}> : use_str
<tools/coq_makefile.{native,byte}> : use_str
<tools/coqdoc/main.{native,byte}> : use_str
-<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide, use_dynlink, use_camlp4, use_libcoqrun
+<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide
<checker/main.{native,byte}> : use_str, use_unix, use_dynlink, use_camlp4
<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 8d9ede0787..1aaf2b71a4 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -11,7 +11,7 @@
open Lexing
open Format
open Config_parser
- open Util
+ open Minilib
let string_buffer = Buffer.create 1024
diff --git a/ide/config_parser.mly b/ide/config_parser.mly
index 8c414d3880..4ab6950b72 100644
--- a/ide/config_parser.mly
+++ b/ide/config_parser.mly
@@ -9,14 +9,14 @@
%{
open Parsing
- open Util
+ open Minilib
%}
%token <string> IDENT STRING
%token EQUAL EOF
-%type <(string list) Util.Stringmap.t> prefs
+%type <(string list) Minilib.Stringmap.t> prefs
%start prefs
%%
diff --git a/ide/coq.ml b/ide/coq.ml
index 96048c3b30..b1bb1f1831 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,9 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
-open Compat
-open Pp
open Ideutils
type coqtop = {
@@ -21,18 +18,6 @@ type coqtop = {
let prerr_endline s = if !debug then prerr_endline s else ()
-let output = ref (Format.formatter_of_out_channel stdout)
-
-let msg m =
- let b = Buffer.create 103 in
- Pp.msg_with (Format.formatter_of_buffer b) m;
- Buffer.contents b
-
-let msgnl m =
- (msg m)^"\n"
-
-let i = ref 0
-
let get_version_date () =
let date =
if Glib.Utf8.validate Coq_config.date
@@ -77,7 +62,8 @@ let coqtop_path () =
let filter_coq_opts args =
let argstr = String.concat " " (List.map Filename.quote args) in
- let oc,ic,ec = Unix.open_process_full (coqtop_path () ^" -nois -filteropts "^argstr) (Unix.environment ()) in
+ let cmd = coqtop_path () ^" -nois -filteropts " ^ argstr in
+ let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
let filtered_args = read_all_lines oc in
let message = read_all_lines ec in
match Unix.close_process_full (oc,ic,ec) with
@@ -102,6 +88,16 @@ let check_connection args =
List.iter Pervasives.prerr_endline lines;
exit 1
+(* TODO: we can probably merge check_connection () and coqlib () *)
+
+let coqlib () =
+ try
+ let ic = Unix.open_process_in (coqtop_path () ^" -where") in
+ let str = input_line ic in
+ ignore (Unix.close_process_in ic);
+ str
+ with _ -> failwith "Error while reading coqlib from coqtop"
+
let eval_call coqtop (c:'a Ide_intf.call) =
Marshal.to_channel coqtop.cin c [];
flush coqtop.cin;
diff --git a/ide/coq.mli b/ide/coq.mli
index 148840be26..37c5bcd006 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -10,6 +10,7 @@ val short_version : unit -> string
val version : unit -> string
val filter_coq_opts : string list -> bool * string list
val check_connection : string list -> unit
+val coqlib : unit -> string
type coqtop
@@ -56,5 +57,3 @@ val make_cases : coqtop -> string -> string list list Ide_intf.value
val current_status : coqtop -> string Ide_intf.value
val goals : coqtop -> Ide_intf.goals Ide_intf.value
-
-val msgnl : Pp.std_ppcmds -> string
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e553ca0b46..1bb3088538 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Preferences
-open Vernacexpr
open Coq
open Coq.PrintOpt
open Gtk_parsing
@@ -1003,7 +1002,7 @@ object(self)
(try
while ((stop#compare (get_current())>=0)
&& (self#process_next_phrase false false false))
- do Util.check_for_interrupt () done
+ do () (* TODO: this looks obsolete : Util.check_for_interrupt ()*) done
with Sys.Break ->
prerr_endline "Interrupted during process_until_iter_or_error");
sync (fun _ ->
@@ -1185,7 +1184,7 @@ object(self)
act_id <- Some
(input_view#event#connect#key_press ~callback:self#active_keypress_handler);
prerr_endline "CONNECTED active : ";
- print_id (Option.get act_id);
+ print_id (match act_id with Some x -> x | None -> assert false);
match
filename
with
@@ -1562,7 +1561,7 @@ let do_print session =
|Some f_name -> begin
let cmd =
"cd " ^ Filename.quote (Filename.dirname f_name) ^ "; " ^
- !current.cmd_coqdoc ^ "--coqlib_path " ^Envars.coqlib () ^
+ !current.cmd_coqdoc ^ "--coqlib_path " ^ !Minilib.coqlib ^
" -ps " ^ Filename.quote (Filename.basename f_name) ^
" | " ^ !current.cmd_print
in
@@ -1588,7 +1587,7 @@ let load_file handler f =
let f = absolute_filename f in
try
prerr_endline "Loading file starts";
- if not (Util.list_fold_left_i
+ if not (Minilib.list_fold_left_i
(fun i found x -> if found then found else
let {analyzed_view=av} = x in
(match av#filename with
@@ -1824,7 +1823,7 @@ let main files =
in
let cmd =
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
- !current.cmd_coqdoc ^ "--coqlib_path " ^Envars.coqlib () ^ " --" ^ kind ^
+ !current.cmd_coqdoc ^ "--coqlib_path " ^ !Minilib.coqlib ^ " --" ^ kind ^
" -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
in
let s,_ = run_command av#insert_message cmd in
@@ -2199,7 +2198,7 @@ let main files =
| None -> warning "Call to external editor available only on named files"
| Some f ->
save_f ();
- let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in
+ let com = Minilib.subst_command_placeholder !current.cmd_editor (Filename.quote f) in
let _ = run_command av#insert_message com in
av#revert)
in
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 4bb80f4a79..4db3ba1436 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -16,10 +16,11 @@ let () =
let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
Coqide.sup_args := List.map Filename.quote args;
Coq.check_connection !Coqide.sup_args;
+ Minilib.coqlib := Coq.coqlib ();
Coqide.ignore_break ();
GtkMain.Rc.add_default_file (Ideutils.lib_ide_file ".coqide-gtk2rc");
(try
- GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
+ GtkMain.Rc.add_default_file (Filename.concat Minilib.home ".coqide-gtk2rc");
with Not_found -> ());
ignore (GtkMain.Main.init ());
initmac () ;
@@ -30,7 +31,7 @@ let () =
`WARNING;`CRITICAL]
(fun ~level msg ->
if level land Glib.Message.log_level `WARNING <> 0
- then Pp.warning msg
+ then Printf.eprintf "Warning: %s\n" msg
else failwith ("Coqide internal error: " ^ msg)));
Coqide.main files;
if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ());
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 87b66babae..4861f61e6c 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -1,3 +1,4 @@
+Minilib
Okey
Config_file
Configwin_keys
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 701203061f..783ade6048 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -69,7 +69,7 @@ let mode_tactic sel_cb (proof:GText.view) = function
proof#buffer#insert head_str;
List.iter insert_hyp hyps;
insert_goal cur_goal cur_goal_menu 1 goals_cnt;
- Util.list_fold_left_i (fun i _ (_,(g,_)) -> insert_goal g [] i goals_cnt) 2 () rem_goals;
+ Minilib.list_fold_left_i (fun i _ (_,(g,_)) -> insert_goal g [] i goals_cnt) 2 () rem_goals;
ignore(proof#buffer#place_cursor
~where:((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2)));
ignore(proof#scroll_to_mark `INSERT)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 319cf4e4d2..a4126ae33d 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,8 +37,7 @@ let prerr_string s =
if !debug then (prerr_string s;flush stderr)
let lib_ide_file f =
- let coqlib = Envars.coqlib () in
- Filename.concat (Filename.concat coqlib "ide") f
+ Filename.concat (Filename.concat !Minilib.coqlib "ide") f
let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
@@ -284,7 +283,7 @@ let run_command f c =
(Unix.close_process_full (cin,cout,cerr), Buffer.contents result)
let browse f url =
- let com = Flags.subst_command_placeholder !current.cmd_browse url in
+ let com = Minilib.subst_command_placeholder !current.cmd_browse url in
let s = Sys.command com in
if s = 127 then
f ("Could not execute\n\""^com^
diff --git a/ide/minilib.ml b/ide/minilib.ml
new file mode 100644
index 0000000000..b791d779ca
--- /dev/null
+++ b/ide/minilib.ml
@@ -0,0 +1,63 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(** Some excerpt of Util and similar files to avoid loading the whole
+ module and its dependencies (and hence Compat and Camlp4) *)
+
+module Stringmap = Map.Make(String)
+
+let list_fold_left_i f =
+ let rec it_list_f i a = function
+ | [] -> a
+ | b::l -> it_list_f (i+1) (f i a b) l
+ in
+ it_list_f
+
+(* [list_chop i l] splits [l] into two lists [(l1,l2)] such that
+ [l1++l2=l] and [l1] has length [i].
+ It raises [Failure] when [i] is negative or greater than the length of [l] *)
+
+let list_chop n l =
+ let rec chop_aux i acc = function
+ | tl when i=0 -> (List.rev acc, tl)
+ | h::t -> chop_aux (pred i) (h::acc) t
+ | [] -> failwith "list_chop"
+ in
+ chop_aux n [] l
+
+
+let list_map_i f =
+ let rec map_i_rec i = function
+ | [] -> []
+ | x::l -> let v = f i x in v :: map_i_rec (i+1) l
+ in
+ map_i_rec
+
+
+let list_index x =
+ let rec index_x n = function
+ | y::l -> if x = y then n else index_x (succ n) l
+ | [] -> raise Not_found
+ in
+ index_x 1
+
+let list_index0 x l = list_index x l - 1
+
+let list_filter_i p =
+ let rec filter_i_rec i = function
+ | [] -> []
+ | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l'
+ in
+ filter_i_rec 0
+
+let subst_command_placeholder s t =
+ Str.global_replace (Str.regexp_string "%s") s t
+
+let home = try Sys.getenv "HOME" with Not_found -> "."
+
+let coqlib = ref ""
diff --git a/ide/minilib.mli b/ide/minilib.mli
new file mode 100644
index 0000000000..aac3e3d77d
--- /dev/null
+++ b/ide/minilib.mli
@@ -0,0 +1,24 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(** Some excerpts of Util and similar files to avoid depending on them
+ and hence on Compat and Camlp4 *)
+
+module Stringmap : Map.S with type key = string
+
+val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
+val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+val list_filter_i : (int -> 'a -> bool) -> 'a list -> 'a list
+val list_chop : int -> 'a list -> 'a list * 'a list
+val list_index0 : 'a -> 'a list -> int
+
+val subst_command_placeholder : string -> string -> string
+
+val home : string
+
+val coqlib : string ref
diff --git a/ide/preferences.ml b/ide/preferences.ml
index a6aaef2576..e31a5904af 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -8,11 +8,10 @@
open Configwin
open Printf
-open Util
-let pref_file = Filename.concat System.home ".coqiderc"
+let pref_file = Filename.concat Minilib.home ".coqiderc"
-let accel_file = Filename.concat System.home ".coqide.keys"
+let accel_file = Filename.concat Minilib.home ".coqide.keys"
let mod_to_str (m:Gdk.Tags.modifier) =
match m with
@@ -170,9 +169,9 @@ let save_pref () =
with _ -> ());
let p = !current in
try
- let add = Stringmap.add in
+ let add = Minilib.Stringmap.add in
let (++) x f = f x in
- Stringmap.empty ++
+ Minilib.Stringmap.empty ++
add "cmd_coqc" [p.cmd_coqc] ++
add "cmd_make" [p.cmd_make] ++
add "cmd_coqmakefile" [p.cmd_coqmakefile] ++
@@ -228,7 +227,7 @@ let load_pref () =
try
let m = Config_lexer.load_file pref_file in
let np = { p with cmd_coqc = p.cmd_coqc } in
- let set k f = try let v = Stringmap.find k m in f v with _ -> () in
+ let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in
let set_hd k f = set k (fun v -> f (List.hd v)) in
let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
let set_int k f = set_hd k (fun v -> f (int_of_string v)) in
@@ -295,14 +294,6 @@ let load_pref () =
prerr_endline ("Could not load preferences ("^
(Printexc.to_string e)^").")
-let split_string_format s =
- try
- let i = Util.string_index_from s 0 "%s" in
- let pre = (String.sub s 0 i) in
- let post = String.sub s (i+2) (String.length s - i - 2) in
- pre,post
- with Not_found -> s,""
-
let configure ?(apply=(fun () -> ())) () =
let cmd_coqc =
string
diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index 048cc6e24a..499d56bd9a 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -16,14 +16,14 @@ object(self)
(* XXX - Temporary hack to compile with archaic lablgtk *)
ignore (super#append_page ?tab_label ?menu_label page);
let real_pos = super#page_num page in
- let lower,higher = Util.list_chop real_pos term_list in
+ let lower,higher = Minilib.list_chop real_pos term_list in
term_list <- lower@[term]@higher;
real_pos
(* XXX - Temporary hack to compile with archaic lablgtk
method insert_term ?(build=default_build) ?pos (term:'a) =
let tab_label,menu_label,page = build term in
let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in
- let lower,higher = Util.list_chop real_pos term_list in
+ let lower,higher = Minilib.list_chop real_pos term_list in
term_list <- lower@[term]@higher;
real_pos
*)
@@ -32,26 +32,26 @@ object(self)
(* XXX - Temporary hack to compile with archaic lablgtk *)
ignore (super#prepend_page ?tab_label ?menu_label page);
let real_pos = super#page_num page in
- let lower,higher = Util.list_chop real_pos term_list in
+ let lower,higher = Minilib.list_chop real_pos term_list in
term_list <- lower@[term]@higher;
real_pos
method set_term (term:'a) =
let tab_label,menu_label,page = make_page term in
let real_pos = super#current_page in
- term_list <- Util.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
+ term_list <- Minilib.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
super#set_page ?tab_label ?menu_label page
method get_nth_term i =
List.nth term_list i
method term_num p =
- Util.list_index0 p term_list
+ Minilib.list_index0 p term_list
method pages = term_list
method remove_page index =
- term_list <- Util.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
+ term_list <- Minilib.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
super#remove_page index
method current_term =
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 6a7d18ebf7..8565c1482b 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -112,10 +112,6 @@ let core_cma = List.map (fun s -> s^".cma") core_libs
let core_cmxa = List.map (fun s -> s^".cmxa") core_libs
let core_mllib = List.map (fun s -> s^".mllib") core_libs
-let ide_cma = "ide/ide.cma"
-let ide_cmxa = "ide/ide.cmxa"
-let ide_mllib = "ide/ide.mllib"
-
let tolink = "scripts/tolink.ml"
let c_headers_base =
@@ -371,16 +367,14 @@ let extra_rules () = begin
(** Generation of tolink.ml *)
- rule tolink ~deps:(ide_mllib::core_mllib) ~prod:tolink
+ rule tolink ~deps:core_mllib ~prod:tolink
(fun _ _ ->
let cat s = String.concat " " (string_list_of_file s) in
let core_mods = String.concat " " (List.map cat core_mllib) in
- let ide_mods = cat ide_mllib in
let core_cmas = String.concat " " core_cma in
Echo (["let copts = \"-cclib -lcoqrun\"\n";
"let core_libs = \"coq_config.cmo "^core_cmas^"\"\n";
- "let core_objs = \"Coq_config "^core_mods^"\"\n";
- "let ide = \""^ide_mods^"\"\n"],
+ "let core_objs = \"Coq_config "^core_mods^"\"\n"],
tolink));
(** Coqtop *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:41:12 +0000