src/Pure/General/path.ML
author wenzelm
Fri, 03 Aug 2012 13:06:25 +0200
changeset 48658 4c7932270d6d
parent 48420 a8ed41b6280b
child 48866 034df7b05759
permissions -rw-r--r--
reject path variable nesting explicitly;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 5011
diff changeset
     1
(*  Title:      Pure/General/path.ML
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
     3
43601
fd650d659275 tuned comments;
wenzelm
parents: 43599
diff changeset
     4
Algebra of file-system paths: basic POSIX notation, extended by named
fd650d659275 tuned comments;
wenzelm
parents: 43599
diff changeset
     5
roots (e.g. //foo) and variables (e.g. $BAR).
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
     6
*)
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
     7
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
     8
signature PATH =
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
     9
sig
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    10
  eqtype T
6460
cb8c85435228 added is_current;
wenzelm
parents: 6319
diff changeset
    11
  val is_current: T -> bool
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    12
  val current: T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    13
  val root: T
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    14
  val named_root: string -> T
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    15
  val parent: T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    16
  val basic: string -> T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    17
  val variable: string -> T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    18
  val is_absolute: T -> bool
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    19
  val is_basic: T -> bool
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    20
  val append: T -> T -> T
6270
c905fe5994a2 val appends: T list -> T;
wenzelm
parents: 6223
diff changeset
    21
  val appends: T list -> T
6319
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
    22
  val make: string list -> T
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
    23
  val implode: T -> string
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
    24
  val explode: string -> T
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
    25
  val pretty: T -> Pretty.T
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
    26
  val print: T -> string
14912
88b9d9165452 added split_ext; removed drop_ext;
wenzelm
parents: 8806
diff changeset
    27
  val dir: T -> T
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    28
  val base: T -> T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    29
  val ext: string -> T -> T
14912
88b9d9165452 added split_ext; removed drop_ext;
wenzelm
parents: 8806
diff changeset
    30
  val split_ext: T -> T * string
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    31
  val expand: T -> T
26881
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
    32
  val position: T -> Position.T
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    33
end;
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    34
6187
c6c4626ef693 enabled sig;
wenzelm
parents: 6183
diff changeset
    35
structure Path: PATH =
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    36
struct
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    37
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    38
(* path elements *)
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    39
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    40
datatype elem =
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    41
  Root of string |
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    42
  Basic of string |
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    43
  Variable of string |
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    44
  Parent;
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    45
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    46
local
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    47
6223
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    48
fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    49
6319
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
    50
fun check_elem (chs as []) = err_elem "Illegal" chs
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
    51
  | check_elem (chs as ["~"]) = err_elem "Illegal" chs
6223
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    52
  | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    53
  | check_elem chs =
48420
a8ed41b6280b disallow quotes in path specifications -- extra paranoia;
wenzelm
parents: 47661
diff changeset
    54
      (case inter (op =) ["/", "\\", "$", ":", "\"", "'"] chs of
6223
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    55
        [] => chs
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    56
      | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    57
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    58
in
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    59
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    60
val root_elem = Root o implode o check_elem;
6223
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    61
val basic_elem = Basic o implode o check_elem;
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    62
val variable_elem = Variable o implode o check_elem;
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    63
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    64
end;
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    65
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    66
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    67
(* type path *)
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    68
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    69
datatype T = Path of elem list;    (*reversed elements*)
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    70
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    71
fun rep (Path xs) = xs;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    72
6460
cb8c85435228 added is_current;
wenzelm
parents: 6319
diff changeset
    73
fun is_current (Path []) = true
cb8c85435228 added is_current;
wenzelm
parents: 6319
diff changeset
    74
  | is_current _ = false;
cb8c85435228 added is_current;
wenzelm
parents: 6319
diff changeset
    75
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    76
val current = Path [];
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    77
val root = Path [Root ""];
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 36135
diff changeset
    78
fun named_root s = Path [root_elem (raw_explode s)];
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 36135
diff changeset
    79
fun basic s = Path [basic_elem (raw_explode s)];
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 36135
diff changeset
    80
fun variable s = Path [variable_elem (raw_explode s)];
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    81
val parent = Path [Parent];
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    82
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    83
fun is_absolute (Path xs) =
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    84
  (case try List.last xs of
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    85
    SOME (Root _) => true
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    86
  | _ => false);
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    87
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    88
fun is_basic (Path [Basic _]) = true
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    89
  | is_basic _ = false;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    90
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    91
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    92
(* append and norm *)
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    93
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    94
fun apply (y as Root _) _ = [y]
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    95
  | apply Parent (xs as (Root _ :: _)) = xs
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    96
  | apply Parent (Basic _ :: rest) = rest
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    97
  | apply y xs = y :: xs;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    98
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
    99
fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs);
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   100
fun appends paths = Library.foldl (uncurry append) (current, paths);
6319
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
   101
val make = appends o map basic;
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   102
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   103
fun norm elems = fold_rev apply elems [];
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   104
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   105
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   106
(* implode *)
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   107
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   108
local
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   109
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   110
fun implode_elem (Root "") = ""
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   111
  | implode_elem (Root s) = "//" ^ s
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   112
  | implode_elem (Basic s) = s
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   113
  | implode_elem (Variable s) = "$" ^ s
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   114
  | implode_elem Parent = "..";
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   115
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   116
in
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   117
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   118
fun implode_path (Path []) = "."
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   119
  | implode_path (Path [Root ""]) = "/"
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   120
  | implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs));
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   121
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   122
end;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   123
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   124
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   125
(* explode *)
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   126
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   127
local
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   128
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   129
fun explode_elem ".." = Parent
47661
012a887997f3 USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents: 45666
diff changeset
   130
  | explode_elem "~" = Variable "USER_HOME"
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   131
  | explode_elem "~~" = Variable "ISABELLE_HOME"
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   132
  | explode_elem s =
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 36135
diff changeset
   133
      (case raw_explode s of
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   134
        "$" :: cs => variable_elem cs
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   135
      | cs => basic_elem cs);
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   136
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   137
val explode_elems =
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   138
  rev o map explode_elem o filter_out (fn c => c = "" orelse c = ".");
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   139
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   140
in
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   141
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   142
fun explode_path str =
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   143
  let val (roots, raw_elems) =
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   144
    (case take_prefix (equal "") (space_explode "/" str) |>> length of
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   145
      (0, es) => ([], es)
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   146
    | (1, es) => ([Root ""], es)
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   147
    | (_, []) => ([Root ""], [])
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 36135
diff changeset
   148
    | (_, e :: es) => ([root_elem (raw_explode e)], es))
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   149
  in Path (norm (explode_elems raw_elems @ roots)) end;
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   150
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   151
end;
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   152
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   153
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
   154
(* print *)
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
   155
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
   156
fun pretty path =
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
   157
  let val s = implode_path path
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44863
diff changeset
   158
  in Pretty.mark (Isabelle_Markup.path s) (Pretty.str (quote s)) end;
43593
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
   159
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
   160
val print = Pretty.str_of o pretty;
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
   161
11140987d415 print Path.T with some markup;
wenzelm
parents: 41944
diff changeset
   162
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   163
(* base element *)
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   164
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   165
fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
43599
e0ee016fc4fd proper Path.print;
wenzelm
parents: 43593
diff changeset
   166
  | split_path _ path = error ("Cannot split path into dir/base: " ^ print path);
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   167
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   168
val dir = split_path #1;
7929
2010ae0393ca added drop_ext;
wenzelm
parents: 7714
diff changeset
   169
val base = split_path (fn (_, s) => Path [Basic s]);
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   170
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   171
fun ext "" = I
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   172
  | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   173
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   174
val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 36135
diff changeset
   175
  (case take_suffix (fn c => c <> ".") (raw_explode s) of
14912
88b9d9165452 added split_ext; removed drop_ext;
wenzelm
parents: 8806
diff changeset
   176
    ([], _) => (Path [Basic s], "")
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   177
  | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
6319
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
   178
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   179
17827
b32fad049413 expand: error on undefined/empty env variable;
wenzelm
parents: 15570
diff changeset
   180
(* expand variables *)
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   181
48658
4c7932270d6d reject path variable nesting explicitly;
wenzelm
parents: 48420
diff changeset
   182
fun eval (Variable s) =
4c7932270d6d reject path variable nesting explicitly;
wenzelm
parents: 48420
diff changeset
   183
      let val path = explode_path (getenv_strict s) in
4c7932270d6d reject path variable nesting explicitly;
wenzelm
parents: 48420
diff changeset
   184
        if exists (fn Variable _ => true | _ => false) (rep path) then
4c7932270d6d reject path variable nesting explicitly;
wenzelm
parents: 48420
diff changeset
   185
          error ("Illegal path variable nesting: " ^ s ^ "=" ^ print path)
4c7932270d6d reject path variable nesting explicitly;
wenzelm
parents: 48420
diff changeset
   186
        else rep path
4c7932270d6d reject path variable nesting explicitly;
wenzelm
parents: 48420
diff changeset
   187
      end
17827
b32fad049413 expand: error on undefined/empty env variable;
wenzelm
parents: 15570
diff changeset
   188
  | eval x = [x];
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   189
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19305
diff changeset
   190
val expand = rep #> maps eval #> norm #> Path;
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   191
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   192
44863
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   193
(* source position -- with smart replacement ISABELLE_HOME *)
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   194
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   195
val isabelle_home = explode_path "~~";
26881
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
   196
44863
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   197
fun position path =
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   198
  let
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   199
    val s = implode_path path;
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   200
    val prfx = implode_path (expand isabelle_home) ^ "/";
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   201
  in
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   202
    Position.file
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   203
      (case try (unprefix prfx) s of
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   204
        NONE => s
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   205
      | SOME s' => "~~/" ^ s')
49ea566cb3b4 more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
wenzelm
parents: 44161
diff changeset
   206
  end;
26881
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
   207
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
   208
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   209
(*final declarations of this structure!*)
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   210
val implode = implode_path;
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   211
val explode = explode_path;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   212
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   213
end;
36135
89d1903fbd50 support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents: 33957
diff changeset
   214