src/Pure/Thy/present.ML
changeset 51567 a86c5e02ba58
parent 51419 5313abe76bd4
child 52549 802576856527
equal deleted inserted replaced
51564:bfdc3f720bd6 51567:a86c5e02ba58
    50 (** additional theory data **)
    50 (** additional theory data **)
    51 
    51 
    52 structure Browser_Info = Theory_Data
    52 structure Browser_Info = Theory_Data
    53 (
    53 (
    54   type T = {chapter: string, name: string};
    54   type T = {chapter: string, name: string};
    55   val empty = {chapter = Context.PureN, name = Context.PureN}: T;
    55   val empty = {chapter = "Unsorted", name = "Unknown"}: T;
    56   fun extend _ = empty;
    56   fun extend _ = empty;
    57   fun merge _ = empty;
    57   fun merge _ = empty;
    58 );
    58 );
       
    59 
       
    60 val _ = Context.>> (Context.map_theory
       
    61   (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}));
    59 
    62 
    60 val session_name = #name o Browser_Info.get;
    63 val session_name = #name o Browser_Info.get;
    61 val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
    64 val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
    62 
    65 
    63 
    66