use_thy: do not set implicit ML context anymore;
authorwenzelm
Sun Jan 27 22:21:37 2008 +0100 (2008-01-27)
changeset 25994d35484265f46
parent 25993 d542486e39e7
child 25995 21b51f748daf
use_thy: do not set implicit ML context anymore;
NEWS
src/Pure/Thy/thy_info.ML
     1.1 --- a/NEWS	Sun Jan 27 22:21:35 2008 +0100
     1.2 +++ b/NEWS	Sun Jan 27 22:21:37 2008 +0100
     1.3 @@ -13,6 +13,11 @@
     1.4  specified via 3 decimal digits (as in SML).  E.g. "foo\095bar" for
     1.5  "foo_bar".
     1.6  
     1.7 +* Theory loader: use_thy (and similar operations) no longer set the
     1.8 +implicit ML context, which was occasionally hard to predict and in
     1.9 +conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which
    1.10 +provides a proper context already.
    1.11 +
    1.12  
    1.13  *** Pure ***
    1.14  
     2.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jan 27 22:21:35 2008 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jan 27 22:21:37 2008 +0100
     2.3 @@ -485,8 +485,7 @@
     2.4  fun gen_use_thy req str =
     2.5    let val name = base_name str in
     2.6      check_unfinished warning name;
     2.7 -    gen_use_thy' req Path.current str;
     2.8 -    CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (get_theory name))))
     2.9 +    gen_use_thy' req Path.current str
    2.10    end;
    2.11  
    2.12  in
    2.13 @@ -532,9 +531,6 @@
    2.14      val dir = master_dir'' (lookup_deps name);
    2.15      val _ = check_unfinished error name;
    2.16      val _ = if int then use_thys_dir dir parents else ();
    2.17 -    (* FIXME tmp *)
    2.18 -    val _ = CRITICAL (fn () =>
    2.19 -      ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names)))));
    2.20  
    2.21      val theory = Theory.begin_theory name (map get_theory parent_names);
    2.22