# HG changeset patch
# User wenzelm
# Date 1343120323 -7200
# Node ID 424fd5364f1597ecb4c1ab3ba334cf576a6bf8cf
# Parent  96c1ef26aabec2b24553f60303778c9b611400d3
clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;

diff -r 96c1ef26aabe -r 424fd5364f15 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Tue Jul 24 10:44:36 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 10:58:43 2012 +0200
@@ -35,15 +35,12 @@
         end;
 
     val _ =
-      Session.init
-        save
-        false (* FIXME reset!? *)
+      Session.init save false
         (Options.bool options "browser_info") browser_info
         (Options.string options "document")
         (Options.bool options "document_graph")
         (space_explode "," (Options.string options "document_variants"))
-        parent
-        base_name
+        parent base_name
         (true (* FIXME copy document/ files on Scala side!? *),
           Options.string options "document_dump")
         ""
diff -r 96c1ef26aabe -r 424fd5364f15 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Jul 24 10:44:36 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Jul 24 10:58:43 2012 +0200
@@ -116,7 +116,7 @@
 
   private case class Session_Entry(
     name: String,
-    reset: Boolean,
+    this_name: Boolean,
     order: Int,
     path: Option[String],
     parent: Option[String],
@@ -196,7 +196,7 @@
           else
             entry.parent match {
               case Some(parent_name) if queue1.defined(parent_name) =>
-                if (entry.reset) entry.name
+                if (entry.this_name) entry.name
                 else parent_name + "-" + entry.name
               case _ => error("Bad parent session")
             }
diff -r 96c1ef26aabe -r 424fd5364f15 src/ZF/ROOT
--- a/src/ZF/ROOT	Tue Jul 24 10:44:36 2012 +0200
+++ b/src/ZF/ROOT	Tue Jul 24 10:58:43 2012 +0200
@@ -1,4 +1,4 @@
-session ZF! (10) in "." = FOL +
+session ZF! (10) in "." = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
diff -r 96c1ef26aabe -r 424fd5364f15 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue Jul 24 10:44:36 2012 +0200
+++ b/src/ZF/ZF.thy	Tue Jul 24 10:58:43 2012 +0200
@@ -6,7 +6,7 @@
 header{*Zermelo-Fraenkel Set Theory*}
 
 theory ZF
-imports FOL
+imports "~~/src/FOL/FOL"
 begin
 
 declare [[eta_contract = false]]