<commit_before>(*  Title:      Pure/General/url.ML
    ID:         $Id$
    Author:     <NAME>, TU Muenchen

Basic URLs.
*)

signature URL =
sig
  datatype T =
    File of Path.T |
    RemoteFile of string * Path.T |
    Http of string * Path.T |
    Ftp of string * Path.T
  val append: T -> T -> T
  val pack: T -> string
  val unpack: string -> T
end;

structure Url: URL =
struct

(* type url *)

datatype T =
  File of Path.T |
  RemoteFile of string * Path.T |
  Http of string * Path.T |
  Ftp of string * Path.T;


(* append *)

fun append (File p)            (File p') = File (Path.append p p')
  | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
  | append (Http (h, p))       (File p') = Http (h, Path.append p p')
  | append (Ftp (h, p))        (File p') = Ftp (h, Path.append p p')
  | append _ url = url;


(* pack *)

fun pack_path p = if Path.is_current p then "" else Path.pack p;

fun pack (File p) = pack_path p
  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;


(* unpack *)

local

fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);

val scan_host1 = gen_host Scan.any1;
val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);

val scan_url =
  Scan.unless (Scan.this_string "file:" ||
    Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
  Scan.this_string "file:///" |-- scan_path >> File ||
  Scan.this_string "file://localhost/" |-- scan_path >> File ||
  Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp;

in<commit_msg>Fix file:/// and file://localhost/ to give absolute paths<commit_after>(*  Title:      Pure/General/url.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>

Basic URLs.
*)

signature URL =
sig
  datatype T =
    File of Path.T |
    RemoteFile of string * Path.T |
    Http of string * Path.T |
    Ftp of string * Path.T
  val append: T -> T -> T
  val pack: T -> string
  val unpack: string -> T
end;

structure Url: URL =
struct

(* type url *)

datatype T =
  File of Path.T |
  RemoteFile of string * Path.T |
  Http of string * Path.T |
  Ftp of string * Path.T;


(* append *)

fun append (File p)            (File p') = File (Path.append p p')
  | append (RemoteFile (h, p)) (File p') = RemoteFile (h, Path.append p p')
  | append (Http (h, p))       (File p') = Http (h, Path.append p p')
  | append (Ftp (h, p))        (File p') = Ftp (h, Path.append p p')
  | append _ url = url;


(* pack *)

fun pack_path p = if Path.is_current p then "" else Path.pack p;

fun pack (File p) = pack_path p
  | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
  | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
  | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;


(* unpack *)

local

fun gen_host quant = (quant (not_equal "/" andf Symbol.not_eof) >> implode) --|
  Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);

val scan_host1 = gen_host Scan.any1;
val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o (curry (op^) "/") o implode);

val scan_url =
  Scan.unless (Scan.this_string "file:" ||
    Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
  Scan.this_string "file:///" |-- scan_path_root >> File ||
  Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
  Scan.this_string "file://" |-- scan_host1 -- scan_path >> RemoteFile ||
  Scan.this_string "http://" |-- scan_host1 -- scan_path >> Http ||
  Scan.this_string "ftp://" |-- scan_host1 -- scan_path >> Ftp;

in
{'fraction_non_alphanumeric': 0.1722077922077922, 'fraction_numerical': 0.0025974025974025974, 'mean_word_length': 2.6676190476190476, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 48, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '886629', 'n_tokens_mistral': 1477, 'n_tokens_neox': 1426, 'n_words': 445}