src/Pure/Thy/thy_load.ML
author wenzelm
Thu, 22 Jul 2010 23:29:39 +0200
changeset 37943 3cbd7fa164b1
parent 37939 965537d86fcc
child 37949 48a874444164
permissions -rw-r--r--
tuned message;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thy_load.ML
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     3
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
     4
Loading files that contribute to a theory, including global load path
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
     5
management.
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     6
*)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     7
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     8
signature BASIC_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     9
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    10
  val show_path: unit -> string list
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    11
  val add_path: string -> unit
10252
dd46544e259d added path_add;
wenzelm
parents: 9696
diff changeset
    12
  val path_add: string -> unit
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    13
  val del_path: string -> unit
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    14
  val reset_path: unit -> unit
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    15
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    16
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    17
signature THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    18
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    19
  include BASIC_THY_LOAD
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    20
  val ml_path: string -> Path.T
7901
c21c3d2256ef export thy_path;
wenzelm
parents: 7438
diff changeset
    21
  val thy_path: string -> Path.T
29418
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    22
  val split_thy_path: Path.T -> Path.T * string
37937
9e482a3e651e tuned signature;
wenzelm
parents: 37903
diff changeset
    23
  val consistent_name: string -> string -> unit
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    24
  val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    25
  val check_file: Path.T -> Path.T -> Path.T * File.ident
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
    26
  val check_thy: Path.T -> string -> Path.T * File.ident
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
    27
  val deps_thy: Path.T -> string ->
37902
4e7864f3643d deps_thy/load_thy: store compact text to reduce space by factor 12;
wenzelm
parents: 37216
diff changeset
    28
   {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
23885
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
    29
  val load_ml: Path.T -> Path.T -> Path.T * File.ident
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    30
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    31
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 33221
diff changeset
    32
structure Thy_Load: THY_LOAD =
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    33
struct
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    34
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    35
(* maintain load path *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    36
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32466
diff changeset
    37
local val load_path = Unsynchronized.ref [Path.current] in
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    38
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
    39
fun show_path () = map Path.implode (! load_path);
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    40
33221
wenzelm
parents: 32966
diff changeset
    41
fun del_path s =
wenzelm
parents: 32966
diff changeset
    42
  CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
wenzelm
parents: 32966
diff changeset
    43
wenzelm
parents: 32966
diff changeset
    44
fun add_path s =
wenzelm
parents: 32966
diff changeset
    45
  CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
wenzelm
parents: 32966
diff changeset
    46
wenzelm
parents: 32966
diff changeset
    47
fun path_add s =
wenzelm
parents: 32966
diff changeset
    48
  CRITICAL (fn () =>
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32466
diff changeset
    49
    (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
33221
wenzelm
parents: 32966
diff changeset
    50
37938
445e5a3244cc eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
wenzelm
parents: 37937
diff changeset
    51
fun reset_path () = CRITICAL (fn () => load_path := [Path.current]);
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    52
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    53
fun search_path dir path =
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    54
  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    55
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    56
end;
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    57
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    58
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    59
(* file formats *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    60
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    61
val ml_path = Path.ext "ML" o Path.basic;
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    62
val thy_path = Path.ext "thy" o Path.basic;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    63
29418
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    64
fun split_thy_path path =
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    65
  (case Path.split_ext path of
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    66
    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    67
  | _ => error ("Bad theory file specification " ^ Path.implode path));
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    68
37937
9e482a3e651e tuned signature;
wenzelm
parents: 37903
diff changeset
    69
fun consistent_name name name' =
9e482a3e651e tuned signature;
wenzelm
parents: 37903
diff changeset
    70
  if name = name' then ()
9e482a3e651e tuned signature;
wenzelm
parents: 37903
diff changeset
    71
  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
9e482a3e651e tuned signature;
wenzelm
parents: 37903
diff changeset
    72
    " does not agree with theory name " ^ quote name');
9e482a3e651e tuned signature;
wenzelm
parents: 37903
diff changeset
    73
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    74
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
    75
(* check files *)
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    76
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    77
local
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    78
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    79
exception NOT_FOUND of Path.T list * Path.T;
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    80
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    81
fun try_file dir src_path =
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    82
  let
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    83
    val prfxs = search_path dir src_path;
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    84
    val path = Path.expand src_path;
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
    85
    val _ = Path.is_current path andalso error "Bad file specification";
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    86
    val result =
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    87
      prfxs |> get_first (fn prfx =>
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    88
        let val full_path = File.full_path (Path.append prfx path)
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    89
        in Option.map (pair full_path) (File.ident full_path) end);
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    90
  in
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    91
    (case result of
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    92
      SOME res => res
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    93
    | NONE => raise NOT_FOUND (prfxs, path))
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    94
  end;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    95
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    96
in
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    97
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    98
fun test_file dir file =
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
    99
  SOME (try_file dir file) handle NOT_FOUND _ => NONE;
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   100
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   101
fun check_file dir file =
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   102
  try_file dir file handle NOT_FOUND (prfxs, path) =>
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   103
    error ("Could not find file " ^ quote (Path.implode path) ^
37943
3cbd7fa164b1 tuned message;
wenzelm
parents: 37939
diff changeset
   104
      "\nin " ^ commas_quote (map Path.implode prfxs));
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   105
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   106
fun check_thy dir name = check_file dir (thy_path name);
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   107
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   108
end;
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
   109
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
   110
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   111
(* theory deps *)
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   112
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
   113
fun deps_thy dir name =
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   114
  let
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
   115
    val master as (path, _) = check_thy dir name;
37902
4e7864f3643d deps_thy/load_thy: store compact text to reduce space by factor 12;
wenzelm
parents: 37216
diff changeset
   116
    val text = File.read path;
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   117
    val (name', imports, uses) =
37903
b7ae269c0d68 replaced Source.of_list_limited by slightly more economic Source.of_string_limited;
wenzelm
parents: 37902
diff changeset
   118
      Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
37937
9e482a3e651e tuned signature;
wenzelm
parents: 37903
diff changeset
   119
    val _ = consistent_name name name';
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
   120
    val uses = map (Path.explode o #1) uses;
24065
21483400c2ca load_thy: avoid reloading of text;
wenzelm
parents: 23944
diff changeset
   121
  in {master = master, text = text, imports = imports, uses = uses} end;
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
   122
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   123
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   124
(* ML files *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   125
23885
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
   126
fun load_ml dir raw_path =
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   127
  let
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   128
    val (path, id) = check_file dir raw_path;
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   129
    val _ = ML_Context.eval_file path;
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37938
diff changeset
   130
  in (path, id) end;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   131
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   132
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   133
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 33221
diff changeset
   134
structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32466
diff changeset
   135
open Basic_Thy_Load;