Initial revision

[helm.git] / helm / interface / pxpUriResolver.ml

diff --git a/helm/interface/pxpUriResolver.ml b/helm/interface/pxpUriResolver.ml
new file mode 100644 (file)
index 0000000..b5b37f3
--- /dev/null
+++ b/helm/interface/pxpUriResolver.ml
@@ -0,0 +1,101 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 11/10/2000                                 *)
+(*                                                                            *)
+(*                                                                            *)
+(******************************************************************************)
+
+let resolve =
+ function
+    "http://localhost:8081/getdtd?url=cic.dtd" ->
+     "/home/pauillac/coq3/sacerdot/HELM/INTERFACE/examples/dtd/cic.dtd"
+  | "http://localhost:8081/getdtd?url=maththeory.dtd" ->
+     "/home/pauillac/coq3/sacerdot/HELM/INTERFACE/examples/dtd/maththeory.dtd"
+  | "http://localhost:8081/getdtd?url=annotations.dtd" ->
+     "/home/pauillac/coq3/sacerdot/HELM/INTERFACE/examples/dtd/annotations.dtd"
+  | s  -> s
+;;
+
+let url_syntax =
+    let enable_if =
+      function
+         `Not_recognized  -> Neturl.Url_part_not_recognized
+       | `Allowed         -> Neturl.Url_part_allowed
+       | `Required        -> Neturl.Url_part_required
+    in
+    { Neturl.null_url_syntax with
+       Neturl.url_enable_scheme = enable_if `Allowed;
+       Neturl.url_enable_host   = enable_if `Allowed;
+       Neturl.url_enable_path   = Neturl.Url_part_required;
+       Neturl.url_accepts_8bits = true;
+    } 
+;;
+
+let file_url_of_id xid =
+  let file_url_of_sysname sysname =
+    (* By convention, we can assume that sysname is a URL conforming
+     * to RFC 1738 with the exception that it may contain non-ASCII
+     * UTF-8 characters. 
+     *)
+    try
+     Neturl.url_of_string url_syntax sysname 
+        (* may raise Malformed_URL *)
+    with
+     Neturl.Malformed_URL -> raise Pxp_reader.Not_competent
+  in
+  let url =
+    match xid with
+       Pxp_types.Anonymous          -> raise Pxp_reader.Not_competent
+     | Pxp_types.Public (_,sysname) ->
+        let sysname = resolve sysname in
+         if sysname <> "" then file_url_of_sysname sysname
+                          else raise Pxp_reader.Not_competent
+     | Pxp_types.System sysname     ->
+        let sysname = resolve sysname in
+         file_url_of_sysname sysname
+  in
+  let scheme =
+    try Neturl.url_scheme url with Not_found -> "file" in
+  let host =
+    try Neturl.url_host url with Not_found -> "" in
+    
+  if scheme <> "file" then raise Pxp_reader.Not_competent;
+  if host <> "" && host <> "localhost" then raise Pxp_reader.Not_competent;
+    
+  url
+;;
+
+let from_file ?system_encoding utf8_filename =
+  
+  let r =
+    new Pxp_reader.resolve_as_file 
+      ?system_encoding:system_encoding
+      ~url_of_id:file_url_of_id
+      ()
+  in
+
+  let utf8_abs_filename =
+    if utf8_filename <> "" && utf8_filename.[0] = '/' then
+      utf8_filename
+    else
+      Sys.getcwd() ^ "/" ^ utf8_filename
+  in
+
+  let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in
+  let url = Neturl.make_url 
+             ~scheme:"file" 
+             ~host:"localhost" 
+             ~path:(Neturl.split_path utf8_abs_filename) 
+             syntax
+  in
+
+  let xid = Pxp_types.System (Neturl.string_of_url url) in
+    
+
+  Pxp_yacc.ExtID(xid, r)
+;;
+
+