marked some CRITICAL sections;
authorwenzelm
Mon Jul 30 11:12:28 2007 +0200 (2007-07-30 ago)
changeset 2407182873bc360c2
parent 24070 ff4c715a11cd
child 24072 8b9e5d776ef3
marked some CRITICAL sections;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Jul 30 10:39:12 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Jul 30 11:12:28 2007 +0200
     1.3 @@ -315,7 +315,8 @@
     1.4  val welcome = Toplevel.imperative (writeln o Session.welcome);
     1.5  
     1.6  val exit = Toplevel.keep (fn state =>
     1.7 -  (ML_Context.set_context (try Toplevel.generic_theory_of state); raise Toplevel.TERMINATE));
     1.8 + (CRITICAL (fn () => ML_Context.set_context (try Toplevel.generic_theory_of state));
     1.9 +  raise Toplevel.TERMINATE));
    1.10  
    1.11  val quit = Toplevel.imperative quit;
    1.12  
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 30 10:39:12 2007 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 30 11:12:28 2007 +0200
     2.3 @@ -280,7 +280,7 @@
     2.4  
     2.5  fun load_thy dir name pos text ml time =
     2.6   (run_thy dir name pos text time;
     2.7 -  ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
     2.8 +  CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name))));
     2.9    if ml then try_ml_file dir name time else ());
    2.10  
    2.11  in
    2.12 @@ -296,7 +296,7 @@
    2.13  (* main loop *)
    2.14  
    2.15  fun gen_loop term =
    2.16 - (ML_Context.set_context NONE;
    2.17 + (CRITICAL (fn () => ML_Context.set_context NONE);
    2.18    Toplevel.loop (isar term));
    2.19  
    2.20  fun gen_main term =
     3.1 --- a/src/Pure/Thy/thy_info.ML	Mon Jul 30 10:39:12 2007 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Jul 30 11:12:28 2007 +0200
     3.3 @@ -454,7 +454,7 @@
     3.4    let val name = base_name str in
     3.5      check_unfinished warning name;
     3.6      gen_use_thy' req Path.current str;
     3.7 -    ML_Context.set_context (SOME (Context.Theory (get_theory name)))
     3.8 +    CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (get_theory name))))
     3.9    end;
    3.10  
    3.11  in
    3.12 @@ -497,7 +497,8 @@
    3.13      val _ = check_unfinished error name;
    3.14      val _ = if int then quiet_update_thys dir parents else ();
    3.15      (* FIXME tmp *)
    3.16 -    val _ = ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names))));
    3.17 +    val _ = CRITICAL (fn () =>
    3.18 +      ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names)))));
    3.19      val _ = check_uses name uses;
    3.20  
    3.21      val theory =