src/Pure/Thy/present.ML

 
 
 
 (** additional theory data **)
 
-structure BrowserInfoArgs =
-struct
+val empty_browser_info = {name = "Pure", session = []: string list, is_local = false};
+
+structure BrowserInfoData = TheoryDataFun
+(struct
   val name = "Pure/browser_info";
   type T = {name: string, session: string list, is_local: bool};
-
-  val empty = {name = "Pure", session = [], is_local = false};
+  val empty = empty_browser_info;
   val copy = I;
-  fun prep_ext _ = {name = "", session = [], is_local = false};
-  fun merge _ = empty;
+  fun extend _ = {name = "", session = [], is_local = false};
+  fun merge _ _ = empty;
   fun print _ _ = ();
-end;
-
-structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs);
+end);
+
 val _ = Context.add_setup [BrowserInfoData.init];
 
 fun get_info thy =
-  if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty
+  if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
+  then empty_browser_info
   else BrowserInfoData.get thy;
 
 
 
 (** graphs **)

 (* state *)
 
 val session_info = 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 (PureThy.get_name (Context.the_context ()));
+fun with_context f = f (Context.theory_name (Context.the_context ()));
 
 
 
 (** document preparation **)