1.1 --- a/src/FOL/ROOT	Thu Jul 19 14:15:08 2012 +0200
     1.2 +++ b/src/FOL/ROOT	Thu Jul 19 14:24:40 2012 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -session FOL! in "." = Pure +
     1.5 +session FOL! (10) in "." = Pure +
     1.6    description "First-Order Logic with Natural Deduction"
     1.7    options [proofs = 2]
     1.8    theories FOL

     2.1 --- a/src/HOL/ROOT	Thu Jul 19 14:15:08 2012 +0200
     2.2 +++ b/src/HOL/ROOT	Thu Jul 19 14:24:40 2012 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -session HOL! in "." = Pure +
     2.5 +session HOL! (1) in "." = Pure +
     2.6    description {* Classical Higher-order Logic *}
     2.7    options [document_graph]
     2.8    theories Complex_Main
     2.9 @@ -19,12 +19,12 @@
    2.10    options [document = false]
    2.11    theories Main
    2.12  
    2.13 -session "HOL-Proofs"! in "." = Pure +
    2.14 +session "HOL-Proofs"! (2) in "." = Pure +
    2.15    description {* HOL-Main with proof terms *}
    2.16    options [document = false, proofs = 2, parallel_proofs = false]
    2.17    theories Main
    2.18  
    2.19 -session HOLCF! = HOL +
    2.20 +session HOLCF! (3) = HOL +
    2.21    description {*
    2.22      Author:     Franz Regensburger
    2.23      Author:     Brian Huffman

     3.1 --- a/src/Pure/Isar/parse.scala	Thu Jul 19 14:15:08 2012 +0200
     3.2 +++ b/src/Pure/Isar/parse.scala	Thu Jul 19 14:24:40 2012 +0200
     3.3 @@ -54,6 +54,7 @@
     3.4          tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
     3.5  
     3.6      def string: Parser[String] = atom("string", _.is_string)
     3.7 +    def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
     3.8      def name: Parser[String] = atom("name declaration", _.is_name)
     3.9      def xname: Parser[String] = atom("name reference", _.is_xname)
    3.10      def text: Parser[String] = atom("text", _.is_text)

     4.1 --- a/src/Pure/Isar/token.scala	Thu Jul 19 14:15:08 2012 +0200
     4.2 +++ b/src/Pure/Isar/token.scala	Thu Jul 19 14:24:40 2012 +0200
     4.3 @@ -74,6 +74,7 @@
     4.4      kind == Token.Kind.VERBATIM ||
     4.5      kind == Token.Kind.COMMENT
     4.6    def is_string: Boolean = kind == Token.Kind.STRING
     4.7 +  def is_nat: Boolean = kind == Token.Kind.NAT
     4.8    def is_name: Boolean =
     4.9      kind == Token.Kind.IDENT ||
    4.10      kind == Token.Kind.SYM_IDENT ||

     5.1 --- a/src/Pure/System/build.scala	Thu Jul 19 14:15:08 2012 +0200
     5.2 +++ b/src/Pure/System/build.scala	Thu Jul 19 14:24:40 2012 +0200
     5.3 @@ -19,14 +19,73 @@
     5.4  
     5.5    type Options = List[(String, Option[String])]
     5.6  
     5.7 -  case class Session_Info(
     5.8 -    dir: Path,
     5.9 -    name: String,
    5.10 -    parent: Option[String],
    5.11 -    description: String,
    5.12 -    options: Options,
    5.13 -    theories: List[(Options, String)],
    5.14 -    files: List[String])
    5.15 +  object Session
    5.16 +  {
    5.17 +    object Key
    5.18 +    {
    5.19 +      object Ordering extends scala.math.Ordering[Key]
    5.20 +      {
    5.21 +        def compare(key1: Key, key2: Key): Int =
    5.22 +          key2.order compare key1.order match {
    5.23 +            case 0 => key1.name compare key2.name
    5.24 +            case ord => ord
    5.25 +          }
    5.26 +      }
    5.27 +    }
    5.28 +
    5.29 +    sealed case class Key(name: String, order: Int)
    5.30 +    {
    5.31 +      override def toString: String = name
    5.32 +    }
    5.33 +
    5.34 +    sealed case class Info(
    5.35 +      dir: Path,
    5.36 +      key: Key,
    5.37 +      parent: Option[String],
    5.38 +      description: String,
    5.39 +      options: Options,
    5.40 +      theories: List[(Options, String)],
    5.41 +      files: List[String])
    5.42 +    {
    5.43 +      def name: String = key.name
    5.44 +    }
    5.45 +
    5.46 +    object Queue
    5.47 +    {
    5.48 +      val empty: Queue = new Queue()
    5.49 +    }
    5.50 +
    5.51 +    final class Queue private(
    5.52 +      keys: Map[String, Key] = Map.empty,
    5.53 +      graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
    5.54 +    {
    5.55 +      def lookup(name: String): Option[Info] =
    5.56 +        keys.get(name).map(graph.get_node(_))
    5.57 +
    5.58 +      def + (info: Info): Queue =
    5.59 +      {
    5.60 +        val keys1 =
    5.61 +          if (keys.isDefinedAt(info.name)) error("Duplicate session: " + quote(info.name))
    5.62 +          else keys + (info.name -> info.key)
    5.63 +
    5.64 +        val graph1 =
    5.65 +          try {
    5.66 +            graph.new_node(info.key, info).
    5.67 +              add_deps_acyclic(info.key, info.parent.toList.map(keys(_)))
    5.68 +          }
    5.69 +          catch {
    5.70 +            case exn: Graph.Cycles[_] =>
    5.71 +              error(cat_lines(exn.cycles.map(cycle =>
    5.72 +                "Cyclic session dependency of " +
    5.73 +                  cycle.map(key => quote(key.toString)).mkString(" via "))))
    5.74 +          }
    5.75 +        new Queue(keys1, graph1)
    5.76 +      }
    5.77 +
    5.78 +      def topological_order: List[Info] =
    5.79 +        graph.topological_order.map(graph.get_node(_))
    5.80 +    }
    5.81 +  }
    5.82  
    5.83  
    5.84    /* parsing */
    5.85 @@ -36,6 +95,7 @@
    5.86    private case class Session_Entry(
    5.87      name: String,
    5.88      reset: Boolean,
    5.89 +    order: Int,
    5.90      path: Option[String],
    5.91      parent: Option[String],
    5.92      description: String,
    5.93 @@ -71,13 +131,14 @@
    5.94  
    5.95        ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
    5.96          (keyword("!") ^^^ true | success(false)) ~
    5.97 +        (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
    5.98          (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
    5.99          (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
   5.100          (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
   5.101          (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
   5.102          rep(theories) ~
   5.103          (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   5.104 -          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
   5.105 +          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
   5.106      }
   5.107  
   5.108      def parse_entries(root: File): List[Session_Entry] =
   5.109 @@ -93,9 +154,9 @@
   5.110  
   5.111    /* find sessions */
   5.112  
   5.113 -  def find_sessions(more_dirs: List[Path]): List[Session_Info] =
   5.114 +  def find_sessions(more_dirs: List[Path]): Session.Queue =
   5.115    {
   5.116 -    val infos = new mutable.ListBuffer[Session_Info]
   5.117 +    var sessions = Session.Queue.empty
   5.118  
   5.119      for {
   5.120        (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true))
   5.121 @@ -118,8 +179,8 @@
   5.122                case None => error("Missing parent session")
   5.123                case Some(parent) =>
   5.124                  val parent_info =
   5.125 -                  infos.find(_.name == parent) getOrElse
   5.126 -                   error("Undefined parent session: " + quote(parent))
   5.127 +                  sessions.lookup(parent) getOrElse
   5.128 +                    error("Undefined parent session: " + quote(parent))
   5.129                  if (entry.reset) entry.name
   5.130                  else parent_info.name + "-" + entry.name
   5.131              }
   5.132 @@ -131,12 +192,10 @@
   5.133            }
   5.134          val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
   5.135          val info =
   5.136 -          Session_Info(dir + path, full_name, entry.parent, entry.description,
   5.137 -            entry.options, thys, entry.files)
   5.138 +          Session.Info(dir + path, Session.Key(full_name, entry.order),
   5.139 +            entry.parent, entry.description, entry.options, thys, entry.files)
   5.140  
   5.141 -        if (infos.exists(_.name == full_name))
   5.142 -          error("Duplicate session: " + quote(full_name))
   5.143 -        infos += info
   5.144 +        sessions += info
   5.145        }
   5.146        catch {
   5.147          case ERROR(msg) =>
   5.148 @@ -144,7 +203,7 @@
   5.149              quote(entry.name) + " (file " + quote(root.toString) + ")")
   5.150        }
   5.151      }
   5.152 -    infos.toList
   5.153 +    sessions
   5.154    }
   5.155  
   5.156  
   5.157 @@ -158,7 +217,8 @@
   5.158      println("options = " + options.toString)
   5.159      println("sessions = " + sessions.toString)
   5.160  
   5.161 -    find_sessions(more_dirs) foreach println
   5.162 +    for (info <- find_sessions(more_dirs).topological_order)
   5.163 +      println(info.name + " in " + info.dir)
   5.164  
   5.165      0
   5.166    }

     6.1 --- a/src/ZF/ROOT	Thu Jul 19 14:15:08 2012 +0200
     6.2 +++ b/src/ZF/ROOT	Thu Jul 19 14:24:40 2012 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -session ZF! in "." = FOL +
     6.5 +session ZF! (10) in "." = FOL +
     6.6    description {*
     6.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8      Copyright   1995  University of Cambridge