replaced writeln by priority;
authorwenzelm
Fri, 01 Sep 2000 00:34:07 +0200
changeset 9778 1f6dca5c4bbb
parent 9777 232fb8886765
child 9779 c71a1acffc27
replaced writeln by priority;
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;