# HG changeset patch
# User wenzelm
# Date 1342621456 -7200
# Node ID 3c55bfad22ebdec65f590d8a8b06a9d2f9d25a18
# Parent  2f923e99405666f1e2715aa229bdc458dacfb556
more tight treatment of reset_name;

diff -r 2f923e994056 -r 3c55bfad22eb src/FOL/ROOT
--- a/src/FOL/ROOT	Wed Jul 18 14:07:31 2012 +0200
+++ b/src/FOL/ROOT	Wed Jul 18 16:24:16 2012 +0200
@@ -1,5 +1,4 @@
-session FOL in "." = Pure +
-  name FOL
+session FOL! in "." = Pure +
   description "First-Order Logic with Natural Deduction"
   options [proofs = 2]
   theories FOL
diff -r 2f923e994056 -r 3c55bfad22eb src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Wed Jul 18 14:07:31 2012 +0200
+++ b/src/Pure/System/build.scala	Wed Jul 18 16:24:16 2012 +0200
@@ -73,9 +73,8 @@
   case class Session_Info(
     dir: Path,
     name: String,
-    path: String,
+    reset_name: Boolean,
     parent: String,
-    alt_name: Option[String],
     description: String,
     options: Options,
     theories: List[(Options, String)],
@@ -85,21 +84,19 @@
   {
     val SESSION = "session"
     val IN = "in"
-    val NAME = "name"
     val DESCRIPTION = "description"
     val OPTIONS = "options"
     val THEORIES = "theories"
     val FILES = "files"
 
     val syntax =
-      Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-        SESSION + IN + NAME + DESCRIPTION + OPTIONS + THEORIES + FILES
+      Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+        SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
 
     def session_info(dir: Path): Parser[Session_Info] =
     {
       val session_name = atom("session name", _.is_name)
       val theory_name = atom("theory name", _.is_name)
-      val file_name = atom("file name", _.is_name)
 
       val option =
         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
@@ -111,16 +108,17 @@
           { case _ ~ (x ~ y) => (x, y) }
 
       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
-        (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
+        (keyword("!") ^^^ true | success(false)) ~
+        (opt(keyword(IN) ~! string ^^ { case _ ~ x => Path.explode(x) })) ~
         (keyword("=") ~> session_name <~ keyword("+")) ~
-        (opt(keyword(NAME) ~! session_name ^^ { case _ ~ x => x })) ~
         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
         rep(theories) ~
-        (keyword(FILES) ~! rep1(file_name) ^^ { case _ ~ x => x } | success(Nil)) ^^
+        (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
-            Session_Info(dir, a, b getOrElse a, c, d, e, f,
-              g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, h) }
+              val dir1 = dir + c.getOrElse(Path.basic(a))
+              val thys = g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
+              Session_Info(dir1, a, b, d, e, f, thys, h) }
     }
 
     def parse_entries(dir: Path, root: File): List[Session_Info] =
diff -r 2f923e994056 -r 3c55bfad22eb src/Tools/jEdit/src/modes/isabelle-session.xml
--- a/src/Tools/jEdit/src/modes/isabelle-session.xml	Wed Jul 18 14:07:31 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-session.xml	Wed Jul 18 16:24:16 2012 +0200
@@ -32,7 +32,6 @@
     <KEYWORDS>
       <KEYWORD1>session</KEYWORD1>
       <KEYWORD2>in</KEYWORD2>
-      <KEYWORD2>name</KEYWORD2>
       <KEYWORD2>description</KEYWORD2>
       <KEYWORD2>files</KEYWORD2>
       <KEYWORD2>options</KEYWORD2>
diff -r 2f923e994056 -r 3c55bfad22eb src/ZF/ROOT
--- a/src/ZF/ROOT	Wed Jul 18 14:07:31 2012 +0200
+++ b/src/ZF/ROOT	Wed Jul 18 16:24:16 2012 +0200
@@ -1,5 +1,4 @@
-session ZF in "." = FOL +
-  name ZF
+session ZF! in "." = FOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge