Remove Whelp commands.

Although these commands were never deprecated, they have been unusable for some
time now, since they send requests to an Italian server which is no longer
alive.

9 files changed, 1 insertions, 334 deletions

diff --git a/_tags b/_tags
index 8cb8b1f90..5c978cabd 100644
--- a/_tags
+++ b/_tags
@@ -24,8 +24,6 @@
 
 ## tags for camlp4 files 
 
-"toplevel/whelp.ml4": use_grammar
-
 "parsing/g_constr.ml4": use_compat5
 "parsing/g_ltac.ml4": use_compat5
 "parsing/g_prim.ml4": use_compat5
@@ -74,4 +72,4 @@
 "tools/coqdoc": include
 "toplevel": include
 
-<plugins/**>: include
\ No newline at end of file
+<plugins/**>: include
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 4547c7fd8..32f94abf7 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -490,87 +490,6 @@ Locate I.Dont.Exist.
 
 \SeeAlso Section \ref{LocateSymbol}
 
-\subsection{The {\sc Whelp} searching tool
-\label{Whelp}}
-
-{\sc Whelp} is an experimental searching and browsing tool for the whole {\Coq}
-library and the whole set of {\Coq} user contributions.  {\sc Whelp} requires a
-browser to work. {\sc Whelp} has been developed at the University of Bologna as
-part of the HELM\footnote{Hypertextual Electronic Library of Mathematics} and
-MoWGLI\footnote{Mathematics on the Web, Get it by Logics and Interfaces}
-projects.  It can be invoked directly from the {\Coq} toplevel or from
-{\CoqIDE}, assuming a graphical environment is also running. The browser to use
-can be selected by setting the environment variable {\tt COQREMOTEBROWSER}. If
-not explicitly set, it defaults to
-\verb!firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"!  or
-\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the underlying
-operating system (in the command, the string \verb!%s!  serves as metavariable
-for the url to open).  The Whelp tool relies on a dedicated Whelp server and on
-another server called Getter that retrieves formal documents. The default Whelp
-server name can be obtained using the command {\tt Test Whelp Server} and the
-default Getter can be obtained using the command: {\tt Test Whelp Getter}. The
-Whelp server name can be changed using the command:
-
-\smallskip
-\noindent {\tt Set Whelp Server {\str}}.\\
-where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}).
-\optindex{Whelp Server}
-\smallskip
-
-\noindent The Getter can be changed using the command:
-\smallskip
-
-\noindent {\tt Set Whelp Getter {\str}}.\\
-where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58081}).  
-\optindex{Whelp Getter}
-
-\bigskip
-
-The {\sc Whelp} commands are:
-
-\subsubsection{\tt Whelp Locate "{\sl reg\_expr}".
-\comindex{Whelp Locate}}
-
-This command opens a browser window and displays the result of seeking
-for all names that match the regular expression {\sl reg\_expr} in the
-{\Coq} library and user contributions. The regular expression can
-contain the special operators are * and ? that respectively stand for
-an arbitrary substring and for exactly one character.
-
-\variant {\tt Whelp Locate {\ident}.}\\
-This is equivalent to {\tt Whelp Locate "{\ident}"}.
-
-\subsubsection{\tt Whelp Match {\pattern}.
-\comindex{Whelp Match}}
-
-This command opens a browser window and displays the result of seeking
-for all statements that match the pattern {\pattern}. Holes in the
-pattern are represented by the wildcard character ``\_''.
-
-\subsubsection[\tt Whelp Instance {\pattern}.]{\tt Whelp Instance {\pattern}.\comindex{Whelp Instance}}
-
-This command opens a browser window and displays the result of seeking
-for all statements that are instances of the pattern {\pattern}. The
-pattern is here assumed to be an universally quantified expression.
-
-\subsubsection[\tt Whelp Elim {\qualid}.]{\tt Whelp Elim {\qualid}.\comindex{Whelp Elim}}
-
-This command opens a browser window and displays the result of seeking
-for all statements that have the ``form'' of an elimination scheme
-over the type denoted by {\qualid}.
-
-\subsubsection[\tt Whelp Hint {\term}.]{\tt Whelp Hint {\term}.\comindex{Whelp Hint}}
-
-This command opens a browser window and displays the result of seeking
-for all statements that can be instantiated so that to prove the
-statement {\term}.
-
-\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint
-{\sl goal}} where {\sl goal} is the current goal to prove. Notice that
-{\Coq} does not send the local environment of definitions to the {\sc
-Whelp} tool so that it only works on requests strictly based on, only,
-definitions of the standard library and user contributions.
-
 \section{Loading files}
 
 \Coq\ offers the possibility of loading different
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
index 6f474eb12..47612cdf7 100644
--- a/ide/MacOS/default_accel_map
+++ b/ide/MacOS/default_accel_map
@@ -247,7 +247,6 @@
 ; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "")
-; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "")
 (gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic right" "")
 ; (gtk_accel_path "<Actions>/Edit/Find Previous" "<Shift>F3")
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 995c45c5a..37e38a546 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -228,8 +228,6 @@ let state_preserving = [
   "Test Printing Synth";
   "Test Printing Wildcard";
 
-  "Whelp Hint";
-  "Whelp Locate";
 ]
 
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index cb05363dd..4564d620e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1171,7 +1171,6 @@ let build_ui () =
     qitem "About" (Some "<Ctrl><Shift>A");
     qitem "Locate" (Some "<Ctrl><Shift>L");
     qitem "Print Assumptions" (Some "<Ctrl><Shift>N");
-    qitem "Whelp Locate" None;
   ];
 
   menu tools_menu [
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index af71b1e78..edfe28b26 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -119,7 +119,6 @@ let init () =
     <menuitem action='About' />
     <menuitem action='Locate' />
     <menuitem action='Print Assumptions' />
-    <menuitem action='Whelp Locate' />
   </menu>
   <menu name='Tools' action='Tools'>
     <menuitem action='Comment' />
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index d22524e5c..bf0f305ab 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -13,7 +13,6 @@ Record
 Vernacinterp
 Mltop
 Vernacentries
-Whelp
 Vernac
 Usage
 Coqloop
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
deleted file mode 100644
index daedc30f4..000000000
--- a/toplevel/whelp.ml4
+++ /dev/null
@@ -1,224 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Flags
-open Pp
-open Errors
-open Names
-open Term
-open Glob_term
-open Libnames
-open Globnames
-open Nametab
-open Detyping
-open Constrintern
-open Dischargedhypsmap
-open Pfedit
-open Tacmach
-open Misctypes
-
-(* Coq interface to the Whelp query engine developed at
-   the University of Bologna *)
-
-let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080"
-let getter_server_name = ref "http://mowgli.cs.unibo.it:58081"
-
-open Goptions
-
-let _ =
-  declare_string_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "Whelp server";
-      optkey   = ["Whelp";"Server"];
-      optread  = (fun () -> !whelp_server_name);
-      optwrite = (fun s -> whelp_server_name := s) }
-
-let _ =
-  declare_string_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "Whelp getter";
-      optkey   = ["Whelp";"Getter"];
-      optread  = (fun () -> !getter_server_name);
-      optwrite = (fun s -> getter_server_name := s) }
-
-
-let make_whelp_request req c =
-  !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
-
-let b = Buffer.create 16
-
-let url_char c =
-  if 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' ||
-     '0' <= c && c <= '9' || c ='.'
-  then Buffer.add_char b c
-  else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c))
-
-let url_string s = String.iter url_char s
-
-let rec url_list_with_sep sep f = function
-  | [] -> ()
-  | [a] -> f a
-  | a::l -> f a; url_string sep; url_list_with_sep sep f l
-
-let url_id id = url_string (Id.to_string id)
-
-let uri_of_dirpath dir =
-  url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir)
-
-let error_whelp_unknown_reference ref =
-  let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
-  errorlabstrm ""
-    (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++
-     strbrk ", are not supported in Whelp.")
-
-let uri_of_repr_kn ref (mp,dir,l) =
-  match mp with
-    | MPfile sl ->
-        uri_of_dirpath (Label.to_id l :: DirPath.repr dir @ DirPath.repr sl)
-    | _ ->
-        error_whelp_unknown_reference ref
-
-let url_paren f l = url_char '('; f l; url_char ')'
-let url_bracket f l = url_char '['; f l; url_char ']'
-
-let whelp_of_glob_sort = function
-  | GProp -> "Prop"
-  | GSet -> "Set"
-  | GType _ -> "Type"
-
-let uri_int n = Buffer.add_string b (string_of_int n)
-
-let uri_of_ind_pointer l =
-  url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l
-
-let uri_of_global ref =
-  match ref with
-  | VarRef id -> error ("Unknown Whelp reference: "^(Id.to_string id)^".")
-  | ConstRef cst ->
-      uri_of_repr_kn ref (repr_con cst); url_string ".con"
-  | IndRef (kn,i) ->
-      uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1]
-  | ConstructRef ((kn,i),j) ->
-      uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j]
-
-let whelm_special = Id.of_string "WHELM_ANON_VAR"
-
-let url_of_name = function
-  | Name id -> url_id id
-  | Anonymous -> url_id whelm_special (* No anon id in Whelp *)
-
-let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c
-
-let uri_params f = function
-  | [] -> ()
-  | l -> url_string "\\subst";
-         url_bracket (url_list_with_sep ";" (uri_of_binding f)) l
-
-let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
-
-let section_parameters = function
-  | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) ->
-      get_discharged_hyp_names (path_of_global (IndRef(induri,0)))
-  | GRef (_,(ConstRef cst as ref),_) ->
-      get_discharged_hyp_names (path_of_global ref)
-  | _ -> []
-
-let merge vl al =
-  let rec aux acc = function
-  | ([],l) | (_,([] as l)) -> List.rev acc, l
-  | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al)
-  in aux [] (vl,al)
-
-let rec uri_of_constr c =
-  match c with
-  | GVar (_,id) -> url_id id
-  | GRef (_,ref,_) ->  uri_of_global ref
-  | GHole _ | GEvar _ -> url_string "?"
-  | GSort (_,s) -> url_string (whelp_of_glob_sort s)
-  | GApp (_,f,args) ->
-      let inst,rest = merge (section_parameters f) args in
-      uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
-      url_list_with_sep " " uri_of_constr rest
-  | GLambda (_,na,k,ty,c) ->
-      url_string "\\lambda "; url_of_name na; url_string ":";
-      uri_of_constr ty; url_string "."; uri_of_constr c
-  | GProd (_,Anonymous,k,ty,c) ->
-      uri_of_constr ty; url_string "\\to "; uri_of_constr c
-  | GProd (_,Name id,k,ty,c) ->
-      url_string "\\forall "; url_id id; url_string ":";
-      uri_of_constr ty; url_string "."; uri_of_constr c
-  | GLetIn (_,na,b,c) ->
-      url_string "let "; url_of_name na; url_string "\\def ";
-      uri_of_constr b; url_string " in "; uri_of_constr c
-  | GCast (_,c, (CastConv t|CastVM t|CastNative t)) ->
-      uri_of_constr c; url_string ":"; uri_of_constr t
-  | GRec _ | GIf _ | GLetTuple _ | GCases _ ->
-      error "Whelp does not support pattern-matching and (co-)fixpoint."
-  | GCast (_,_, CastCoerce) ->
-      anomaly (Pp.str "Written w/o parenthesis")
-  | GPatVar _ ->
-      anomaly (Pp.str "Found constructors not supported in constr")
-
-let make_string f x = Buffer.reset b; f x; Buffer.contents b
-
-let send_whelp req s =
-  let url = make_whelp_request req s in
-  let command = Util.subst_command_placeholder browser_cmd_fmt url in
-  let _ = CUnix.run_command ~hook:print_string command in ()
-
-let whelp_constr env sigma req c =
-  let c = detype false [whelm_special] env sigma c in
-  send_whelp req (make_string uri_of_constr c)
-
-let whelp_constr_expr req c =
-  let (sigma,env)= Lemmas.get_current_context () in
-  let _,c = interp_open_constr env sigma c in
-  whelp_constr env sigma req c
-
-let whelp_locate s =
-  send_whelp "locate" s
-
-let whelp_elim ind =
-  send_whelp "elim" (make_string uri_of_global (IndRef ind))
-
-let on_goal f =
-  let gls = Proof.V82.subgoals (get_pftreestate ()) in
-  let gls = { gls with Evd.it = List.hd gls.Evd.it }  in
-  f (pf_env gls) (project gls) (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
-
-type whelp_request =
-  | Locate of string
-  | Elim of inductive
-  | Constr of string * constr
-
-let whelp = function
-  | Locate s -> whelp_locate s
-  | Elim ind -> whelp_elim ind
-  | Constr (s,c) -> whelp_constr (Global.env()) (Evd.empty) s c
-
-VERNAC ARGUMENT EXTEND whelp_constr_request
-| [ "Match" ] -> [ "match" ]
-| [ "Instance" ] -> [ "instance" ]
-END
-
-VERNAC COMMAND EXTEND Whelp CLASSIFIED AS QUERY
-| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ]
-| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ]
-| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ]
-| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
-END
-
-VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY
-| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ]
-| [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] ->
-  [ on_goal (fun env sigma -> whelp_constr env sigma "hint") ]
-END
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
deleted file mode 100644
index 62272c50f..000000000
--- a/toplevel/whelp.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Coq interface to the Whelp query engine developed at
-   the University of Bologna *)
-
-open Names
-open Term
-
-type whelp_request =
-  | Locate of string
-  | Elim of inductive
-  | Constr of string * constr
-
-val whelp : whelp_request -> unit