src/Pure/General/url.ML
author aspinall
Fri, 25 Mar 2005 13:03:47 +0100
changeset 15625 43f1669cbae3
parent 15175 b62f7b493360
child 15627 7a108ae4c798
permissions -rw-r--r--
Support non-standard file: URL syntax, temporarily.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/url.ML
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     4
15625
43f1669cbae3 Support non-standard file: URL syntax, temporarily.
aspinall
parents: 15175
diff changeset
     5
Basic URLs.  See RFC 1738.
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     6
*)
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     7
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     8
signature URL =
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
     9
sig
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    10
  datatype T =
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    11
    File of Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    12
    RemoteFile of string * Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    13
    Http of string * Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    14
    Ftp of string * Path.T
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    15
  val append: T -> T -> T
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    16
  val pack: T -> string
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    17
  val unpack: string -> T
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    18
end;
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    19
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    20
structure Url: URL =
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    21
struct
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    22
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    23
(* type url *)
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    24
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    25
datatype T =
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    26
  File of Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    27
  RemoteFile of string * Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    28
  Http of string * Path.T |
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    29
  Ftp of string * Path.T;
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    30
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    31
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    32
(* append *)
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    33
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    34
fun append (File p)            (File p') = File (Path.append p p')
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    35
  | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    36
  | append (Http (h, p))       (File p') = Http (h, Path.append p p')
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    37
  | append (Ftp (h, p))        (File p') = Ftp (h, Path.append p p')
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    38
  | append _ url = url;
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    39
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    40
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    41
(* pack *)
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    42
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    43
fun pack_path p = if Path.is_current p then "" else Path.pack p;
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    44
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    45
fun pack (File p) = pack_path p
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    46
  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    47
  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    48
  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    49
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    50
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    51
(* unpack *)
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    52
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    53
local
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    54
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    55
fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    56
  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    57
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    58
val scan_host1 = gen_host Scan.any1;
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    59
val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
15175
b62f7b493360 Fix file:/// and file://localhost/ to give absolute paths
aspinall
parents: 15174
diff changeset
    60
val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o (curry (op^) "/") o implode);
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    61
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    62
val scan_url =
14909
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    63
  Scan.unless (Scan.this_string "file:" ||
988b4342ed1f tuned representation; added RemoteFile;
wenzelm
parents: 8806
diff changeset
    64
    Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
15175
b62f7b493360 Fix file:/// and file://localhost/ to give absolute paths
aspinall
parents: 15174
diff changeset
    65
  Scan.this_string "file:///" |-- scan_path_root >> File ||
b62f7b493360 Fix file:/// and file://localhost/ to give absolute paths
aspinall
parents: 15174
diff changeset
    66
  Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
15174
fff9c761f89e Fix file:/// and file://localhost/ to return local file result
aspinall
parents: 14981
diff changeset
    67
  Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    68
  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
15625
43f1669cbae3 Support non-standard file: URL syntax, temporarily.
aspinall
parents: 15175
diff changeset
    69
  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp ||
43f1669cbae3 Support non-standard file: URL syntax, temporarily.
aspinall
parents: 15175
diff changeset
    70
  Scan.this_string "file://" |-- scan_host1 -- scan_path >> Ftp (* or other proto *) ||
43f1669cbae3 Support non-standard file: URL syntax, temporarily.
aspinall
parents: 15175
diff changeset
    71
  (* NB: this next one is not in RFC 1738, but produced by some Haskell libraries *)
43f1669cbae3 Support non-standard file: URL syntax, temporarily.
aspinall
parents: 15175
diff changeset
    72
  Scan.this_string "file:" |-- scan_path >> File 
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    73
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    74
in
6639
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    75
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    76
fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    77
d399db16964c Basic URLs.
wenzelm
parents:
diff changeset
    78
end;
14918
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    79
9f30a1238090 improved RemoteFile;
wenzelm
parents: 14909
diff changeset
    80
end;