src/Pure/General/url.ML
changeset 21503 c4ea7e8c3937
parent 19305 5c16895d548b
child 21515 43d55165b282
equal deleted inserted replaced
21502:7f3ea2b3bab6 21503:c4ea7e8c3937
    63   Scan.unless (Scan.this_string "file:" ||
    63   Scan.unless (Scan.this_string "file:" ||
    64     Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
    64     Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
    65   Scan.this_string "file:///" |-- scan_path_root >> File ||
    65   Scan.this_string "file:///" |-- scan_path_root >> File ||
    66   Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
    66   Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
    67   Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
    67   Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
       
    68   Scan.this_string "file:/" |-- scan_path_root >> File ||
    68   Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
    69   Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
    69   Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
    70   Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
    70 
    71 
    71 in
    72 in
    72 
    73