# HG changeset patch
# User wenzelm
# Date 879348117 -3600
# Node ID 68c7b37f8721b2dad1c402296d1b90f0311bdb41
# Parent  6ae637493076628866c472bc97c33147576083fc
major cleanup;
removed several obsolete functions;
moved file stuff to Thy/file.ML;

diff -r 6ae637493076 -r 68c7b37f8721 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Nov 12 16:21:26 1997 +0100
+++ b/src/Pure/library.ML	Wed Nov 12 16:21:57 1997 +0100
@@ -4,13 +4,13 @@
     Copyright   1992  University of Cambridge
 
 Basic library: functions, options, pairs, booleans, lists, integers,
-strings, lists as sets, association lists, generic tables, balanced trees,
-orders, input / output, timing, filenames, misc functions.
+strings, lists as sets, association lists, generic tables, balanced
+trees, orders, diagnostics, timing, misc functions.
 *)
 
-infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
-      mem mem_int mem_string union union_int union_string  
-      inter inter_int inter_string subset subset_int subset_string subdir_of;
+infix |> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
+  mem mem_int mem_string union union_int union_string inter inter_int
+  inter_string subset subset_int subset_string;
 
 
 structure Library =
@@ -27,16 +27,10 @@
 (*reverse apply*)
 fun (x |> f) = f x;
 
-(*combine two functions forming the union of their domains*)
-fun (f orelf g) = fn x => f x handle Match => g x;
-
 (*application of (infix) operator to its left or right argument*)
 fun apl (x, f) y = f (x, y);
 fun apr (f, y) x = f (x, y);
 
-(*functional for pairs*)
-fun pairself f (x, y) = (f x, f y);
-
 (*function exponentiation: f(...(f x)...) with n applications of f*)
 fun funpow n f x =
   let fun rep (0, x) = x
@@ -61,6 +55,7 @@
 fun the (Some x) = x
   | the None = raise OPTION;
 
+(*strict!*)
 fun if_none None y = y
   | if_none (Some x) _ = x;
 
@@ -97,9 +92,10 @@
 
 fun swap (x, y) = (y, x);
 
-(*apply the function to a component of a pair*)
+(*apply function to components*)
 fun apfst f (x, y) = (f x, y);
 fun apsnd f (x, y) = (x, f y);
+fun pairself f (x, y) = (f x, f y);
 
 
 
@@ -114,29 +110,11 @@
 (* operators for combining predicates *)
 
 fun (p orf q) = fn x => p x orelse q x;
-
 fun (p andf q) = fn x => p x andalso q x;
 
-fun notf p x = not (p x);
-
 
 (* predicates on lists *)
 
-fun orl [] = false
-  | orl (x :: xs) = x orelse orl xs;
-
-fun andl [] = true
-  | andl (x :: xs) = x andalso andl xs;
-
-(*Several object-logics declare theories named List or Option, hiding the
-  eponymous basis library structures.*)
-structure Basis_Library =
-    struct
-    structure List = List
-    and       Option = Option
-    end;
-
-
 (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
 fun exists (pred: 'a -> bool) : 'a list -> bool =
   let fun boolf [] = false
@@ -156,6 +134,7 @@
 fun reset flag = (flag := false; false);
 fun toggle flag = (flag := not (! flag); ! flag);
 
+(*temporarily set flag, handling errors*)
 fun setmp flag value f x =
   let
     val orig_value = ! flag;
@@ -243,18 +222,22 @@
   | split_last [x] = ([], x)
   | split_last (x :: xs) = apfst (cons x) (split_last xs);
 
+(*find the position of an element in a list*)
+fun find_index pred =
+  let fun find _ [] = ~1
+        | find n (x :: xs) = if pred x then n else find (n + 1) xs;
+  in find 0 end;
 
-(*find the position of an element in a list*)
-fun find_index (pred: 'a->bool) : 'a list -> int =
-  let fun find _ []      = ~1
-        | find n (x::xs) = if pred x then n else find (n+1) xs
-  in find 0 end;
-fun find_index_eq x = find_index (equal x);
+val find_index_eq = find_index o equal;
+
+(*find first element satisfying predicate*)
+fun find_first _ [] = None
+  | find_first pred (x :: xs) =
+      if pred x then Some x else find_first pred xs;
 
 (*flatten a list of lists to a list*)
 fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
 
-
 (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
   (proc x1; ...; proc xn) for side effects*)
 fun seq (proc: 'a -> unit) : 'a list -> unit =
@@ -262,7 +245,6 @@
         | seqf (x :: xs) = (proc x; seqf xs)
   in seqf end;
 
-
 (*separate s [x1, x2, ..., xn]  ===>  [x1, s, x2, s, ..., s, xn]*)
 fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
   | separate _ xs = xs;
@@ -287,7 +269,6 @@
 
 fun filter_out f = filter (not o f);
 
-
 fun mapfilter (f: 'a -> 'b option) ([]: 'a list) = [] : 'b list
   | mapfilter f (x :: xs) =
       (case f x of
@@ -295,11 +276,6 @@
       | Some y => y :: mapfilter f xs);
 
 
-fun find_first pred = let
-  fun f [] = None
-  |   f (x :: xs) = if pred x then Some x else f  xs
-  in f end;
-
 (* lists of pairs *)
 
 fun map2 _ ([], []) = []
@@ -320,7 +296,6 @@
   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
   | _ ~~ _ = raise LIST "~~";
 
-
 (*inverse of ~~; the old 'split':
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
 fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l);
@@ -396,6 +371,7 @@
   | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i;
 
 
+
 (** strings **)
 
 fun is_letter ch =
@@ -420,7 +396,6 @@
 (*printable chars*)
 fun is_printable c = ord c > ord " " andalso ord c <= ord "~";
 
-
 (*lower all chars of string*)
 val to_lower =
   let
@@ -430,14 +405,13 @@
       else ch;
   in implode o (map lower) o explode end;
 
-
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;
 
 (*simple quoting (does not escape special chars)*)
 val quote = enclose "\"" "\"";
 
-(*space_implode "..." (explode "hello"); gives "h...e...l...l...o"*)
+(*space_implode "..." (explode "hello") = "h...e...l...l...o"*)
 fun space_implode a bs = implode (separate a bs);
 
 val commas = space_implode ", ";
@@ -446,17 +420,7 @@
 (*concatenate messages, one per line, into a string*)
 val cat_lines = space_implode "\n";
 
-(*BAD_space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*)
-fun BAD_space_explode sep s =
-  let fun divide [] "" = []
-        | divide [] part = [part]
-        | divide (c::s) part =
-            if c = sep then
-              (if part = "" then divide s "" else part :: divide s "")
-            else divide s (part ^ c)
-  in divide (explode s) "" end;
-
-(*space_explode "." "h.e..l.lo"; gives ["h", "e", "", "l", "lo"]*)
+(*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
 fun space_explode _ "" = []
   | space_explode sep str =
       let
@@ -798,7 +762,7 @@
 
 (*print error message and abort to top level*)
 exception ERROR;
-fun error_msg s = !error_fn s;			(*promise to raise ERROR later!*)
+fun error_msg s = !error_fn s;	  (*promise to raise ERROR later!*)
 fun error s = (error_msg s; raise ERROR);
 fun sys_error msg = (error_msg " !! SYSTEM ERROR !!\n"; error msg);
 
@@ -806,14 +770,13 @@
 fun deny p msg = if p then error msg else ();
 
 (*Assert pred for every member of l, generating a message if pred fails*)
-fun assert_all pred l msg_fn = 
+fun assert_all pred l msg_fn =
   let fun asl [] = ()
-        | asl (x::xs) = if pred x then asl xs
-                        else error (msg_fn x)
-  in  asl l  end;
+        | asl (x::xs) = if pred x then asl xs else error (msg_fn x)
+  in asl l end;
 
 
-(* handle errors (capturing messages) *)
+(* handle errors capturing messages *)
 
 datatype 'a error =
   Error of string |
@@ -825,64 +788,12 @@
     fun capture s = buffer := ! buffer ^ s ^ "\n";
     val result = Some (setmp error_fn capture f x) handle ERROR => None;
   in
-    case result of
+    (case result of
       None => Error (! buffer)
-    | Some y => OK y
-  end;
-
-
-(* read / write files *)
-
-fun read_file name =
-  let
-    val instream  = TextIO.openIn name;
-    val intext = TextIO.inputAll instream;
-  in
-    TextIO.closeIn instream;
-    intext
-  end;
-
-fun write_file name txt =
-  let val outstream = TextIO.openOut name in
-    TextIO.output (outstream, txt);
-    TextIO.closeOut outstream
-  end;
-
-fun append_file name txt =
-  let val outstream = TextIO.openAppend name in
-    TextIO.output (outstream, txt);
-    TextIO.closeOut outstream
+    | Some y => OK y)
   end;
 
 
-(*for the "test" target in IsaMakefiles -- signifies successful termination*)
-fun maketest msg =
-  (writeln msg; write_file "test" "Test examples ran successfully\n");
-
-
-(*print a list surrounded by the brackets lpar and rpar, with comma separator
-  print nothing for empty list*)
-fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) =
-  let fun prec x = (prs ","; pre x)
-  in
-    (case l of
-      [] => ()
-    | x::l => (prs lpar; pre x; seq prec l; prs rpar))
-  end;
-
-(*print a list of items separated by newlines*)
-fun print_list_ln (pre: 'a -> unit) : 'a list -> unit =
-  seq (fn x => (pre x; writeln ""));
-
-
-val print_int = prs o string_of_int;
-
-
-(* output to LaTeX / xdvi *)
-fun latex s =
-  execute ("( cd /tmp ; echo \"" ^ s ^
-    "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &");
-
 
 (** timing **)
 
@@ -892,69 +803,6 @@
 (*timed application function*)
 fun timeap f x = timeit (fn () => f x);
 
-(*timed "use" function, printing filenames*)
-fun time_use fname = timeit (fn () =>
-  (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
-   writeln ("\n**** Finished " ^ fname ^ " ****")));
-
-(*use the file, but exit with error code if errors found.*)
-fun exit_use fname = use fname handle _ => exit 1;
-
-
-(** filenames and paths **)
-
-(*Convert UNIX filename of the form "path/file" to "path/" and "file";
-  if filename contains no slash, then it returns "" and "file"*)
-val split_filename =
-  (pairself implode) o take_suffix (not_equal "/") o explode;
-
-val base_name = #2 o split_filename;
-
-(*Merge splitted filename (path and file);
-  if path does not end with one a slash is appended*)
-fun tack_on "" name = name
-  | tack_on path name =
-      if last_elem (explode path) = "/" then path ^ name
-      else path ^ "/" ^ name;
-
-(*Remove the extension of a filename, i.e. the part after the last '.'*)
-val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode;
-
-(*Make relative path to reach an absolute location from a different one*)
-fun relative_path cur_path dest_path =
-  let (*Remove common beginning of both paths and make relative path*)
-      fun mk_relative [] [] = []
-        | mk_relative [] ds = ds
-        | mk_relative cs [] = map (fn _ => "..") cs
-        | mk_relative (c::cs) (d::ds) =
-            if c = d then mk_relative cs ds
-            else ".." :: map (fn _ => "..") cs @ (d::ds);
-  in if cur_path = "" orelse hd (explode cur_path) <> "/" orelse
-        dest_path = "" orelse hd (explode dest_path) <> "/" then
-       error "Relative or empty path passed to relative_path"
-     else ();
-     space_implode "/" (mk_relative (BAD_space_explode "/" cur_path)
-                                    (BAD_space_explode "/" dest_path))
-  end;
-
-(*Determine if absolute path1 is a subdirectory of absolute path2*)
-fun path1 subdir_of path2 =
-  if hd (explode path1) <> "/" orelse hd (explode path2) <> "/" then
-    error "Relative or empty path passed to subdir_of"
-  else (BAD_space_explode "/" path2) prefix (BAD_space_explode "/" path1);
-
-fun absolute_path cwd file =
-  let fun rm_points [] result = rev result
-        | rm_points (".."::ds) result = rm_points ds (tl result)
-        | rm_points ("."::ds) result = rm_points ds result
-        | rm_points (d::ds) result = rm_points ds (d::result);
-  in if file = "" then ""
-     else if hd (explode file) = "/" then file
-     else "/" ^ space_implode "/"
-                  (rm_points (BAD_space_explode "/" (tack_on cwd file)) [])
-  end;
-
-fun file_exists file = (file_info file <> "");
 
 
 (** misc functions **)
@@ -1112,9 +960,12 @@
             in implode lets :: scanwords is_let rest end;
   in scan1 (#2 (take_prefix (not o is_let) cs)) end;
 
+
+
+(* Variable-branching trees: for proof terms etc. *)
+datatype 'a mtree = Join of 'a * 'a mtree list;
+
+
 end;
 
-(*Variable-branching trees: for proof terms*)
-datatype 'a mtree = Join of 'a * 'a mtree list;
-
 open Library;