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