--- 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
--- 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
--- 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
--- 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
--- 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]
--- 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
--- 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]
--- 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
--- 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
--- 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 =
--- 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
--- 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