src/Pure/General/file.ML
author wenzelm
Wed, 03 Feb 1999 16:32:32 +0100
changeset 6182 4a07dfe3583f
parent 6118 caa439435666
child 6218 3e9d6edc99a8
permissions -rw-r--r--
use Path.T; added 'cd', 'rm', 'use';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 5009
diff changeset
     1
(*  Title:      Pure/General/file.ML
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     4
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     5
File system operations.
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
     6
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
     7
TODO:
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
     8
  - close in case of error (!?);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     9
*)
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    10
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    11
signature FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    12
sig
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    13
  val sys_path_fn: (Path.T -> string) ref
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    14
  val tmp_path: Path.T -> Path.T
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    15
  eqtype info
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    16
  val info: Path.T -> info option
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    17
  val exists: Path.T -> bool
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    18
  val read: Path.T -> string
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    19
  val write: Path.T -> string -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    20
  val append: Path.T -> string -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    21
  val copy: Path.T -> Path.T -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    22
  val use: Path.T -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    23
  val cd: Path.T -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    24
  val rm: Path.T -> unit
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    25
end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    26
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    27
structure File: FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    28
struct
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    29
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    30
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    31
(* sys_path (default for Unix) *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    32
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    33
val sys_path_fn = ref Path.pack;
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    34
fun sysify path = ! sys_path_fn (Path.expand path);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    35
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    36
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    37
(* tmp_path *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    38
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    39
fun tmp_path path =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    40
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    41
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    42
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    43
(* info / exists *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    44
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    45
datatype info = Info of string;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    46
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    47
fun info path =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    48
  let val name = sysify path in
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    49
    (case file_info name of
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    50
      "" => None
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    51
    | s => Some (Info (name ^ ": " ^ s)))	(* FIXME include full path (!?) *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    52
  end;
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    53
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    54
val exists = is_some o info;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    55
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    56
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    57
(* read / write files *)
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    58
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    59
fun read path =
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    60
  let
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    61
    val instream  = TextIO.openIn (sysify path);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    62
    val intext = TextIO.inputAll instream;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    63
  in
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    64
    TextIO.closeIn instream;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    65
    intext
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    66
  end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    67
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    68
fun write path txt =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    69
  let val outstream = TextIO.openOut (sysify path) in
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    70
    TextIO.output (outstream, txt);
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    71
    TextIO.closeOut outstream
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    72
  end;
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    73
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    74
fun append path txt =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    75
  let val outstream = TextIO.openAppend (sysify path) in
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    76
    TextIO.output (outstream, txt);
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    77
    TextIO.closeOut outstream
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    78
  end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    79
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    80
fun copy inpath outpath = write outpath (read inpath);
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    81
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    82
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    83
(* misc operations *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    84
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    85
val use = use o sysify;
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    86
val cd = Library.cd o sysify;
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    87
val rm = OS.FileSys.remove o sysify;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    88
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    89
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    90
end;