clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
authorwenzelm
Tue Jul 24 10:58:43 2012 +0200 (2012-07-24)
changeset 48462424fd5364f15
parent 48461 96c1ef26aabe
child 48463 07f752935ece
clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
src/Pure/System/build.ML
src/Pure/System/build.scala
src/ZF/ROOT
src/ZF/ZF.thy
     1.1 --- a/src/Pure/System/build.ML	Tue Jul 24 10:44:36 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 10:58:43 2012 +0200
     1.3 @@ -35,15 +35,12 @@
     1.4          end;
     1.5  
     1.6      val _ =
     1.7 -      Session.init
     1.8 -        save
     1.9 -        false (* FIXME reset!? *)
    1.10 +      Session.init save false
    1.11          (Options.bool options "browser_info") browser_info
    1.12          (Options.string options "document")
    1.13          (Options.bool options "document_graph")
    1.14          (space_explode "," (Options.string options "document_variants"))
    1.15 -        parent
    1.16 -        base_name
    1.17 +        parent base_name
    1.18          (true (* FIXME copy document/ files on Scala side!? *),
    1.19            Options.string options "document_dump")
    1.20          ""
     2.1 --- a/src/Pure/System/build.scala	Tue Jul 24 10:44:36 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Tue Jul 24 10:58:43 2012 +0200
     2.3 @@ -116,7 +116,7 @@
     2.4  
     2.5    private case class Session_Entry(
     2.6      name: String,
     2.7 -    reset: Boolean,
     2.8 +    this_name: Boolean,
     2.9      order: Int,
    2.10      path: Option[String],
    2.11      parent: Option[String],
    2.12 @@ -196,7 +196,7 @@
    2.13            else
    2.14              entry.parent match {
    2.15                case Some(parent_name) if queue1.defined(parent_name) =>
    2.16 -                if (entry.reset) entry.name
    2.17 +                if (entry.this_name) entry.name
    2.18                  else parent_name + "-" + entry.name
    2.19                case _ => error("Bad parent session")
    2.20              }
     3.1 --- a/src/ZF/ROOT	Tue Jul 24 10:44:36 2012 +0200
     3.2 +++ b/src/ZF/ROOT	Tue Jul 24 10:58:43 2012 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -session ZF! (10) in "." = FOL +
     3.5 +session ZF! (10) in "." = Pure +
     3.6    description {*
     3.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8      Copyright   1995  University of Cambridge
     4.1 --- a/src/ZF/ZF.thy	Tue Jul 24 10:44:36 2012 +0200
     4.2 +++ b/src/ZF/ZF.thy	Tue Jul 24 10:58:43 2012 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header{*Zermelo-Fraenkel Set Theory*}
     4.5  
     4.6  theory ZF
     4.7 -imports FOL
     4.8 +imports "~~/src/FOL/FOL"
     4.9  begin
    4.10  
    4.11  declare [[eta_contract = false]]