src/Pure/General/path.ML
author haftmann
Tue, 23 Sep 2008 18:11:44 +0200
changeset 28337 93964076e7b8
parent 26881 bb68f50644a9
child 29606 fedb8be05f24
permissions -rw-r--r--
case default fallback for NBE
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
    ID:         $Id$
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
     4
23863
8f3099589cfa tuned signature;
wenzelm
parents: 23672
diff changeset
     5
Abstract algebra of file paths (external encoding in Unix style).
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
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    14
  val parent: T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    15
  val basic: string -> T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    16
  val variable: string -> T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    17
  val is_absolute: T -> bool
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    18
  val is_basic: T -> bool
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    19
  val append: T -> T -> T
6270
c905fe5994a2 val appends: T list -> T;
wenzelm
parents: 6223
diff changeset
    20
  val appends: T list -> T
6319
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
    21
  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
    22
  val implode: T -> string
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
    23
  val explode: string -> T
14912
88b9d9165452 added split_ext; removed drop_ext;
wenzelm
parents: 8806
diff changeset
    24
  val dir: T -> T
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    25
  val base: T -> T
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    26
  val ext: string -> T -> T
14912
88b9d9165452 added split_ext; removed drop_ext;
wenzelm
parents: 8806
diff changeset
    27
  val split_ext: T -> T * string
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    28
  val expand: T -> T
26881
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
    29
  val position: T -> Position.T
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    30
end;
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    31
6187
c6c4626ef693 enabled sig;
wenzelm
parents: 6183
diff changeset
    32
structure Path: PATH =
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    33
struct
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    34
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    35
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    36
(* path elements *)
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    37
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    38
datatype elem = Root | Parent | Basic of string | Variable of string;
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    39
6223
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    40
fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    41
6319
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
    42
fun check_elem (chs as []) = err_elem "Illegal" chs
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
    43
  | check_elem (chs as ["~"]) = err_elem "Illegal" chs
6223
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    44
  | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    45
  | check_elem chs =
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    46
      (case ["/", "\\", "$", ":"] inter_string chs of
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    47
        [] => chs
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    48
      | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    49
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    50
val basic_elem = Basic o implode o check_elem;
e8807883e3e3 check_elem: allow ~, except for '~' and '~~';
wenzelm
parents: 6187
diff changeset
    51
val variable_elem = Variable o implode o check_elem;
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    52
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    53
fun is_var (Variable _) = true
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    54
  | is_var _ = false;
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    55
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    56
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    57
(* type path *)
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    58
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    59
datatype T = Path of elem list;
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    60
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    61
fun rep (Path xs) = xs;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    62
6460
cb8c85435228 added is_current;
wenzelm
parents: 6319
diff changeset
    63
fun is_current (Path []) = true
cb8c85435228 added is_current;
wenzelm
parents: 6319
diff changeset
    64
  | is_current _ = false;
cb8c85435228 added is_current;
wenzelm
parents: 6319
diff changeset
    65
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    66
val current = Path [];
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    67
val root = Path [Root];
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    68
val parent = Path [Parent];
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    69
fun basic s = Path [basic_elem (explode s)];
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    70
fun variable s = Path [variable_elem (explode s)];
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    71
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    72
fun is_absolute (Path (Root :: _)) = true
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    73
  | is_absolute _ = false;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    74
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    75
fun is_basic (Path [Basic _]) = true
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    76
  | is_basic _ = false;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    77
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    78
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    79
(* append and norm *)
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    80
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    81
(*append non-normal path (2n arg) to reversed normal one, result is normal*)
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    82
fun rev_app xs [] = rev xs
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    83
  | rev_app _ (Root :: ys) = rev_app [Root] ys
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    84
  | rev_app (x :: xs) (Parent :: ys) =
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    85
      if x = Parent orelse is_var x then rev_app (Parent :: x :: xs) ys
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    86
      else if x = Root then rev_app (x :: xs) ys
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    87
      else rev_app xs ys
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    88
  | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    89
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    90
fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    91
fun appends paths = Library.foldl (uncurry append) (current, paths);
6319
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
    92
val make = appends o map basic;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    93
fun norm path = rev_app [] path;
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    94
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
    95
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
    96
(* implode *)
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
    97
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
    98
fun implode_elem Root = ""
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
    99
  | implode_elem Parent = ".."
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   100
  | implode_elem (Basic s) = s
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   101
  | implode_elem (Variable s) = "$" ^ s;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   102
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   103
fun implode_path (Path []) = "."
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   104
  | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   105
  | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   106
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   107
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   108
(* explode *)
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   109
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   110
fun explode_elem "" = Root
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   111
  | explode_elem ".." = Parent
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   112
  | explode_elem "~" = Variable "HOME"
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   113
  | 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
   114
  | explode_elem s =
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   115
      (case explode s of
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   116
        "$" :: cs => variable_elem cs
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   117
      | cs => basic_elem cs);
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   118
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   119
val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   120
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   121
fun explode_path str = Path (norm
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   122
  (case space_explode "/" str of
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   123
    "" :: ss => Root :: explode_elems ss
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   124
  | ss => explode_elems ss));
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   125
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   126
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   127
(* base element *)
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   128
7929
2010ae0393ca added drop_ext;
wenzelm
parents: 7714
diff changeset
   129
fun split_path f (path as Path xs) =
2010ae0393ca added drop_ext;
wenzelm
parents: 7714
diff changeset
   130
  (case try split_last xs of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   131
    SOME (prfx, Basic s) => f (prfx, s)
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   132
  | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   133
14912
88b9d9165452 added split_ext; removed drop_ext;
wenzelm
parents: 8806
diff changeset
   134
val dir = split_path (fn (prfx, _) => Path prfx);
7929
2010ae0393ca added drop_ext;
wenzelm
parents: 7714
diff changeset
   135
val base = split_path (fn (_, s) => Path [Basic s]);
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   136
7929
2010ae0393ca added drop_ext;
wenzelm
parents: 7714
diff changeset
   137
fun ext "" path = path
2010ae0393ca added drop_ext;
wenzelm
parents: 7714
diff changeset
   138
  | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   139
14912
88b9d9165452 added split_ext; removed drop_ext;
wenzelm
parents: 8806
diff changeset
   140
val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 17827
diff changeset
   141
  (case take_suffix (fn c => c <> ".") (explode s) of
14912
88b9d9165452 added split_ext; removed drop_ext;
wenzelm
parents: 8806
diff changeset
   142
    ([], _) => (Path [Basic s], "")
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   143
  | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
6319
80173cb8691c added make, dir;
wenzelm
parents: 6270
diff changeset
   144
6183
ca3ff2fee318 more abstract implementation;
wenzelm
parents: 6118
diff changeset
   145
17827
b32fad049413 expand: error on undefined/empty env variable;
wenzelm
parents: 15570
diff changeset
   146
(* expand variables *)
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   147
17827
b32fad049413 expand: error on undefined/empty env variable;
wenzelm
parents: 15570
diff changeset
   148
fun eval (Variable s) =
b32fad049413 expand: error on undefined/empty env variable;
wenzelm
parents: 15570
diff changeset
   149
    (case getenv s of
b32fad049413 expand: error on undefined/empty env variable;
wenzelm
parents: 15570
diff changeset
   150
      "" => error ("Undefined Isabelle environment variable: " ^ quote s)
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   151
    | path => rep (explode_path path))
17827
b32fad049413 expand: error on undefined/empty env variable;
wenzelm
parents: 15570
diff changeset
   152
  | eval x = [x];
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   153
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19305
diff changeset
   154
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
   155
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   156
26881
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
   157
(* source position *)
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
   158
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
   159
val position = Position.file o implode_path o expand;
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
   160
bb68f50644a9 renamed Position.path to Path.position;
wenzelm
parents: 23863
diff changeset
   161
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   162
(*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
   163
val implode = implode_path;
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19482
diff changeset
   164
val explode = explode_path;
5011
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   165
37c253fd3dc6 moved Thy/path.ML to General/path.ML;
wenzelm
parents:
diff changeset
   166
end;