aide contextuelle / menus compilation + print + export

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3698 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 764 insertions, 31 deletions

diff --git a/.depend b/.depend
index d689b6b729..5d45780062 100644
--- a/.depend
+++ b/.depend
@@ -469,6 +469,8 @@ ide/find_phrase.cmo: ide/ideutils.cmo
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmo 
 ide/highlight.cmx: ide/ideutils.cmx 
+ide/ideutils.cmo: config/coq_config.cmi ide/preferences.cmo 
+ide/ideutils.cmx: config/coq_config.cmx ide/preferences.cmx 
 interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \
     kernel/inductive.cmi library/libnames.cmi library/nameops.cmi \
diff --git a/Makefile b/Makefile
index b0be198ef2..4ec92ca607 100644
--- a/Makefile
+++ b/Makefile
@@ -422,11 +422,16 @@ COQIDEBYTE=bin/coqide.byte$(EXE)
 COQIDEOPT=bin/coqide.opt$(EXE)
 COQIDE=bin/coqide.$(BEST)$(EXE)
 
-COQIDECMO=ide/ideutils.cmo ide/find_phrase.cmo ide/highlight.cmo ide/coq.cmo ide/coqide.cmo
+COQIDECMO=ide/preferences.cmo \
+	  ide/ideutils.cmo ide/find_phrase.cmo \
+          ide/highlight.cmo ide/coq.cmo ide/coqide.cmo
 COQIDECMX=$(COQIDECMO:.cmo=.cmx)
 COQIDEFLAGS=-I +lablgtk2
 beforedepend:: ide/find_phrase.ml ide/highlight.ml
 
+FULLIDELIB=$(FULLCOQLIB)/ide
+IDEFILES=ide/coq.gif ide/.coqiderc
+
 ide: $(COQIDE)
 
 $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX)
@@ -900,6 +905,8 @@ install-library:
 	cp states/*.coq $(FULLCOQLIB)/states
 	$(MKDIR) $(FULLEMACSLIB)
 	cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
+	$(MKDIR) $(FULLIDELIB)
+	cp $(IDEFILES) $(FULLIDELIB)
 
 install-library-light:
 	$(MKDIR) $(FULLCOQLIB)
diff --git a/distrib/RH/do_build b/distrib/RH/do_build
index c39ec1b538..973d1d914d 100644
--- a/distrib/RH/do_build
+++ b/distrib/RH/do_build
@@ -1,2 +1,2 @@
 ./configure -bindir /usr/bin -libdir /usr/lib/coq -mandir /usr/man -emacs emacs -emacslib /usr/share/emacs/site-lisp -opt -reals all        # Need ocamlc.opt and ocamlopt.opt
-make world check      # Use native coq to compile theories
+make world      # Use native coq to compile theories
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1614c905a1..e045e81eae 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,8 +1,8 @@
+open Preferences
 open Vernacexpr
 open Coq
 open Ideutils
 
-  
 let out_some s = match s with | None -> assert false | Some f -> f
 
 let yes_icon = "gtk-yes"
@@ -21,10 +21,10 @@ let default_monospace_font_name = "Monospace 14"
 let manual_monospace_font = ref None
 let manual_general_font = ref None
 
-let has_config_file = (Sys.file_exists ".coqiderc") || 
-		      (try Sys.file_exists 
-			 (Filename.concat (Sys.getenv "HOME") ".coqiderc")
-		       with Not_found -> false)
+let has_config_file = 
+  (Sys.file_exists (Filename.concat lib_ide ".coqiderc")) || 
+  (try Sys.file_exists (Filename.concat (Sys.getenv "HOME") ".coqiderc")
+   with Not_found -> false)
 
 let _ = if not has_config_file then 
   manual_monospace_font := Some (Pango.Font.from_string default_monospace_font_name);
@@ -138,6 +138,7 @@ object('self)
     method set_message : string -> unit
     method show_goals : unit
     method undo_last_step : unit
+    method help_for_keyword : unit -> unit
   end
 
 let (input_views:analyzed_views viewable_script Vector.t) = Vector.create ()
@@ -800,6 +801,16 @@ object(self)
 	   end;
 	 end;
 	 last_index <- not last_index;)
+
+  method help_for_keyword () =
+    let it = self#get_insert in
+    let start = it#backward_word_start in
+    let stop = start#forward_word_end in
+    let text = input_buffer#get_text ~slice:true ~start ~stop () in
+    try 
+      let u = url_for_keyword text in browse (current.doc_url ^ u) 
+    with _ -> ()
+
   initializer 
     ignore (message_buffer#connect#after#insert_text
 	      ~callback:(fun it s -> ignore 
@@ -890,7 +901,7 @@ let main () =
   let file_factory = new GMenu.factory file_menu ~accel_group in
 
   (* File/Load Menu *)
-  let load_m = file_factory#add_item "Open" ~key:GdkKeysyms._O in
+  let load_m = file_factory#add_item "Open/Create" ~key:GdkKeysyms._O in
   let load_f () = 	  
     match GToolbox.select_file ~title:"Load file" () with 
       | None -> ()
@@ -1000,24 +1011,61 @@ let main () =
   revert_m#misc#set_state `INSENSITIVE;
 
   (* File/Print Menu *)
-  let print_m = file_factory#add_item "Print" in
-  print_m#misc#set_state `INSENSITIVE;
+  let print_f () =
+    let v = get_current_view () in
+    let av = out_some v.analyzed_view in
+    match v.filename with
+      | None -> 
+	  !flash_info "Cannot print: this buffer has no name"
+      | Some f ->
+	  let cmd = 
+	    "cd " ^ Filename.dirname f ^ "; " ^
+	    current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^ 
+	    " | " ^ current.cmd_print
+	  in
+	  let c = Sys.command cmd in
+	  !flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
+  in
+  let print_m = file_factory#add_item "Print" ~callback:print_f in
 
   (* File/Export to Menu *)
+  let export_f kind () =
+    let v = get_current_view () in
+    let av = out_some v.analyzed_view in
+    match v.filename with
+      | None -> 
+	  !flash_info "Cannot print: this buffer has no name"
+      | Some f ->
+	  let basef = Filename.basename f in
+	  let output = 
+	    let basef_we = try Filename.chop_extension basef with _ -> basef in
+	    match kind with
+	      | "latex" -> basef_we ^ ".tex"
+	      | "dvi" | "ps" | "html" -> basef_we ^ "." ^ kind
+	      | _ -> assert false
+	  in
+	  let cmd = 
+	    "cd " ^ Filename.dirname f ^ "; " ^
+	    current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
+	  in
+	  let c = Sys.command cmd in
+	  !flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
+  in
   let file_export_m =  file_factory#add_submenu "Export to" in
 
   let file_export_factory = new GMenu.factory file_export_m ~accel_group in
-  let export_html_m = file_export_factory#add_item "Html" in
-  export_html_m#misc#set_state `INSENSITIVE;
-  
-  let export_latex_m = file_export_factory#add_item "LaTeX" in
-  export_latex_m#misc#set_state `INSENSITIVE;
-
-  let export_dvi_m = file_export_factory#add_item "Dvi" in
-  export_dvi_m#misc#set_state `INSENSITIVE;
-
-  let export_ps_m = file_export_factory#add_item "Ps" in
-  export_ps_m#misc#set_state `INSENSITIVE;
+  let export_html_m = 
+    file_export_factory#add_item "Html" ~callback:(export_f "html") 
+  in
+  let export_latex_m = 
+    file_export_factory#add_item "LaTeX" ~callback:(export_f "latex")
+  in
+  let export_dvi_m = 
+    file_export_factory#add_item "Dvi" ~callback:(export_f "dvi") 
+  in
+  let export_ps_m = 
+    file_export_factory#add_item "Ps" ~callback:(export_f "ps") 
+  in
 
   (* File/Rehighlight Menu *)
   let rehighlight_m = file_factory#add_item "Rehighlight" ~key:GdkKeysyms._L in
@@ -1189,9 +1237,33 @@ let main () =
   (* Commands Menu *)
   let commands_menu =  factory#add_submenu "Commands" in
   let commands_factory = new GMenu.factory commands_menu ~accel_group in
-  ignore (commands_factory#add_item "Compile");
-  ignore (commands_factory#add_item "Make");
-  ignore (commands_factory#add_item "Make Makefile");
+  let compile_f () =
+    let v = get_active_view () in
+    let av = out_some v.analyzed_view in
+    match v.filename with
+      | None -> 
+	  !flash_info "Active buffer has no name"
+      | Some f ->
+	  let c = Sys.command (current.cmd_coqc ^ " " ^ f) in
+	  if c = 0 then
+	    !flash_info (f ^ " successfully compiled")
+	  else begin
+	    !flash_info (f ^ " failed to compile");
+	    av#process_until_end_or_error
+	  end
+  in
+  let compile_m = commands_factory#add_item "Compile" ~callback:compile_f in
+  let make_f () =
+    let c = Sys.command current.cmd_make in
+    !flash_info (current.cmd_make ^ if c = 0 then " succeeded" else " failed")
+  in
+  let make_m = commands_factory#add_item "Make" ~callback:make_f in
+  let coq_makefile_f () =
+    let c = Sys.command current.cmd_coqmakefile in
+    !flash_info 
+      (current.cmd_coqmakefile ^ if c = 0 then " succeeded" else " failed")
+  in
+  let _ = commands_factory#add_item "Make Makefile" ~callback:coq_makefile_f in
 
   (* Configuration Menu *)
 
@@ -1214,6 +1286,28 @@ let main () =
     configuration_factory#add_item "Customize fonts"
       ~callback:(fun () -> font_selector#present ())
   in
+
+  (* Help Menu *)
+
+  let help_menu = factory#add_submenu "Help" in
+  let help_factory = new GMenu.factory help_menu  
+		     ~accel_modi:[]
+		     ~accel_group in
+  let _ = help_factory#add_item "Browse Coq Manual" 
+	  ~callback:(fun () -> browse (current.doc_url ^ "main.html")) in
+  let _ = help_factory#add_item "Browse Coq Library" 
+	  ~callback:(fun () -> browse current.library_url) in
+  let _ = 
+    help_factory#add_item "Help for keyword" ~key:GdkKeysyms._F1
+    ~callback:(fun () -> 
+		 let av = out_some ((get_current_view ()).analyzed_view) in
+		 av#help_for_keyword ())
+  in
+  let _ = help_factory#add_separator () in
+  let about_m = help_factory#add_item "About" in
+
+  (* Window layout *)
+
   let hb = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () in
   let _ = hb#set_position (window_width/2 ) in
   _notebook := Some (GPack.notebook ~packing:hb#add1 ());
@@ -1288,7 +1382,8 @@ let main () =
 			 font_selector#misc#hide ()));
 
   (try 
-     let startup_image = GdkPixbuf.from_file "coq.gif" in
+     let image = Filename.concat lib_ide "coq.gif" in
+     let startup_image = GdkPixbuf.from_file image in
      tv2#buffer#insert_pixbuf ~iter:tv2#buffer#start_iter 
        ~pixbuf:startup_image;
      tv2#buffer#insert ~iter:tv2#buffer#start_iter "\t\t";
@@ -1323,12 +1418,14 @@ let main () =
 
   (match !manual_monospace_font with 
      | None -> ()
-     | Some f -> view#misc#modify_font f; tv2#misc#modify_font f; tv3#misc#modify_font f)
+     | Some f -> view#misc#modify_font f; tv2#misc#modify_font f; tv3#misc#modify_font f);
+  ignore (about_m#connect#activate 
+	  ~callback:(fun () -> tv3#buffer#set_text "by Benjamin Monate"))
     
 let start () = 
   cant_break ();
   Coq.init ();
-  GtkMain.Rc.add_default_file ".coqiderc";
+  GtkMain.Rc.add_default_file (Filename.concat lib_ide ".coqiderc");
   (try 
      GtkMain.Rc.add_default_file (Filename.concat (Sys.getenv "HOME") ".coqiderc");
   with Not_found -> ());
diff --git a/ide/extract_index.mll b/ide/extract_index.mll
new file mode 100644
index 0000000000..1eb2c13d6e
--- /dev/null
+++ b/ide/extract_index.mll
@@ -0,0 +1,22 @@
+
+{
+  open Lexing 
+}
+
+(* additional lexer to extract URL from Coq manual's index *)
+
+rule entry = parse
+  | "<LI><TT>" [^ ',']* "</TT>, "
+      { let s = lexeme lexbuf in
+	let n = String.length s in
+	String.sub s 8 (n - 15), extract_index_url lexbuf }
+  | "<LI>" [^ ',']* ", " 
+      { let s = lexeme lexbuf in
+	let n = String.length s in
+	String.sub s 4 (n - 6), extract_index_url lexbuf }
+
+and extract_index_url = parse
+  | "<A HREF=\"" [^ '"']* '"'
+      { let s = lexeme lexbuf in
+	let n = String.length s in
+	String.sub s 9 (n - 10) }
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 53d4a020ce..3c73d8f672 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -22,3 +22,5 @@ and skip_comment = parse
 	  skip_comment lexbuf}
   | _  { if Ideutils.is_char_start (Lexing.lexeme lexbuf).[0] then incr length; skip_comment lexbuf}
   | eof  { raise (Lex_error "No closing *)") }
+
+
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 9999e576b9..09b8c408a8 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,4 +1,8 @@
 
+open Preferences
+
+let lib_ide = Filename.concat Coq_config.coqlib "ide"
+  
 let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
 
 let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0
@@ -43,3 +47,29 @@ let try_export file_name s =
     output_string oc s;
     close_out oc
   with e -> prerr_endline (Printexc.to_string e)
+
+let browse url =
+  let l,r = Preferences.current.cmd_browse in
+  ignore (Sys.command (l ^ url ^ r))
+
+let url_for_keyword =
+  let ht = Hashtbl.create 97 in
+  begin try
+    let cin = open_in (Filename.concat lib_ide "index_urls.txt") in
+    try while true do
+      let s = input_line cin in
+      try 
+	let i = String.index s ',' in
+	let k = String.sub s 0 i in
+	let u = String.sub s (i + 1) (String.length s - i - 1) in
+	Hashtbl.add ht k u
+      with _ ->
+	()
+    done with End_of_file ->
+      close_in cin
+  with _ ->
+    ()
+  end;
+  (Hashtbl.find ht : string -> string)
+
+
diff --git a/ide/index_urls.txt b/ide/index_urls.txt
new file mode 100644
index 0000000000..fea61809df
--- /dev/null
+++ b/ide/index_urls.txt
@@ -0,0 +1,563 @@
++,node.0.2.0.html#@default146
+-,node.0.2.1.html#@default247
+2,node.1.2.9.html#@default514
+;,node.1.2.12.html#@default547
+?,node.1.0.6.html#@default358
+?,node.1.2.1.html#@default410
+&,node.0.2.0.html#@default164
+{A}+{B},node.0.2.0.html#@default174
+{x:A & (P x)},node.0.2.0.html#@default163
+{x:A | (P x)},node.0.2.0.html#@default157
+|,node.0.2.0.html#@default158
+A*B,node.0.2.0.html#@default150
+A+{B},node.0.2.0.html#@default178
+A+B,node.0.2.0.html#@default145
+Abort,node.1.1.0.html#@default385
+Absolute names,node.0.1.6.html#@default85
+Abstract,node.1.2.12.html#@default559
+Absurd,node.1.2.3.html#@default442
+Acc,node.0.2.0.html#@default215
+Acc_inv,node.0.2.0.html#@default216
+Acc_rec,node.0.2.0.html#@default217
+Add Abstract Ring,node.3.7.4.html#@default643
+Add Abstract Semi Ring,node.3.7.4.html#@default644
+Add Field,node.1.2.10.html#@default526
+Add LoadPath,node.1.0.4.html#@default338
+Add ML Path,node.1.0.4.html#@default342
+Add Morphism,node.3.8.2.html#@default647
+Add Printing If,node.0.1.1.html#@default67
+Add Printing Let,node.0.1.1.html#@default63
+Add Rec LoadPath,node.1.0.4.html#@default339
+Add Rec ML Path,node.1.0.4.html#@default343
+Add Ring,node.1.2.10.html#@default523
+Add Semi Ring,node.1.2.10.html#@default524
+Add Setoid,node.3.8.1.html#@default646
+All,node.0.2.0.html#@default110
+AllT,node.0.2.0.html#@default224
+Apply,node.1.2.2.html#@default427
+Apply ... with,node.1.2.2.html#@default428
+Arithmetical notations,node.0.2.1.html#@default244
+Arity,node.0.3.4.html#@default288
+Assert,node.1.2.2.html#@default433
+Associativity,node.2.0.1.html#@default571
+Assumption,node.1.2.2.html#@default412
+Auto,node.1.2.10.html#@default515
+AutoRewrite,node.1.2.10.html#@default528
+Axiom,node.0.0.2.html#@default24
+abstractions,node.0.0.1.html#@default16
+absurd,node.0.2.0.html#@default121
+absurd_set,node.0.2.0.html#@default188
+all,node.0.2.0.html#@default109
+allT,node.0.2.0.html#@default223
+and,node.0.2.0.html#@default99
+and_rec,node.0.2.0.html#@default189
+applications,node.0.0.1.html#@default18
+Back,node.1.0.5.html#@default348
+Bad Magic Number,node.1.0.3.html#@default331
+Begin Silent,node.1.0.7.html#@default366
+Binding list,node.1.2.2.html#@default441
+beta-reduction,node.0.3.2.html#@default274
+bool,node.0.2.0.html#@default135
+bool_choice,node.0.2.0.html#@default181
+byte-code,node.3.0.0.html#@default574
+Calculus of (Co)Inductive Constructions,node.0.3.html#@default255
+Canonical Structure,node.0.1.7.html#@default91
+Case,node.1.2.6.html#@default468
+Case ... with,node.1.2.6.html#@default469
+Cases,node.3.2.html#@default593
+Cases...of...end,node.0.0.1.html#@default21
+Cbv,node.1.2.4.html#@default445
+Cd,node.1.0.4.html#@default337
+Change,node.1.2.2.html#@default438
+Change ... in,node.1.2.2.html#@default440
+Chapter,node.0.1.3.html#@default73
+Check,node.1.0.1.html#@default308
+Choice,node.0.2.0.html#@default179
+Choice2,node.0.2.0.html#@default180
+CIC,node.0.3.html#@default254
+Clear,node.1.2.2.html#@default414
+ClearBody,node.1.2.2.html#@default415
+Coercion,node.3.3.5.html#@default601
+Coercion Local,node.3.3.5.html#@default602
+Coercions,node.0.1.8.html#@default92
+and sections,node.3.3.9.html#@default616
+classes,node.3.3.1.html#@default596
+FUNCLASS,node.3.3.2.html#@default597
+identity,node.3.3.3.html#@default599
+inheritance graph,node.3.3.4.html#@default600
+presentation,node.3.3.html#@default595
+SORTCLASS,node.3.3.2.html#@default598
+CoFixpoint,node.0.0.2.html#@default40
+CoInductive,node.0.0.2.html#@default38
+Comments,node.0.0.0.html#@default2
+Compare,node.1.2.8.html#@default489
+Compiled files,node.1.0.3.html#@default327
+Compute,node.1.2.4.html#@default447
+Connectives,node.0.2.0.html#@default94
+Constant,node.0.0.2.html#@default31
+Constructor,node.1.2.5.html#@default455
+Constructor ...  with,node.1.2.5.html#@default456
+Context,node.0.3.1.html#@default263
+Contradiction,node.1.2.3.html#@default443
+Contributions,node.0.2.2.html#@default253
+Conversion rules,node.0.3.2.html#@default273
+Conversion tactics,node.1.2.4.html#@default444
+coqdep,node.3.1.1.html#@default582
+coq_Makefile,node.3.1.2.html#@default584
+coqmktop,node.3.1.0.html#@default579
+coq-tex,node.3.1.3.html#@default586
+coqweb,node.3.1.3.html#@default587
+Correctness,node.3.5.html#@default619
+Cut,node.1.2.2.html#@default434
+CutRewrite,node.1.2.7.html#@default482
+congr_eqT,node.0.2.0.html#@default241
+conj,node.0.2.0.html#@default100
+coqc,node.3.0.html#@default573
+coqtop,node.3.0.html#@default572
+Datatypes,node.0.2.0.html#@default132
+Debugger,node.3.1.0.html#@default580
+Decide Equality,node.1.2.8.html#@default488
+Declarations,node.0.0.2.html#@default23
+Declare ML Module,node.1.0.3.html#@default333
+Decompose,node.1.2.6.html#@default473
+Decompose Record,node.1.2.6.html#@default475
+Decompose Sum,node.1.2.6.html#@default474
+Defined,node.0.0.2.html#@default48
+Definition,node.0.0.2.html#@default33
+Definitions,node.0.0.2.html#@default29
+Dependencies,node.3.1.1.html#@default581
+Dependent Inversion,node.1.2.9.html#@default501
+Dependent Inversion ... with,node.1.2.9.html#@default503
+Dependent Inversion_clear,node.1.2.9.html#@default502
+Dependent Inversion_clear ... with,node.1.2.9.html#@default504
+Dependent Rewrite ->,node.1.2.8.html#@default495
+Dependent Rewrite <-,node.1.2.8.html#@default496
+Derive Dependent Inversion,node.1.2.9.html#@default511
+Derive Dependent Inversion_clear,node.1.2.9.html#@default512
+Derive Inversion,node.1.2.9.html#@default508
+Derive Inversion_clear,node.1.2.9.html#@default509
+Derive Inversion_clear ... with,node.1.2.9.html#@default510
+Destruct,node.1.2.6.html#@default466
+Discriminate,node.1.2.8.html#@default490
+DiscrR,node.0.2.1.html#@default250
+Do,node.1.2.12.html#@default542
+Double Induction,node.1.2.6.html#@default472
+Drop,node.1.0.7.html#@default365
+delta-reduction,node.0.0.2.html#@default30
+EApply,node.1.2.2.html#@default429
+EAuto,node.1.2.10.html#@default517
+Elim ... using,node.1.2.6.html#@default463
+Elim ... with,node.1.2.6.html#@default462
+Singleton elimination,node.0.3.4.html#@default294
+Elimination sorts,node.0.3.4.html#@default291
+ElimType,node.1.2.6.html#@default464
+Emacs,node.3.1.5.html#@default589
+EmptyT,node.0.2.0.html#@default233
+End,node.0.1.3.html#@default74
+End Silent,node.1.0.7.html#@default368
+Environment,node.0.0.2.html#@default32
+Environment variables,node.3.0.3.html#@default577
+Equality,node.0.2.0.html#@default118
+Eval,node.1.0.1.html#@default309
+EX,node.0.2.0.html#@default113
+EXT,node.0.2.0.html#@default229
+Ex,node.0.2.0.html#@default112
+Ex2,node.0.2.0.html#@default116
+Exact,node.1.2.1.html#@default408
+Exc,node.0.2.0.html#@default182
+Except,node.0.2.0.html#@default187
+Exists,node.1.2.5.html#@default458
+Explicitation of implicit arguments,node.0.1.7.html#@default88
+ExT,node.0.2.0.html#@default228
+ExT2,node.0.2.0.html#@default231
+Extensive grammars,node.1.0.6.html#@default362
+Extract Constant,node.3.6.1.html#@default637
+Extract Inductive,node.3.6.1.html#@default638
+Extraction,node.3.6.html#@default623
+Extraction,node.1.0.1.html#@default310
+Extraction Inline,node.3.6.1.html#@default633
+Extraction Language,node.3.6.1.html#@default628
+Extraction Module,node.3.6.0.html#@default626
+Extraction NoInline,node.3.6.1.html#@default634
+eq,node.0.2.0.html#@default119
+eq_add_S,node.0.2.0.html#@default193
+eq_ind_r,node.0.2.0.html#@default126
+eq_rec,node.0.2.0.html#@default186
+eq_rec_r,node.0.2.0.html#@default127
+eq_rect,node.0.2.0.html#@default128
+eq_rect_r,node.0.2.0.html#@default129
+eq_S,node.0.2.0.html#@default190
+eqT,node.0.2.0.html#@default236
+eqT_ind_r,node.0.2.0.html#@default242
+eqT_rec_r,node.0.2.0.html#@default243
+error,node.0.2.0.html#@default184
+ex,node.0.2.0.html#@default111
+ex2,node.0.2.0.html#@default115
+ex_intro,node.0.2.0.html#@default114
+ex_intro2,node.0.2.0.html#@default117
+exist,node.0.2.0.html#@default160
+exist2,node.0.2.0.html#@default162
+existS,node.0.2.0.html#@default166
+existS2,node.0.2.0.html#@default170
+exT,node.0.2.0.html#@default227
+exT2,node.0.2.0.html#@default232
+exT_intro,node.0.2.0.html#@default230
+Fact,node.0.0.2.html#@default44
+Fail,node.1.2.12.html#@default540
+False,node.0.2.0.html#@default97
+False_rec,node.0.2.0.html#@default185
+Field,node.1.2.10.html#@default525
+First,node.1.2.12.html#@default553
+Fix,node.0.3.4.html#@default298
+Fix_F,node.0.2.0.html#@default219
+Fix_F_eq,node.0.2.0.html#@default222
+Fix_F_inv,node.0.2.0.html#@default221
+Fixpoint,node.0.0.2.html#@default39
+Focus,node.1.1.1.html#@default392
+Fold,node.1.2.4.html#@default453
+Fourier,node.1.2.10.html#@default527
+Fst,node.0.2.0.html#@default155
+f_equal,node.0.2.0.html#@default124
+f_equal<I>i</I>,node.0.2.0.html#@default130
+false,node.0.2.0.html#@default137
+fix_eq,node.0.2.0.html#@default220
+fst,node.0.2.0.html#@default153
+Gallina,node.0.0.html#@default0
+gallina,node.3.1.6.html#@default591
+Generalize,node.1.2.2.html#@default436
+Generalize Dependent,node.1.2.2.html#@default437
+Global Variable,node.3.5.2.html#@default620
+Goal,node.0.0.2.html#@default50
+Grammar,node.1.0.6.html#@default361
+ge,node.0.2.0.html#@default208
+gen,node.0.2.0.html#@default226
+goal,node.1.2.html#@default405
+gt,node.0.2.0.html#@default209
+Head normal form,node.0.3.2.html#@default286
+Hint,node.1.2.11.html#@default531
+Hint Rewrite,node.1.2.10.html#@default529
+Hints databases,node.1.2.11.html#@default530
+Hints Immediate,node.1.2.11.html#@default533
+Hints Resolve,node.1.2.11.html#@default532
+Hints Unfold,node.1.2.11.html#@default534
+Hnf,node.1.2.4.html#@default449
+HTML,node.3.1.4.html#@default588
+Hypothesis,node.0.0.2.html#@default28
+I,node.0.2.0.html#@default96
+Identity Coercion,node.3.3.5.html#@default605
+Idtac,node.1.2.12.html#@default538
+IF,node.0.2.0.html#@default107
+proof of,node.3.5.html#@default618
+Implicit Arguments Off,node.1.0.6.html#@default355
+Implicit Arguments On,node.1.0.6.html#@default354
+Implicits,node.1.0.6.html#@default356
+Induction,node.1.2.6.html#@default465
+Inductive,node.0.0.2.html#@default36
+Inductive definitions,node.0.0.2.html#@default35
+Infix,node.1.0.6.html#@default363
+Info,node.1.2.12.html#@default557
+Injection,node.1.2.8.html#@default492
+Inspect,node.1.0.0.html#@default305
+Intro,node.1.2.2.html#@default418
+Intro ... after,node.1.2.2.html#@default426
+Intro after,node.1.2.2.html#@default425
+Intros,node.1.2.2.html#@default422
+Intros pattern,node.1.2.6.html#@default471
+Intros until,node.1.2.2.html#@default423
+Intuition,node.1.2.10.html#@default520
+Inversion,node.1.2.9.html#@default497
+Inversion ... in,node.1.2.9.html#@default499
+Inversion ... using,node.1.2.9.html#@default505
+Inversion ... using ... in,node.1.2.9.html#@default506
+Inversion_clear,node.1.2.9.html#@default498
+Inversion_clear ... in,node.1.2.9.html#@default500
+IsSucc,node.0.2.0.html#@default195
+if ... then ... else,node.0.1.1.html#@default55
+iff,node.0.2.0.html#@default106
+implicit arguments,node.0.1.7.html#@default86
+inl,node.0.2.0.html#@default147
+inleft,node.0.2.0.html#@default176
+inr,node.0.2.0.html#@default148
+inright,node.0.2.0.html#@default177
+iota-reduction,node.0.3.2.html#@default275
+LApply,node.1.2.2.html#@default430
+Lazy,node.1.2.4.html#@default446
+Left,node.1.2.5.html#@default459
+Lemma,node.0.0.2.html#@default42
+LetTac,node.1.2.2.html#@default431
+Lexical conventions,node.0.0.0.html#@default1
+Libraries,node.0.1.5.html#@default82
+Load,node.1.0.2.html#@default325
+Load Verbose,node.1.0.2.html#@default326
+Loadpath,node.1.0.4.html#@default335
+Local,node.0.0.2.html#@default34
+Local definitions,node.0.0.1.html#@default19
+Locate,node.1.0.1.html#@default323
+Locate Library,node.1.0.4.html#@default346
+Logical paths,node.0.1.5.html#@default83
+le,node.0.2.0.html#@default204
+le_n,node.0.2.0.html#@default205
+le_S,node.0.2.0.html#@default206
+left,node.0.2.0.html#@default172
+let ... in,node.0.1.1.html#@default56
+let-in,node.0.0.1.html#@default20
+local context,node.1.1.html#@default372
+lt,node.0.2.0.html#@default207
+Makefile,node.3.1.2.html#@default583
+Man pages,node.3.1.7.html#@default592
+ML-like patterns,node.0.1.1.html#@default54
+Module,node.0.1.4.html#@default75
+Module Type,node.0.1.4.html#@default78
+Move,node.1.2.2.html#@default416
+Mutual Inductive,node.0.0.2.html#@default37
+mult,node.0.2.0.html#@default201
+mult_n_O,node.0.2.0.html#@default202
+mult_n_Sm,node.0.2.0.html#@default203
+NewDestruct,node.1.2.6.html#@default467
+NewInduction,node.1.2.6.html#@default461
+None,node.0.2.0.html#@default143
+Normal form,node.0.3.2.html#@default285
+Notation,node.2.0.0.html#@default569
+Notations for real numbers,node.0.2.1.html#@default249
+n_Sn,node.0.2.0.html#@default197
+nat,node.0.2.0.html#@default138
+nat_case,node.0.2.0.html#@default210
+nat_double_ind,node.0.2.0.html#@default211
+native code,node.3.0.0.html#@default575
+not,node.0.2.0.html#@default98
+not_eq_S,node.0.2.0.html#@default194
+notT,node.0.2.0.html#@default235
+O,node.0.2.0.html#@default139
+O_S,node.0.2.0.html#@default196
+Omega,node.1.2.10.html#@default521
+Opaque,node.1.0.1.html#@default311
+Options of the command line,node.3.0.4.html#@default578
+Orelse,node.1.2.12.html#@default544
+option,node.0.2.0.html#@default141
+or,node.0.2.0.html#@default103
+or_introl,node.0.2.0.html#@default104
+or_intror,node.0.2.0.html#@default105
+Parameter,node.0.0.2.html#@default25
+Pattern,node.1.2.4.html#@default454
+Peano's arithmetic notations,node.0.2.1.html#@default248
+Pose,node.1.2.2.html#@default432
+Positivity,node.0.3.4.html#@default287
+Precedences,node.2.0.1.html#@default570
+Pretty printing,node.1.0.6.html#@default360
+Print,node.1.0.0.html#@default302
+Print All,node.1.0.0.html#@default304
+Print Classes,node.3.3.6.html#@default606
+Print Coercion Paths,node.3.3.6.html#@default609
+Print Coercions,node.3.3.6.html#@default607
+Print Extraction Inline,node.3.6.1.html#@default635
+Print Graph,node.3.3.6.html#@default608
+Print Hint,node.1.2.11.html#@default535
+Print HintDb,node.1.2.11.html#@default536
+Print LoadPath,node.1.0.4.html#@default341
+Print ML Modules,node.1.0.3.html#@default334
+Print ML Path,node.1.0.4.html#@default344
+Print Module,node.0.1.4.html#@default80
+Print Module Type,node.0.1.4.html#@default81
+Print Modules,node.1.0.3.html#@default332
+Print Proof,node.1.0.0.html#@default303
+Print Section,node.1.0.0.html#@default306
+Print Table Printing If,node.0.1.1.html#@default70
+Print Table Printing Let,node.0.1.1.html#@default66
+Programming,node.0.2.0.html#@default131
+Prolog,node.1.2.10.html#@default518
+Prompt,node.1.1.html#@default371
+Proof,node.0.0.2.html#@default45
+Proof editing,node.1.1.html#@default370
+Proof General,node.3.1.5.html#@default590
+Proof term,node.1.1.html#@default373
+Prop,node.0.0.1.html#@default11
+Pwd,node.1.0.4.html#@default336
+pair,node.0.2.0.html#@default152
+plus,node.0.2.0.html#@default198
+plus_n_O,node.0.2.0.html#@default199
+plus_n_Sm,node.0.2.0.html#@default200
+pred,node.0.2.0.html#@default191
+pred_Sn,node.0.2.0.html#@default192
+prod,node.0.2.0.html#@default149
+products,node.0.0.1.html#@default17
+proj1,node.0.2.0.html#@default101
+proj2,node.0.2.0.html#@default102
+projS1,node.0.2.0.html#@default167
+projS2,node.0.2.0.html#@default168
+Qed,node.0.0.2.html#@default47
+Qualified identifiers,node.0.1.6.html#@default84
+Quantifiers,node.0.2.0.html#@default108
+Quit,node.1.0.7.html#@default364
+Quote,node.1.2.9.html#@default513
+?,node.0.1.7.html#@default90
+Read Module,node.1.0.3.html#@default328
+Record,node.0.1.0.html#@default52
+Recursion,node.0.2.0.html#@default213
+Recursive arguments,node.0.3.4.html#@default300
+Recursive Extraction,node.3.6.0.html#@default625
+Recursive Extraction Module,node.3.6.0.html#@default627
+Red,node.1.2.4.html#@default448
+Refine,node.1.2.1.html#@default409
+Reflexivity,node.1.2.7.html#@default484
+Remark,node.0.0.2.html#@default43
+Remove LoadPath,node.1.0.4.html#@default340
+Remove Printing If,node.0.1.1.html#@default68
+Remove Printing Let,node.0.1.1.html#@default64
+Rename,node.1.2.2.html#@default417
+Replace ... with,node.1.2.7.html#@default483
+Require,node.1.0.3.html#@default329
+Require Export,node.1.0.3.html#@default330
+Reset,node.1.0.5.html#@default347
+Reset Extraction Inline,node.3.6.1.html#@default636
+Reset Initial,node.1.0.5.html#@default350
+Resource file,node.3.0.2.html#@default576
+Restart,node.1.1.1.html#@default391
+Restore State,node.1.0.5.html#@default349
+Resume,node.1.1.0.html#@default387
+Rewrite,node.1.2.7.html#@default476
+Rewrite ->,node.1.2.7.html#@default477
+Rewrite -> ... in,node.1.2.7.html#@default480
+Rewrite <-,node.1.2.7.html#@default478
+Rewrite <- ... in,node.1.2.7.html#@default481
+Rewrite ... in,node.1.2.7.html#@default479
+Right,node.1.2.5.html#@default460
+Ring,node.1.2.10.html#@default522
+refl_eqT,node.0.2.0.html#@default237
+refl_equal,node.0.2.0.html#@default120
+right,node.0.2.0.html#@default173
+S,node.0.2.0.html#@default140
+Save,node.0.0.2.html#@default49
+Scheme,node.1.2.13.html#@default561
+Script file,node.1.0.2.html#@default324
+Search,node.1.0.1.html#@default313
+Search ... inside ...,node.1.0.1.html#@default317
+Search ... outside ...,node.1.0.1.html#@default320
+SearchAbout,node.1.0.1.html#@default314
+SearchPattern,node.1.0.1.html#@default315
+SearchPattern ... outside ...,node.1.0.1.html#@default321
+SearchRewrite,node.1.0.1.html#@default316
+SearchRewrite ... inside ...,node.1.0.1.html#@default319
+SearchRewrite ... outside ...,node.1.0.1.html#@default322
+Section,node.0.1.3.html#@default72
+Sections,node.0.1.3.html#@default71
+Set,node.0.0.1.html#@default10
+Set Extraction AutoInline,node.3.6.1.html#@default631
+Set Extraction Optimize,#@default629
+Set Hyps_limit,node.1.1.2.html#@default402
+Set Implicit Arguments,node.0.1.7.html#@default87
+Set Printing Coercion,node.3.3.7.html#@default612
+Set Printing Coercions,node.3.3.7.html#@default610
+Set Printing Synth,node.0.1.1.html#@default60
+Set Printing Wildcard,node.0.1.1.html#@default57
+Set Undo,node.1.1.1.html#@default389
+Setoid_replace,node.3.8.html#@default645
+Setoid_rewrite,node.3.8.3.html#@default649
+Show,node.1.1.2.html#@default394
+Show Conjectures,node.1.1.2.html#@default399
+Show Implicits,node.1.1.2.html#@default395
+Show Intro,node.1.1.2.html#@default400
+Show Intros,node.1.1.2.html#@default401
+Show Programs,node.3.5.2.html#@default621
+Show Proof,node.1.1.2.html#@default398
+Show Script,node.1.1.2.html#@default396
+Show Tree,node.1.1.2.html#@default397
+Silent mode,node.1.0.7.html#@default367
+Simpl,node.1.2.4.html#@default450
+Simple Inversion,node.1.2.9.html#@default507
+Simplify_eq,node.1.2.8.html#@default494
+Small inductive type,node.0.3.4.html#@default292
+Snd,node.0.2.0.html#@default156
+Solve,node.1.2.12.html#@default555
+Some,node.0.2.0.html#@default142
+Sorts,node.0.0.1.html#@default8
+Split,node.1.2.5.html#@default457
+SplitAbsolu,node.0.2.1.html#@default251
+SplitRmult,node.0.2.1.html#@default252
+Strong elimination,node.0.3.4.html#@default293
+Structure,node.3.3.8.html#@default615
+Subst,node.1.2.7.html#@default487
+Substitution,node.0.3.0.html#@default262
+Suspend,node.1.1.0.html#@default386
+Symmetry,node.1.2.7.html#@default485
+Syntactic Definition,node.0.1.7.html#@default89
+Syntax,node.1.0.6.html#@default359
+sig,node.0.2.0.html#@default159
+sig2,node.0.2.0.html#@default161
+sigS,node.0.2.0.html#@default165
+sigS2,node.0.2.0.html#@default169
+snd,node.0.2.0.html#@default154
+sort,node.0.0.1.html#@default7
+specif,node.0.0.1.html#@default14
+subgoal,node.1.2.html#@default406
+sum,node.0.2.0.html#@default144
+sum_eqT,node.0.2.0.html#@default238
+sumbool,node.0.2.0.html#@default171
+sumor,node.0.2.0.html#@default175
+sym_eq,node.0.2.0.html#@default122
+sym_not_eq,node.0.2.0.html#@default125
+sym_not_eqT,node.0.2.0.html#@default239
+Tactic Definition,node.1.2.14.html#@default563
+Tacticals,node.1.2.12.html#@default537
+Do,node.1.2.12.html#@default543
+Fail,node.1.2.12.html#@default541
+First,node.1.2.12.html#@default554
+Solve,node.1.2.12.html#@default556
+Idtac,node.1.2.12.html#@default539
+Info,node.1.2.12.html#@default558
+Orelse,node.1.2.12.html#@default545
+Repeat,node.1.2.12.html#@default546
+Try,node.1.2.12.html#@default552
+Tactics,node.1.2.html#@default404
+Tauto,node.1.2.10.html#@default519
+Terms,node.0.0.1.html#@default5
+Test Printing If,node.0.1.1.html#@default69
+Test Printing Let,node.0.1.1.html#@default65
+Test Printing Synth,node.0.1.1.html#@default62
+Test Printing Wildcard,node.0.1.1.html#@default59
+Theorem,node.0.0.2.html#@default41
+Theories,node.0.2.html#@default93
+Time,node.1.0.7.html#@default369
+Transitivity,node.1.2.7.html#@default486
+Transparent,node.1.0.1.html#@default312
+Trivial,node.1.2.10.html#@default516
+True,node.0.2.0.html#@default95
+Try,node.1.2.12.html#@default551
+Type,node.0.0.1.html#@default9
+Type of constructor,node.0.3.4.html#@default289
+Typing rules,node.0.3.1.html#@default265
+Ax,node.0.3.1.html#@default266
+Cases,node.0.3.4.html#@default296
+Const,node.0.3.1.html#@default268
+Conv,node.0.3.2.html#@default282
+Fix,node.0.3.4.html#@default299
+Lam,node.0.3.1.html#@default270
+Let,node.0.3.1.html#@default272
+Prod,node.0.3.1.html#@default269
+Var,node.0.3.1.html#@default267
+tactic macros,node.1.2.14.html#@default562
+trans_eq,node.0.2.0.html#@default123
+trans_eqT,node.0.2.0.html#@default240
+true,node.0.2.0.html#@default136
+tt,node.0.2.0.html#@default134
+Undo,node.1.1.1.html#@default388
+Unfocus,node.1.1.1.html#@default393
+Unfold,node.1.2.4.html#@default451
+Unfold ... in,node.1.2.4.html#@default452
+UnitT,node.0.2.0.html#@default234
+Unset Extraction AutoInline,node.3.6.1.html#@default632
+Unset Extraction Optimize,#@default630
+Unset Hyps_limit,node.1.1.2.html#@default403
+Unset Implicit Arguments,node.1.0.6.html#@default353
+Unset Printing Coercion,node.3.3.7.html#@default613
+Unset Printing Coercions,node.3.3.7.html#@default611
+Unset Printing Synth,node.0.1.1.html#@default61
+Unset Printing Wildcard,node.0.1.1.html#@default58
+Unset Undo,node.1.1.1.html#@default390
+unit,node.0.2.0.html#@default133
+Variable,node.0.0.2.html#@default26
+Variables,node.0.0.2.html#@default27
+value,node.0.2.0.html#@default183
+Well founded induction,node.0.2.0.html#@default214
+Well foundedness,node.0.2.0.html#@default212
+Write State,node.1.0.5.html#@default351
+well_founded,node.0.2.0.html#@default218
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 2702854e2c..79384ec166 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -1,6 +1,7 @@
 type pref =
     {
       mutable cmd_coqc : string;
+      mutable cmd_make : string;
       mutable cmd_coqmakefile : string;
       mutable cmd_coqdoc : string;
 
@@ -11,21 +12,25 @@ type pref =
       mutable auto_save_delay : float;
       mutable auto_save_name : string*string;
 
-      mutable automatic_tactics : string * string list;
+      mutable automatic_tactics : (string * string) list;
       mutable cmd_print : string;
 
       mutable modifier_for_navigation : Gdk.Tags.modifier list;
       mutable modifier_for_templates : Gdk.Tags.modifier list;
       
+      mutable cmd_browse : string * string;
 
+      mutable doc_url : string;
+      mutable library_url : string;
     }
 
 
 let (current:pref) = 
   {
     cmd_coqc = "coqc";
-    cmd_coqmakefile = "coqmakefile";
-    cmd_coqdoc = "coqdoc";
+    cmd_make = "make";
+    cmd_coqmakefile = "coq_makefile -o Makefile *.v";
+    cmd_coqdoc = "coqdoc -q -g";
     cmd_print = "lpr";
     
 
@@ -40,4 +45,9 @@ let (current:pref) =
     
     modifier_for_navigation = [`CONTROL; `MOD1];
     modifier_for_templates = [`MOD1];
-  }
+    
+    cmd_browse = "netscape -remote \"OpenURL(", ")\"";
+
+    doc_url = "http://coq.inria.fr/doc/";
+    library_url = "http://coq.inria.fr/library/";
+ }