# HG changeset patch
# User wenzelm
# Date 1363004926 -3600
# Node ID 03b586ee5930d726ddb2b5af0b5670bbe58267cb
# Parent  1dff81cf425bdd17499e4e98dc510a2b96528426
support for 'chapter' specifications within session ROOT;

diff -r 1dff81cf425b -r 03b586ee5930 src/CCL/ROOT
--- a/src/CCL/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/CCL/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter CCL
+
 session CCL = Pure +
   description {*
     Author:     Martin Coen, Cambridge University Computer Laboratory
diff -r 1dff81cf425b -r 03b586ee5930 src/CTT/ROOT
--- a/src/CTT/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/CTT/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter CTT
+
 session CTT = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
diff -r 1dff81cf425b -r 03b586ee5930 src/Cube/ROOT
--- a/src/Cube/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/Cube/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter Cube
+
 session Cube = Pure +
   description {*
     Author:     Tobias Nipkow
diff -r 1dff81cf425b -r 03b586ee5930 src/Doc/ROOT
--- a/src/Doc/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/Doc/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter Doc
+
 session Classes (doc) in "Classes" = HOL +
   options [document_variants = "classes"]
   theories [document = false] Setup
diff -r 1dff81cf425b -r 03b586ee5930 src/FOL/ROOT
--- a/src/FOL/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/FOL/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter FOL
+
 session FOL = Pure +
   description "First-Order Logic with Natural Deduction"
   options [proofs = 2]
diff -r 1dff81cf425b -r 03b586ee5930 src/FOLP/ROOT
--- a/src/FOLP/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/FOLP/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter FOLP
+
 session FOLP = Pure +
   description {*
     Author:     Martin Coen, Cambridge University Computer Laboratory
diff -r 1dff81cf425b -r 03b586ee5930 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/HOL/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter HOL
+
 session HOL (main) = Pure +
   description {* Classical Higher-order Logic *}
   options [document_graph]
diff -r 1dff81cf425b -r 03b586ee5930 src/LCF/ROOT
--- a/src/LCF/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/LCF/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter LCF
+
 session LCF = Pure +
   description {*
     Author:     Tobias Nipkow
diff -r 1dff81cf425b -r 03b586ee5930 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/Pure/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter Pure
+
 session RAW =
   theories
   files
diff -r 1dff81cf425b -r 03b586ee5930 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/Pure/Tools/build.scala	Mon Mar 11 13:28:46 2013 +0100
@@ -14,6 +14,7 @@
 import java.util.zip.GZIPInputStream
 
 import scala.collection.SortedSet
+import scala.collection.mutable
 import scala.annotation.tailrec
 
 
@@ -46,6 +47,8 @@
   /** session information **/
 
   // external version
+  abstract class Entry
+  sealed case class Chapter(name: String) extends Entry
   sealed case class Session_Entry(
     pos: Position.T,
     name: String,
@@ -55,10 +58,11 @@
     description: String,
     options: List[Options.Spec],
     theories: List[(List[Options.Spec], List[String])],
-    files: List[String])
+    files: List[String]) extends Entry
 
   // internal version
   sealed case class Session_Info(
+    chapter: String,
     select: Boolean,
     pos: Position.T,
     groups: List[String],
@@ -72,8 +76,8 @@
 
   def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
 
-  def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
-      : (String, Session_Info) =
+  def session_info(options: Options, select: Boolean, dir: Path,
+      chapter: String, entry: Session_Entry): (String, Session_Info) =
     try {
       val name = entry.name
 
@@ -87,10 +91,11 @@
         entry.theories.map({ case (opts, thys) =>
           (session_options ++ opts, thys.map(Path.explode(_))) })
       val files = entry.files.map(Path.explode(_))
-      val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
+      val entry_digest =
+        SHA1.digest((chapter, name, entry.parent, entry.options, entry.theories).toString)
 
       val info =
-        Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
+        Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
           entry.parent, entry.description, session_options, theories, files, entry_digest)
 
       (name, info)
@@ -180,6 +185,9 @@
 
   /* parser */
 
+  val chapter_default = "Unsorted"
+
+  private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
   private val DESCRIPTION = "description"
@@ -189,10 +197,20 @@
 
   lazy val root_syntax =
     Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-      (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
+      (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
+      IN + DESCRIPTION + OPTIONS + THEORIES + FILES
 
   private object Parser extends Parse.Parser
   {
+    def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos)
+
+    def chapter(pos: Position.T): Parser[Chapter] =
+    {
+      val chapter_name = atom("chapter name", _.is_name)
+
+      command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
+    }
+
     def session_entry(pos: Position.T): Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
@@ -219,11 +237,19 @@
             Session_Entry(pos, a, b, c, d, e, f, g, h) }
     }
 
-    def parse_entries(root: Path): List[Session_Entry] =
+    def parse_entries(root: Path): List[(String, Session_Entry)] =
     {
       val toks = root_syntax.scan(File.read(root))
-      parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
-        case Success(result, _) => result
+
+      parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match {
+        case Success(result, _) =>
+          var chapter = chapter_default
+          val entries = new mutable.ListBuffer[(String, Session_Entry)]
+          result.foreach {
+            case Chapter(name) => chapter = name
+            case session_entry: Session_Entry => entries += ((chapter, session_entry))
+          }
+          entries.toList
         case bad => error(bad.toString)
       }
     }
@@ -250,7 +276,8 @@
     def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
     {
       val root = dir + ROOT
-      if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
+      if (root.is_file)
+        Parser.parse_entries(root).map(p => session_info(options, select, dir, p._1, p._2))
       else Nil
     }
 
@@ -398,7 +425,7 @@
             val groups =
               if (info.groups.isEmpty) ""
               else info.groups.mkString(" (", " ", ")")
-            progress.echo("Session " + name + groups)
+            progress.echo("Session " + info.chapter + "/" + name + groups)
           }
 
           val thy_deps =
diff -r 1dff81cf425b -r 03b586ee5930 src/Sequents/ROOT
--- a/src/Sequents/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/Sequents/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter Sequents
+
 session Sequents = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
diff -r 1dff81cf425b -r 03b586ee5930 src/ZF/ROOT
--- a/src/ZF/ROOT	Mon Mar 11 12:27:31 2013 +0100
+++ b/src/ZF/ROOT	Mon Mar 11 13:28:46 2013 +0100
@@ -1,3 +1,5 @@
+chapter ZF
+
 session ZF (main) = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory