# HG changeset patch
# User clasohm
# Date 830255896 -7200
# Node ID d706a6dce9305feb845bd622d708e92e81e85af5
# Parent  e56cdf7117291dcda1a663f13070be990c4526bd
use_dir and exit_use_dir now change the CWD only temporarily

diff -r e56cdf711729 -r d706a6dce930 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Mon Apr 22 15:42:20 1996 +0200
+++ b/src/Pure/Thy/thy_read.ML	Tue Apr 23 12:38:16 1996 +0200
@@ -1354,18 +1354,24 @@
   in Symtab.lookup (d2, id) end;
 
 
-(*CD to a directory and load its ROOT.ML file;
+(*Temporarily enter a directory and load its ROOT.ML file;
   also do some work for HTML generation*)
-fun use_dir dirname =
-  (cd dirname;
-   if !make_html then init_html() else ();
-   use "ROOT.ML";
-   finish_html());
+local
 
-fun exit_use_dir dirname =
-  (cd dirname;
-   if !make_html then init_html() else ();
-   exit_use "ROOT.ML";
-   finish_html());
+  fun gen_use_dir use_cmd dirname =
+    let val old_dir = pwd ();
+    in cd dirname;
+       if !make_html then init_html() else ();
+       use_cmd "ROOT.ML";
+       finish_html();
+       cd old_dir
+    end;
+
+in
+
+  val use_dir = gen_use_dir use;
+  val exit_use_dir = gen_use_dir exit_use;
+
+end
 
 end;