# HG changeset patch
# User wenzelm
# Date 967761247 -7200
# Node ID 1f6dca5c4bbbd4d4e5ed537b16403a6303d9fa35
# Parent  232fb8886765be5f9a4559162750f47c840a135a
replaced writeln by priority;

diff -r 232fb8886765 -r 1f6dca5c4bbb src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Sep 01 00:33:36 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Sep 01 00:34:07 2000 +0200
@@ -248,9 +248,9 @@
   if time then
     let val name = Path.pack path in
       timeit (fn () =>
-       (writeln ("\n**** Starting file " ^ quote name ^ " ****");
+       (priority ("\n**** Starting file " ^ quote name ^ " ****");
         run_file path;
-        writeln ("**** Finished file " ^ quote name ^ " ****\n")))
+        priority ("**** Finished file " ^ quote name ^ " ****\n")))
     end
   else run_file path;
 
@@ -267,7 +267,7 @@
 
 fun load_thy ml time initiators dir name parents =
   let
-    val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
+    val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
 
     val _ = touch_thy name;
     val master = ThyLoad.load_thy dir name ml time;
@@ -366,7 +366,7 @@
   if is_finished name then error (loader_msg "cannot remove finished theory" [name])
   else
     let val succs = thy_graph Graph.all_succs [name] in
-      writeln (loader_msg "removing" succs);
+      priority (loader_msg "removing" succs);
       seq (perform Remove) succs;
       change_thys (Graph.del_nodes succs)
     end;