begin_theory: priority message to gain some robustness in sync communication;
authorwenzelm
Wed, 13 Sep 2000 22:32:15 +0200
changeset 9953035a8288310a
parent 9952 24914e42b857
child 9954 734e0ec40f44
begin_theory: priority message to gain some robustness in sync communication;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Sep 13 22:31:19 2000 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Sep 13 22:32:15 2000 +0200
     1.3 @@ -385,6 +385,7 @@
     1.4    let
     1.5      val assert_thy = if upd then quiet_update_thy true else weak_use_thy;
     1.6      val _ = check_unfinished error name;
     1.7 +    val _ = priority (loader_msg "looking up" [name]);
     1.8      val _ = (map Path.basic parents; seq assert_thy parents);
     1.9      val theory = PureThy.begin_theory name (map get_theory parents);
    1.10      val deps =