src/Pure/Thy/present.ML
changeset 32738 15bb09ca0378
parent 31819 2c0ab4485f48
child 33522 737589bb9bb8
     1.1 --- a/src/Pure/Thy/present.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -161,10 +161,11 @@
     1.4  
     1.5  (* state *)
     1.6  
     1.7 -val browser_info = ref empty_browser_info;
     1.8 -fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
     1.9 +val browser_info = Unsynchronized.ref empty_browser_info;
    1.10 +fun change_browser_info f =
    1.11 +  CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
    1.12  
    1.13 -val suppress_tex_source = ref false;
    1.14 +val suppress_tex_source = Unsynchronized.ref false;
    1.15  fun no_document f x = setmp_noncritical suppress_tex_source true f x;
    1.16  
    1.17  fun init_theory_info name info =
    1.18 @@ -229,7 +230,7 @@
    1.19  
    1.20  (* state *)
    1.21  
    1.22 -val session_info = ref (NONE: session_info option);
    1.23 +val session_info = Unsynchronized.ref (NONE: session_info option);
    1.24  
    1.25  fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
    1.26  fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
    1.27 @@ -534,5 +535,5 @@
    1.28  
    1.29  end;
    1.30  
    1.31 -structure BasicPresent: BASIC_PRESENT = Present;
    1.32 -open BasicPresent;
    1.33 +structure Basic_Present: BASIC_PRESENT = Present;
    1.34 +open Basic_Present;