use_dir and exit_use_dir now change the CWD only temporarily
authorclasohm
Tue Apr 23 12:38:16 1996 +0200 (1996-04-23)
changeset 1670d706a6dce930
parent 1669 e56cdf711729
child 1671 608196238072
use_dir and exit_use_dir now change the CWD only temporarily
src/Pure/Thy/thy_read.ML
     1.1 --- a/src/Pure/Thy/thy_read.ML	Mon Apr 22 15:42:20 1996 +0200
     1.2 +++ b/src/Pure/Thy/thy_read.ML	Tue Apr 23 12:38:16 1996 +0200
     1.3 @@ -1354,18 +1354,24 @@
     1.4    in Symtab.lookup (d2, id) end;
     1.5  
     1.6  
     1.7 -(*CD to a directory and load its ROOT.ML file;
     1.8 +(*Temporarily enter a directory and load its ROOT.ML file;
     1.9    also do some work for HTML generation*)
    1.10 -fun use_dir dirname =
    1.11 -  (cd dirname;
    1.12 -   if !make_html then init_html() else ();
    1.13 -   use "ROOT.ML";
    1.14 -   finish_html());
    1.15 +local
    1.16  
    1.17 -fun exit_use_dir dirname =
    1.18 -  (cd dirname;
    1.19 -   if !make_html then init_html() else ();
    1.20 -   exit_use "ROOT.ML";
    1.21 -   finish_html());
    1.22 +  fun gen_use_dir use_cmd dirname =
    1.23 +    let val old_dir = pwd ();
    1.24 +    in cd dirname;
    1.25 +       if !make_html then init_html() else ();
    1.26 +       use_cmd "ROOT.ML";
    1.27 +       finish_html();
    1.28 +       cd old_dir
    1.29 +    end;
    1.30 +
    1.31 +in
    1.32 +
    1.33 +  val use_dir = gen_use_dir use;
    1.34 +  val exit_use_dir = gen_use_dir exit_use;
    1.35 +
    1.36 +end
    1.37  
    1.38  end;