Utilisation du module Buffer; encodage plus rigoureux des symboles en uri

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

1 files changed, 61 insertions, 55 deletions

diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index bc735f8d1..dfda56623 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -31,8 +31,25 @@ open Detyping
 let make_whelp_request req c =
   "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty&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' or 'a' <= c & c <= 'z' or 
+     '0' <= c & c <= '9' or 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 (string_of_id id)
+
 let uri_of_dirpath dir =
-  "cic:/" ^ String.concat "/" (List.map Names.string_of_id (List.rev 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 Idset.empty ref in
@@ -45,56 +62,41 @@ let uri_of_repr_kn ref (mp,dir,l) =
     | _ ->
         error_whelp_unknown_reference ref
 
-let url_encode_product = "%5Cforall+" (* \forall *)
-let url_encode_imply  = "%5Cto+"      (* \to *)
-let url_encode_lambda  = "%5Clambda+" (* \lambda *)
-let url_encode_let = "let+"           (* let *)
-let url_encode_def = "%5Cdef+"        (* \def *)
-let url_encode_in = "+in+"            (* in *)
-let url_encode_colon = "%3A"          (* : *)
-let url_encode_dot = "."              (* . *)
-let url_encode_semicolon = "%3B"      (* ; *)
-let uri_encode_question_mark = "%3F"  (* ? *)
-let url_encode_lpar = "%28"           (* ( *)
-let url_encode_rpar = "%29"           (* ) *)
-let url_encode_slash = "%2F"          (* / *)
-let url_encode_subst = "%5Csubst"     (* \subst *)
-let url_encode_assign = "%5CAssign"   (* \Assign *)
-let url_encode_ind_pointer = ".ind%23xpointer" (* .ind#xpointer *)
-let url_paren s = url_encode_lpar ^ s ^ url_encode_rpar
-let url_bracket s = "%5B" ^ s ^ "%5D"
-
-let uri_of_sort = function
+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_rawsort = function
   | RProp Null -> "Prop"
   | RProp Pos -> "Set"
   | RType _ -> "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: "^(string_of_id id)
+  | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id))
   | ConstRef cst ->
-      uri_of_repr_kn ref (repr_con cst)
-      ^".con"
+      uri_of_repr_kn ref (repr_con cst); url_string ".con"
   | IndRef (kn,i) -> 
-      uri_of_repr_kn ref (repr_kn kn) ^ url_encode_ind_pointer ^
-      url_paren ("1" ^ url_encode_slash ^ string_of_int (i+1))
+      uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1]
   | ConstructRef ((kn,i),j) ->
-      uri_of_repr_kn ref (repr_kn kn) ^ url_encode_ind_pointer ^
-      url_paren ("1" ^ url_encode_slash ^ string_of_int (i+1)
-                     ^ url_encode_slash ^ string_of_int j)
+      uri_of_repr_kn ref (repr_kn 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 -> string_of_id id
-  | Anonymous -> string_of_id whelm_special (* No anon id in Whelp *)
+  | Name id -> url_id id
+  | Anonymous -> url_id whelm_special (* No anon id in Whelp *)
 
-let uri_of_binding (id,c) = string_of_id id ^ url_encode_assign ^ c
+let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c
 
-let uri_params = function
-  | [] -> ""
-  | l -> url_encode_subst ^ url_bracket 
-      (String.concat url_encode_semicolon (List.map uri_of_binding l))
+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)
 
@@ -111,33 +113,35 @@ let merge vl al =
   | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al)
   in aux [] (vl,al)
 
-let rec uri_of_constr = function
-  | RVar (_,id) -> string_of_id id
-  | RRef (_,ref) -> (uri_of_global ref)
+let rec uri_of_constr c =
+  url_paren (fun () -> match c with
+  | RVar (_,id) -> url_id id
+  | RRef (_,ref) ->  uri_of_global ref
   | RApp (_,f,args) ->
-      let args = List.map uri_of_constr args in
       let inst,rest = merge (section_parameters f) args in
-      url_paren (uri_of_constr f ^ "+" ^ uri_params inst ^ 
-        String.concat "+" rest)
+      uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; 
+      url_list_with_sep " " uri_of_constr rest
   | RLambda (_,na,ty,c) ->
-      url_paren (url_encode_lambda ^ url_of_name na ^ url_encode_colon
-        ^ uri_of_constr ty ^ url_encode_dot ^ uri_of_constr c)
+      url_string "\\lambda "; url_of_name na; url_string ":";
+      uri_of_constr ty; url_string "."; uri_of_constr c
   | RProd (_,Anonymous,ty,c) ->
-      url_paren (uri_of_constr ty ^ url_encode_imply ^ uri_of_constr c)
+      uri_of_constr ty; url_string "\\to "; uri_of_constr c
   | RProd (_,Name id,ty,c) ->
-      url_paren (url_encode_product ^ string_of_id id ^ url_encode_colon
-        ^ uri_of_constr ty ^ url_encode_dot ^ uri_of_constr c)
+      url_string "\\forall "; url_id id; url_string ":";
+      uri_of_constr ty; url_string "."; uri_of_constr c
   | RLetIn (_,na,b,c) ->
-      url_paren (url_encode_let ^ url_of_name na ^ url_encode_def ^ 
-      uri_of_constr b ^ url_encode_in ^ uri_of_constr c)
+      url_string "let "; url_of_name na; url_string "\\def ";
+      uri_of_constr b; url_string " in "; uri_of_constr c
   | RCast (_,c,t) ->
-      url_paren (uri_of_constr c ^ url_encode_colon ^ uri_of_constr t)
-  | RHole _ | REvar _ -> uri_encode_question_mark
-  | RSort (_,s) -> uri_of_sort s
+      uri_of_constr c; url_string ":"; uri_of_constr t
+  | RHole _ | REvar _ -> url_string "?"
+  | RSort (_,s) -> url_string (whelp_of_rawsort s)
   | RRec _ | RIf _ | RLetTuple _ | ROrderedCase _ | RCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint"
   | RPatVar _ | RDynamic _ -> 
-      anomaly "Found constructors not supported in constr"
+      anomaly "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
@@ -146,7 +150,7 @@ let send_whelp req s =
 
 let whelp_constr env req c =
   let c = detype (false,env) [whelm_special] [] c in
-  send_whelp req (uri_of_constr c)
+  send_whelp req (make_string uri_of_constr c)
 
 let whelp_constr_expr req c =
   let (sigma,env)= get_current_context () in
@@ -156,7 +160,8 @@ let whelp_constr_expr req c =
 let whelp_locate s =
   send_whelp "locate" s
 
-let whelp_elim ind = send_whelp "elim" (uri_of_global (IndRef ind))
+let whelp_elim ind = 
+  send_whelp "elim" (make_string uri_of_global (IndRef ind))
 
 let locate_inductive r =
   let (loc,qid) = qualid_of_reference r in
@@ -183,6 +188,7 @@ END
 
 VERNAC COMMAND EXTEND Whelp
 | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] 
+| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] 
 | [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ] 
 | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
 END