src/Pure/General/path.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 44863 49ea566cb3b4
child 45666 d83797ef0d2d
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     1 (*  Title:      Pure/General/path.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Algebra of file-system paths: basic POSIX notation, extended by named
     5 roots (e.g. //foo) and variables (e.g. $BAR).
     6 *)
     7 
     8 signature PATH =
     9 sig
    10   eqtype T
    11   val is_current: T -> bool
    12   val current: T
    13   val root: T
    14   val named_root: string -> T
    15   val parent: T
    16   val basic: string -> T
    17   val variable: string -> T
    18   val is_absolute: T -> bool
    19   val is_basic: T -> bool
    20   val append: T -> T -> T
    21   val appends: T list -> T
    22   val make: string list -> T
    23   val implode: T -> string
    24   val explode: string -> T
    25   val pretty: T -> Pretty.T
    26   val print: T -> string
    27   val dir: T -> T
    28   val base: T -> T
    29   val ext: string -> T -> T
    30   val split_ext: T -> T * string
    31   val expand: T -> T
    32   val position: T -> Position.T
    33 end;
    34 
    35 structure Path: PATH =
    36 struct
    37 
    38 (* path elements *)
    39 
    40 datatype elem =
    41   Root of string |
    42   Basic of string |
    43   Variable of string |
    44   Parent;
    45 
    46 local
    47 
    48 fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
    49 
    50 fun check_elem (chs as []) = err_elem "Illegal" chs
    51   | check_elem (chs as ["~"]) = err_elem "Illegal" chs
    52   | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
    53   | check_elem chs =
    54       (case inter (op =) ["/", "\\", ":"] chs of
    55         [] => chs
    56       | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
    57 
    58 in
    59 
    60 val root_elem = Root o implode o check_elem;
    61 val basic_elem = Basic o implode o check_elem;
    62 val variable_elem = Variable o implode o check_elem;
    63 
    64 end;
    65 
    66 
    67 (* type path *)
    68 
    69 datatype T = Path of elem list;    (*reversed elements*)
    70 
    71 fun rep (Path xs) = xs;
    72 
    73 fun is_current (Path []) = true
    74   | is_current _ = false;
    75 
    76 val current = Path [];
    77 val root = Path [Root ""];
    78 fun named_root s = Path [root_elem (raw_explode s)];
    79 fun basic s = Path [basic_elem (raw_explode s)];
    80 fun variable s = Path [variable_elem (raw_explode s)];
    81 val parent = Path [Parent];
    82 
    83 fun is_absolute (Path xs) =
    84   (case try List.last xs of
    85     SOME (Root _) => true
    86   | _ => false);
    87 
    88 fun is_basic (Path [Basic _]) = true
    89   | is_basic _ = false;
    90 
    91 
    92 (* append and norm *)
    93 
    94 fun apply (y as Root _) _ = [y]
    95   | apply Parent (xs as (Root _ :: _)) = xs
    96   | apply Parent (Basic _ :: rest) = rest
    97   | apply y xs = y :: xs;
    98 
    99 fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs);
   100 fun appends paths = Library.foldl (uncurry append) (current, paths);
   101 val make = appends o map basic;
   102 
   103 fun norm elems = fold_rev apply elems [];
   104 
   105 
   106 (* implode *)
   107 
   108 local
   109 
   110 fun implode_elem (Root "") = ""
   111   | implode_elem (Root s) = "//" ^ s
   112   | implode_elem (Basic s) = s
   113   | implode_elem (Variable s) = "$" ^ s
   114   | implode_elem Parent = "..";
   115 
   116 in
   117 
   118 fun implode_path (Path []) = "."
   119   | implode_path (Path [Root ""]) = "/"
   120   | implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs));
   121 
   122 end;
   123 
   124 
   125 (* explode *)
   126 
   127 local
   128 
   129 fun explode_elem ".." = Parent
   130   | explode_elem "~" = Variable "HOME"
   131   | explode_elem "~~" = Variable "ISABELLE_HOME"
   132   | explode_elem s =
   133       (case raw_explode s of
   134         "$" :: cs => variable_elem cs
   135       | cs => basic_elem cs);
   136 
   137 val explode_elems =
   138   rev o map explode_elem o filter_out (fn c => c = "" orelse c = ".");
   139 
   140 in
   141 
   142 fun explode_path str =
   143   let val (roots, raw_elems) =
   144     (case take_prefix (equal "") (space_explode "/" str) |>> length of
   145       (0, es) => ([], es)
   146     | (1, es) => ([Root ""], es)
   147     | (_, []) => ([Root ""], [])
   148     | (_, e :: es) => ([root_elem (raw_explode e)], es))
   149   in Path (norm (explode_elems raw_elems @ roots)) end;
   150 
   151 end;
   152 
   153 
   154 (* print *)
   155 
   156 fun pretty path =
   157   let val s = implode_path path
   158   in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
   159 
   160 val print = Pretty.str_of o pretty;
   161 
   162 
   163 (* base element *)
   164 
   165 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
   166   | split_path _ path = error ("Cannot split path into dir/base: " ^ print path);
   167 
   168 val dir = split_path #1;
   169 val base = split_path (fn (_, s) => Path [Basic s]);
   170 
   171 fun ext "" = I
   172   | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
   173 
   174 val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
   175   (case take_suffix (fn c => c <> ".") (raw_explode s) of
   176     ([], _) => (Path [Basic s], "")
   177   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
   178 
   179 
   180 (* expand variables *)
   181 
   182 fun eval (Variable s) = rep (explode_path (getenv_strict s))
   183   | eval x = [x];
   184 
   185 val expand = rep #> maps eval #> norm #> Path;
   186 
   187 
   188 (* source position -- with smart replacement ISABELLE_HOME *)
   189 
   190 val isabelle_home = explode_path "~~";
   191 
   192 fun position path =
   193   let
   194     val s = implode_path path;
   195     val prfx = implode_path (expand isabelle_home) ^ "/";
   196   in
   197     Position.file
   198       (case try (unprefix prfx) s of
   199         NONE => s
   200       | SOME s' => "~~/" ^ s')
   201   end;
   202 
   203 
   204 (*final declarations of this structure!*)
   205 val implode = implode_path;
   206 val explode = explode_path;
   207 
   208 end;
   209