summaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
commite4282ea99c664d8d58067bee199cbbcf881b60d5 (patch)
treed4c4a873eb055c728666f367469fa26c3417793a /ide
parenta0a94c1340a63cdb824507b973393882666ba52a (diff)
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml4
-rw-r--r--ide/coqide.ml8
-rw-r--r--ide/preferences.ml6
3 files changed, 10 insertions, 8 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index e2649c82..a44428c7 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq.ml 11826 2009-01-22 06:43:35Z notin $ *)
+(* $Id: coq.ml 11948 2009-02-27 16:01:53Z glondu $ *)
open Vernac
open Vernacexpr
@@ -424,6 +424,8 @@ let interp_with_options verbosely options s =
prerr_endline s;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
+ (* Temporary hack to make coqide.byte work (WTF???) *)
+ Pervasives.prerr_endline "";
match pe with
| None -> assert false
| Some((loc,vernac) as last) ->
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ea2dfe4d..cc147d5e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 11853 2009-01-23 18:40:58Z notin $ *)
+(* $Id: coqide.ml 12104 2009-04-24 18:10:10Z notin $ *)
open Preferences
open Vernacexpr
@@ -3237,7 +3237,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
~callback:
(fun () ->
let av = Option.get ((get_current_view ()).analyzed_view) in
- browse av#insert_message (!current.doc_url ^ "main.html")) in
+ browse av#insert_message (!current.doc_url)) in
let _ = help_factory#add_item "Browse Coq _Library"
~callback:
(fun () ->
@@ -3518,8 +3518,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let about_full_string =
"\nCoq is developed by the Coq Development Team\
\n(INRIA - CNRS - University Paris 11 and partners)\
- \nWeb site: http://coq.inria.fr\
- \nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
+ \nWeb site: " ^ Coq_config.wwwcoq ^
+ "\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
\n\
\nCredits for CoqIDE, the Integrated Development Environment for Coq:\
\n\
diff --git a/ide/preferences.ml b/ide/preferences.ml
index dba56a77..ffb346d9 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: preferences.ml 11276 2008-07-28 00:28:34Z glondu $ *)
+(* $Id: preferences.ml 12104 2009-04-24 18:10:10Z notin $ *)
open Configwin
open Printf
@@ -135,8 +135,8 @@ let (current:pref ref) =
(* text_font = Pango.Font.from_string "sans 12";*)
text_font = Pango.Font.from_string "Monospace 10";
- doc_url = "http://coq.inria.fr/doc/";
- library_url = "http://coq.inria.fr/library/";
+ doc_url = Coq_config.wwwrefman;
+ library_url = Coq_config.wwwstdlib;
show_toolbar = true;
contextual_menus_on_goal = true;