more tight treatment of reset_name;
authorwenzelm
Wed Jul 18 16:24:16 2012 +0200 (2012-07-18)
changeset 483363c55bfad22eb
parent 48335 2f923e994056
child 48337 9c7f8e5805b4
more tight treatment of reset_name;
src/FOL/ROOT
src/Pure/System/build.scala
src/Tools/jEdit/src/modes/isabelle-session.xml
src/ZF/ROOT
     1.1 --- a/src/FOL/ROOT	Wed Jul 18 14:07:31 2012 +0200
     1.2 +++ b/src/FOL/ROOT	Wed Jul 18 16:24:16 2012 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4 -session FOL in "." = Pure +
     1.5 -  name FOL
     1.6 +session FOL! in "." = Pure +
     1.7    description "First-Order Logic with Natural Deduction"
     1.8    options [proofs = 2]
     1.9    theories FOL
     2.1 --- a/src/Pure/System/build.scala	Wed Jul 18 14:07:31 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Wed Jul 18 16:24:16 2012 +0200
     2.3 @@ -73,9 +73,8 @@
     2.4    case class Session_Info(
     2.5      dir: Path,
     2.6      name: String,
     2.7 -    path: String,
     2.8 +    reset_name: Boolean,
     2.9      parent: String,
    2.10 -    alt_name: Option[String],
    2.11      description: String,
    2.12      options: Options,
    2.13      theories: List[(Options, String)],
    2.14 @@ -85,21 +84,19 @@
    2.15    {
    2.16      val SESSION = "session"
    2.17      val IN = "in"
    2.18 -    val NAME = "name"
    2.19      val DESCRIPTION = "description"
    2.20      val OPTIONS = "options"
    2.21      val THEORIES = "theories"
    2.22      val FILES = "files"
    2.23  
    2.24      val syntax =
    2.25 -      Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    2.26 -        SESSION + IN + NAME + DESCRIPTION + OPTIONS + THEORIES + FILES
    2.27 +      Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    2.28 +        SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
    2.29  
    2.30      def session_info(dir: Path): Parser[Session_Info] =
    2.31      {
    2.32        val session_name = atom("session name", _.is_name)
    2.33        val theory_name = atom("theory name", _.is_name)
    2.34 -      val file_name = atom("file name", _.is_name)
    2.35  
    2.36        val option =
    2.37          name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
    2.38 @@ -111,16 +108,17 @@
    2.39            { case _ ~ (x ~ y) => (x, y) }
    2.40  
    2.41        ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
    2.42 -        (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
    2.43 +        (keyword("!") ^^^ true | success(false)) ~
    2.44 +        (opt(keyword(IN) ~! string ^^ { case _ ~ x => Path.explode(x) })) ~
    2.45          (keyword("=") ~> session_name <~ keyword("+")) ~
    2.46 -        (opt(keyword(NAME) ~! session_name ^^ { case _ ~ x => x })) ~
    2.47          (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
    2.48          (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
    2.49          rep(theories) ~
    2.50 -        (keyword(FILES) ~! rep1(file_name) ^^ { case _ ~ x => x } | success(Nil)) ^^
    2.51 +        (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
    2.52            { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
    2.53 -            Session_Info(dir, a, b getOrElse a, c, d, e, f,
    2.54 -              g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, h) }
    2.55 +              val dir1 = dir + c.getOrElse(Path.basic(a))
    2.56 +              val thys = g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
    2.57 +              Session_Info(dir1, a, b, d, e, f, thys, h) }
    2.58      }
    2.59  
    2.60      def parse_entries(dir: Path, root: File): List[Session_Info] =
     3.1 --- a/src/Tools/jEdit/src/modes/isabelle-session.xml	Wed Jul 18 14:07:31 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/modes/isabelle-session.xml	Wed Jul 18 16:24:16 2012 +0200
     3.3 @@ -32,7 +32,6 @@
     3.4      <KEYWORDS>
     3.5        <KEYWORD1>session</KEYWORD1>
     3.6        <KEYWORD2>in</KEYWORD2>
     3.7 -      <KEYWORD2>name</KEYWORD2>
     3.8        <KEYWORD2>description</KEYWORD2>
     3.9        <KEYWORD2>files</KEYWORD2>
    3.10        <KEYWORD2>options</KEYWORD2>
     4.1 --- a/src/ZF/ROOT	Wed Jul 18 14:07:31 2012 +0200
     4.2 +++ b/src/ZF/ROOT	Wed Jul 18 16:24:16 2012 +0200
     4.3 @@ -1,5 +1,4 @@
     4.4 -session ZF in "." = FOL +
     4.5 -  name ZF
     4.6 +session ZF! in "." = FOL +
     4.7    description {*
     4.8      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.9      Copyright   1995  University of Cambridge