accomodate change of TheoryDataFun;
authorwenzelm
Fri Jun 17 18:33:11 2005 +0200 (2005-06-17)
changeset 164268c3118c9c054
parent 16425 2427be27cc60
child 16427 9975aab75d72
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
proper treatment of Pure session;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Fri Jun 17 18:33:08 2005 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Fri Jun 17 18:33:11 2005 +0200
     1.3 @@ -72,23 +72,24 @@
     1.4  
     1.5  (** additional theory data **)
     1.6  
     1.7 -structure BrowserInfoArgs =
     1.8 -struct
     1.9 +val empty_browser_info = {name = "Pure", session = []: string list, is_local = false};
    1.10 +
    1.11 +structure BrowserInfoData = TheoryDataFun
    1.12 +(struct
    1.13    val name = "Pure/browser_info";
    1.14    type T = {name: string, session: string list, is_local: bool};
    1.15 -
    1.16 -  val empty = {name = "Pure", session = [], is_local = false};
    1.17 +  val empty = empty_browser_info;
    1.18    val copy = I;
    1.19 -  fun prep_ext _ = {name = "", session = [], is_local = false};
    1.20 -  fun merge _ = empty;
    1.21 +  fun extend _ = {name = "", session = [], is_local = false};
    1.22 +  fun merge _ _ = empty;
    1.23    fun print _ _ = ();
    1.24 -end;
    1.25 +end);
    1.26  
    1.27 -structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs);
    1.28  val _ = Context.add_setup [BrowserInfoData.init];
    1.29  
    1.30  fun get_info thy =
    1.31 -  if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty
    1.32 +  if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
    1.33 +  then empty_browser_info
    1.34    else BrowserInfoData.get thy;
    1.35  
    1.36  
    1.37 @@ -234,7 +235,7 @@
    1.38  val session_info = ref (NONE: session_info option);
    1.39  
    1.40  fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
    1.41 -fun with_context f = f (PureThy.get_name (Context.the_context ()));
    1.42 +fun with_context f = f (Context.theory_name (Context.the_context ()));
    1.43  
    1.44  
    1.45