tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
authorwenzelm
Wed, 22 Aug 2012 21:06:26 +0200
changeset 48887 c49eca45cbb0
parent 48886 9604c6563226
child 48888 74ad16f79425
tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Aug 22 21:02:02 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Aug 22 21:06:26 2012 +0200
@@ -124,11 +124,7 @@
   Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
     (case Token.get_files tok of
       SOME files => files
-    | NONE =>
-        let
-          val path = Path.explode name;
-          val _ = warning ("Dynamic loading of files: " ^ Path.print path);
-        in read_files cmd (master_directory thy) path end));
+    | NONE => read_files cmd (master_directory thy) (Path.explode name)));
 
 fun resolve_files dir span =
   (case span of