--- a/src/Pure/Thy/present.ML Wed Mar 27 21:25:33 2013 +0100
+++ b/src/Pure/Thy/present.ML Thu Mar 28 14:01:56 2013 +0100
@@ -52,11 +52,14 @@
structure Browser_Info = Theory_Data
(
type T = {chapter: string, name: string};
- val empty = {chapter = Context.PureN, name = Context.PureN}: T;
+ val empty = {chapter = "Unsorted", name = "Unknown"}: T;
fun extend _ = empty;
fun merge _ = empty;
);
+val _ = Context.>> (Context.map_theory
+ (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}));
+
val session_name = #name o Browser_Info.get;
val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;