src/Pure/Thy/present.ML

   make_browser_info (f (theories, files, tex_index, html_index, graph));
 
 
 (* state *)
 
-val browser_info = ref empty_browser_info;
-fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
-
-val suppress_tex_source = ref false;
+val browser_info = Unsynchronized.ref empty_browser_info;
+fun change_browser_info f =
+  CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
+
+val suppress_tex_source = Unsynchronized.ref false;
 fun no_document f x = setmp_noncritical suppress_tex_source true f x;
 
 fun init_theory_info name info =
   change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
     (Symtab.update (name, info) theories, files, tex_index, html_index, graph));

     verbose = verbose, readme = readme}: session_info;
 
 
 (* state *)
 
-val session_info = ref (NONE: session_info option);
+val session_info = Unsynchronized.ref (NONE: session_info option);
 
 fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
 fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
 
 

   in isabelle_document false doc_format documentN "" doc_path result_path end;
 
 
 end;
 
-structure BasicPresent: BASIC_PRESENT = Present;
-open BasicPresent;
+structure Basic_Present: BASIC_PRESENT = Present;
+open Basic_Present;