# HG changeset patch
# User wenzelm
# Date 926520871 -7200
# Node ID 254ab03bd08289e414e62bdd1dda0926feba0742
# Parent  d2e8342bf5c34f8b1c910adc6f8ee8729ff4979d
rearranged some modules;

diff -r d2e8342bf5c3 -r 254ab03bd082 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed May 12 16:52:28 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed May 12 16:54:31 1999 +0200
@@ -198,7 +198,7 @@
 
 fun deps_thy name ml path =
   let
-    val src = Source.of_file path;
+    val src = File.source path;
     val is_old = warn_theory_style path (is_old_theory src);
     val (name', parents, files) =
       (*Note: old style headers dynamically depend on the current lexicon :-( *)
@@ -248,7 +248,7 @@
   end;
 
 fun run_thy name path =
-  let val (src, pos) = Source.of_file path in
+  let val (src, pos) = File.source path in
     Present.theory_source name src;
     if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src)
     else (Toplevel.excursion (parse_thy (src, pos))
diff -r d2e8342bf5c3 -r 254ab03bd082 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Wed May 12 16:52:28 1999 +0200
+++ b/src/Pure/Isar/session.ML	Wed May 12 16:54:31 1999 +0200
@@ -61,7 +61,7 @@
 fun use_dir reset info parent name =
   (init reset parent name;
     Present.init info (path ()) name;
-    Symbol.use root_file;
+    File.symbol_use root_file;
     finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
 
 
diff -r d2e8342bf5c3 -r 254ab03bd082 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed May 12 16:52:28 1999 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed May 12 16:54:31 1999 +0200
@@ -75,7 +75,7 @@
 fun load_file raw_path =
   (case check_file raw_path of
     None => error ("Could not find ML file " ^ quote (Path.pack raw_path))
-  | Some (path, info) => (Symbol.use path; (path, info)));
+  | Some (path, info) => (File.symbol_use path; (path, info)));
 
 
 (* check_thy *)
diff -r d2e8342bf5c3 -r 254ab03bd082 src/Pure/Thy/thy_syn.ML
--- a/src/Pure/Thy/thy_syn.ML	Wed May 12 16:52:28 1999 +0200
+++ b/src/Pure/Thy/thy_syn.ML	Wed May 12 16:54:31 1999 +0200
@@ -55,7 +55,7 @@
     val txt_out = ThyParse.parse_thy (! syntax) chs;
   in
     File.write tmp_path txt_out;
-    Symbol.use tmp_path;
+    File.symbol_use tmp_path;
     if ! delete_tmpfiles then File.rm tmp_path else ()
   end;