author | wenzelm |
Thu, 04 Feb 1999 18:17:01 +0100 | |
changeset 6230 | 85fc589a66ea |
parent 6229 | f839b261b87f |
child 6231 | 438a642ee92d |
--- a/src/Pure/Thy/session.ML Thu Feb 04 18:16:22 1999 +0100 +++ b/src/Pure/Thy/session.ML Thu Feb 04 18:17:01 1999 +0100 @@ -48,9 +48,14 @@ fun finish () = (ThyInfo.finish_all (); session_finished := true); -(* use_dir *) (* FIXME info *) +(* use_dir *) + +val root_file = ThyLoad.ml_path "ROOT"; -fun use_dir reset info name = (init reset name; Use.exit_use "ROOT.ML"; finish ()); +fun use_dir reset info name = + (init reset name; + Symbol.use root_file handle _ => exit 1; + finish ()); end;