# HG changeset patch
# User wenzelm
# Date 1119025991 -7200
# Node ID 8c3118c9c054fec3c8ce204fab969344d60e5898
# Parent  2427be27cc60eb6a7289ef6d6246bb4d2d8fc0e7
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
proper treatment of Pure session;

diff -r 2427be27cc60 -r 8c3118c9c054 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Jun 17 18:33:08 2005 +0200
+++ b/src/Pure/Thy/present.ML	Fri Jun 17 18:33:11 2005 +0200
@@ -72,23 +72,24 @@
 
 (** 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;
+end);
 
-structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs);
 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;
 
 
@@ -234,7 +235,7 @@
 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 ()));