# HG changeset patch
# User wenzelm
# Date 918069901 -3600
# Node ID 3e9d6edc99a8d321ba9063fbf1897aaabb006363
# Parent  9dac1ee185e37cc09dd2e1cb19be2aa99a3bce5b
added join_info;

diff -r 9dac1ee185e3 -r 3e9d6edc99a8 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Feb 03 17:36:55 1999 +0100
+++ b/src/Pure/General/file.ML	Wed Feb 03 20:25:01 1999 +0100
@@ -14,6 +14,7 @@
   val tmp_path: Path.T -> Path.T
   eqtype info
   val info: Path.T -> info option
+  val join_info: info -> info -> info
   val exists: Path.T -> bool
   val read: Path.T -> string
   val write: Path.T -> string -> unit
@@ -42,13 +43,15 @@
 
 (* info / exists *)
 
-datatype info = Info of string;
+datatype info = Info of string list;
+
+fun join_info (Info xs) (Info ys) = Info (xs @ ys);
 
 fun info path =
   let val name = sysify path in
     (case file_info name of
       "" => None
-    | s => Some (Info (name ^ ": " ^ s)))	(* FIXME include full path (!?) *)
+    | s => Some (Info [name ^ ": " ^ s]))	(* FIXME include full path (!?) *)
   end;
 
 val exists = is_some o info;