# HG changeset patch
# User wenzelm
# Date 1342700680 -7200
# Node ID a78e5d3995993cca9dbff9cba1b2d2ef950aebb7
# Parent  cbb25adad26ff9d6b976e1053fa98a738c19aac6
support Session.Queue with ordering and dependencies;

diff -r cbb25adad26f -r a78e5d399599 src/FOL/ROOT
--- a/src/FOL/ROOT	Thu Jul 19 14:15:08 2012 +0200
+++ b/src/FOL/ROOT	Thu Jul 19 14:24:40 2012 +0200
@@ -1,4 +1,4 @@
-session FOL! in "." = Pure +
+session FOL! (10) in "." = Pure +
   description "First-Order Logic with Natural Deduction"
   options [proofs = 2]
   theories FOL
diff -r cbb25adad26f -r a78e5d399599 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Jul 19 14:15:08 2012 +0200
+++ b/src/HOL/ROOT	Thu Jul 19 14:24:40 2012 +0200
@@ -1,4 +1,4 @@
-session HOL! in "." = Pure +
+session HOL! (1) in "." = Pure +
   description {* Classical Higher-order Logic *}
   options [document_graph]
   theories Complex_Main
@@ -19,12 +19,12 @@
   options [document = false]
   theories Main
 
-session "HOL-Proofs"! in "." = Pure +
+session "HOL-Proofs"! (2) in "." = Pure +
   description {* HOL-Main with proof terms *}
   options [document = false, proofs = 2, parallel_proofs = false]
   theories Main
 
-session HOLCF! = HOL +
+session HOLCF! (3) = HOL +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman
diff -r cbb25adad26f -r a78e5d399599 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Thu Jul 19 14:15:08 2012 +0200
+++ b/src/Pure/Isar/parse.scala	Thu Jul 19 14:24:40 2012 +0200
@@ -54,6 +54,7 @@
         tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
 
     def string: Parser[String] = atom("string", _.is_string)
+    def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
     def name: Parser[String] = atom("name declaration", _.is_name)
     def xname: Parser[String] = atom("name reference", _.is_xname)
     def text: Parser[String] = atom("text", _.is_text)
diff -r cbb25adad26f -r a78e5d399599 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Thu Jul 19 14:15:08 2012 +0200
+++ b/src/Pure/Isar/token.scala	Thu Jul 19 14:24:40 2012 +0200
@@ -74,6 +74,7 @@
     kind == Token.Kind.VERBATIM ||
     kind == Token.Kind.COMMENT
   def is_string: Boolean = kind == Token.Kind.STRING
+  def is_nat: Boolean = kind == Token.Kind.NAT
   def is_name: Boolean =
     kind == Token.Kind.IDENT ||
     kind == Token.Kind.SYM_IDENT ||
diff -r cbb25adad26f -r a78e5d399599 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Jul 19 14:15:08 2012 +0200
+++ b/src/Pure/System/build.scala	Thu Jul 19 14:24:40 2012 +0200
@@ -19,14 +19,73 @@
 
   type Options = List[(String, Option[String])]
 
-  case class Session_Info(
-    dir: Path,
-    name: String,
-    parent: Option[String],
-    description: String,
-    options: Options,
-    theories: List[(Options, String)],
-    files: List[String])
+  object Session
+  {
+    object Key
+    {
+      object Ordering extends scala.math.Ordering[Key]
+      {
+        def compare(key1: Key, key2: Key): Int =
+          key2.order compare key1.order match {
+            case 0 => key1.name compare key2.name
+            case ord => ord
+          }
+      }
+    }
+
+    sealed case class Key(name: String, order: Int)
+    {
+      override def toString: String = name
+    }
+
+    sealed case class Info(
+      dir: Path,
+      key: Key,
+      parent: Option[String],
+      description: String,
+      options: Options,
+      theories: List[(Options, String)],
+      files: List[String])
+    {
+      def name: String = key.name
+    }
+
+    object Queue
+    {
+      val empty: Queue = new Queue()
+    }
+
+    final class Queue private(
+      keys: Map[String, Key] = Map.empty,
+      graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
+    {
+      def lookup(name: String): Option[Info] =
+        keys.get(name).map(graph.get_node(_))
+
+      def + (info: Info): Queue =
+      {
+        val keys1 =
+          if (keys.isDefinedAt(info.name)) error("Duplicate session: " + quote(info.name))
+          else keys + (info.name -> info.key)
+
+        val graph1 =
+          try {
+            graph.new_node(info.key, info).
+              add_deps_acyclic(info.key, info.parent.toList.map(keys(_)))
+          }
+          catch {
+            case exn: Graph.Cycles[_] =>
+              error(cat_lines(exn.cycles.map(cycle =>
+                "Cyclic session dependency of " +
+                  cycle.map(key => quote(key.toString)).mkString(" via "))))
+          }
+        new Queue(keys1, graph1)
+      }
+
+      def topological_order: List[Info] =
+        graph.topological_order.map(graph.get_node(_))
+    }
+  }
 
 
   /* parsing */
@@ -36,6 +95,7 @@
   private case class Session_Entry(
     name: String,
     reset: Boolean,
+    order: Int,
     path: Option[String],
     parent: Option[String],
     description: String,
@@ -71,13 +131,14 @@
 
       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
         (keyword("!") ^^^ true | success(false)) ~
+        (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
         (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
         rep(theories) ~
         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
-          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
+          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
     }
 
     def parse_entries(root: File): List[Session_Entry] =
@@ -93,9 +154,9 @@
 
   /* find sessions */
 
-  def find_sessions(more_dirs: List[Path]): List[Session_Info] =
+  def find_sessions(more_dirs: List[Path]): Session.Queue =
   {
-    val infos = new mutable.ListBuffer[Session_Info]
+    var sessions = Session.Queue.empty
 
     for {
       (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true))
@@ -118,8 +179,8 @@
               case None => error("Missing parent session")
               case Some(parent) =>
                 val parent_info =
-                  infos.find(_.name == parent) getOrElse
-                   error("Undefined parent session: " + quote(parent))
+                  sessions.lookup(parent) getOrElse
+                    error("Undefined parent session: " + quote(parent))
                 if (entry.reset) entry.name
                 else parent_info.name + "-" + entry.name
             }
@@ -131,12 +192,10 @@
           }
         val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
         val info =
-          Session_Info(dir + path, full_name, entry.parent, entry.description,
-            entry.options, thys, entry.files)
+          Session.Info(dir + path, Session.Key(full_name, entry.order),
+            entry.parent, entry.description, entry.options, thys, entry.files)
 
-        if (infos.exists(_.name == full_name))
-          error("Duplicate session: " + quote(full_name))
-        infos += info
+        sessions += info
       }
       catch {
         case ERROR(msg) =>
@@ -144,7 +203,7 @@
             quote(entry.name) + " (file " + quote(root.toString) + ")")
       }
     }
-    infos.toList
+    sessions
   }
 
 
@@ -158,7 +217,8 @@
     println("options = " + options.toString)
     println("sessions = " + sessions.toString)
 
-    find_sessions(more_dirs) foreach println
+    for (info <- find_sessions(more_dirs).topological_order)
+      println(info.name + " in " + info.dir)
 
     0
   }
diff -r cbb25adad26f -r a78e5d399599 src/ZF/ROOT
--- a/src/ZF/ROOT	Thu Jul 19 14:15:08 2012 +0200
+++ b/src/ZF/ROOT	Thu Jul 19 14:24:40 2012 +0200
@@ -1,4 +1,4 @@
-session ZF! in "." = FOL +
+session ZF! (10) in "." = FOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge