support for 'chapter' specifications within session ROOT;
authorwenzelm
Mon Mar 11 13:28:46 2013 +0100 (2013-03-11)
changeset 5139703b586ee5930
parent 51390 1dff81cf425b
child 51398 c3d02b3518c2
support for 'chapter' specifications within session ROOT;
src/CCL/ROOT
src/CTT/ROOT
src/Cube/ROOT
src/Doc/ROOT
src/FOL/ROOT
src/FOLP/ROOT
src/HOL/ROOT
src/LCF/ROOT
src/Pure/ROOT
src/Pure/Tools/build.scala
src/Sequents/ROOT
src/ZF/ROOT
     1.1 --- a/src/CCL/ROOT	Mon Mar 11 12:27:31 2013 +0100
     1.2 +++ b/src/CCL/ROOT	Mon Mar 11 13:28:46 2013 +0100
     1.3 @@ -1,3 +1,5 @@
     1.4 +chapter CCL
     1.5 +
     1.6  session CCL = Pure +
     1.7    description {*
     1.8      Author:     Martin Coen, Cambridge University Computer Laboratory
     2.1 --- a/src/CTT/ROOT	Mon Mar 11 12:27:31 2013 +0100
     2.2 +++ b/src/CTT/ROOT	Mon Mar 11 13:28:46 2013 +0100
     2.3 @@ -1,3 +1,5 @@
     2.4 +chapter CTT
     2.5 +
     2.6  session CTT = Pure +
     2.7    description {*
     2.8      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.1 --- a/src/Cube/ROOT	Mon Mar 11 12:27:31 2013 +0100
     3.2 +++ b/src/Cube/ROOT	Mon Mar 11 13:28:46 2013 +0100
     3.3 @@ -1,3 +1,5 @@
     3.4 +chapter Cube
     3.5 +
     3.6  session Cube = Pure +
     3.7    description {*
     3.8      Author:     Tobias Nipkow
     4.1 --- a/src/Doc/ROOT	Mon Mar 11 12:27:31 2013 +0100
     4.2 +++ b/src/Doc/ROOT	Mon Mar 11 13:28:46 2013 +0100
     4.3 @@ -1,3 +1,5 @@
     4.4 +chapter Doc
     4.5 +
     4.6  session Classes (doc) in "Classes" = HOL +
     4.7    options [document_variants = "classes"]
     4.8    theories [document = false] Setup
     5.1 --- a/src/FOL/ROOT	Mon Mar 11 12:27:31 2013 +0100
     5.2 +++ b/src/FOL/ROOT	Mon Mar 11 13:28:46 2013 +0100
     5.3 @@ -1,3 +1,5 @@
     5.4 +chapter FOL
     5.5 +
     5.6  session FOL = Pure +
     5.7    description "First-Order Logic with Natural Deduction"
     5.8    options [proofs = 2]
     6.1 --- a/src/FOLP/ROOT	Mon Mar 11 12:27:31 2013 +0100
     6.2 +++ b/src/FOLP/ROOT	Mon Mar 11 13:28:46 2013 +0100
     6.3 @@ -1,3 +1,5 @@
     6.4 +chapter FOLP
     6.5 +
     6.6  session FOLP = Pure +
     6.7    description {*
     6.8      Author:     Martin Coen, Cambridge University Computer Laboratory
     7.1 --- a/src/HOL/ROOT	Mon Mar 11 12:27:31 2013 +0100
     7.2 +++ b/src/HOL/ROOT	Mon Mar 11 13:28:46 2013 +0100
     7.3 @@ -1,3 +1,5 @@
     7.4 +chapter HOL
     7.5 +
     7.6  session HOL (main) = Pure +
     7.7    description {* Classical Higher-order Logic *}
     7.8    options [document_graph]
     8.1 --- a/src/LCF/ROOT	Mon Mar 11 12:27:31 2013 +0100
     8.2 +++ b/src/LCF/ROOT	Mon Mar 11 13:28:46 2013 +0100
     8.3 @@ -1,3 +1,5 @@
     8.4 +chapter LCF
     8.5 +
     8.6  session LCF = Pure +
     8.7    description {*
     8.8      Author:     Tobias Nipkow
     9.1 --- a/src/Pure/ROOT	Mon Mar 11 12:27:31 2013 +0100
     9.2 +++ b/src/Pure/ROOT	Mon Mar 11 13:28:46 2013 +0100
     9.3 @@ -1,3 +1,5 @@
     9.4 +chapter Pure
     9.5 +
     9.6  session RAW =
     9.7    theories
     9.8    files
    10.1 --- a/src/Pure/Tools/build.scala	Mon Mar 11 12:27:31 2013 +0100
    10.2 +++ b/src/Pure/Tools/build.scala	Mon Mar 11 13:28:46 2013 +0100
    10.3 @@ -14,6 +14,7 @@
    10.4  import java.util.zip.GZIPInputStream
    10.5  
    10.6  import scala.collection.SortedSet
    10.7 +import scala.collection.mutable
    10.8  import scala.annotation.tailrec
    10.9  
   10.10  
   10.11 @@ -46,6 +47,8 @@
   10.12    /** session information **/
   10.13  
   10.14    // external version
   10.15 +  abstract class Entry
   10.16 +  sealed case class Chapter(name: String) extends Entry
   10.17    sealed case class Session_Entry(
   10.18      pos: Position.T,
   10.19      name: String,
   10.20 @@ -55,10 +58,11 @@
   10.21      description: String,
   10.22      options: List[Options.Spec],
   10.23      theories: List[(List[Options.Spec], List[String])],
   10.24 -    files: List[String])
   10.25 +    files: List[String]) extends Entry
   10.26  
   10.27    // internal version
   10.28    sealed case class Session_Info(
   10.29 +    chapter: String,
   10.30      select: Boolean,
   10.31      pos: Position.T,
   10.32      groups: List[String],
   10.33 @@ -72,8 +76,8 @@
   10.34  
   10.35    def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
   10.36  
   10.37 -  def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
   10.38 -      : (String, Session_Info) =
   10.39 +  def session_info(options: Options, select: Boolean, dir: Path,
   10.40 +      chapter: String, entry: Session_Entry): (String, Session_Info) =
   10.41      try {
   10.42        val name = entry.name
   10.43  
   10.44 @@ -87,10 +91,11 @@
   10.45          entry.theories.map({ case (opts, thys) =>
   10.46            (session_options ++ opts, thys.map(Path.explode(_))) })
   10.47        val files = entry.files.map(Path.explode(_))
   10.48 -      val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
   10.49 +      val entry_digest =
   10.50 +        SHA1.digest((chapter, name, entry.parent, entry.options, entry.theories).toString)
   10.51  
   10.52        val info =
   10.53 -        Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
   10.54 +        Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
   10.55            entry.parent, entry.description, session_options, theories, files, entry_digest)
   10.56  
   10.57        (name, info)
   10.58 @@ -180,6 +185,9 @@
   10.59  
   10.60    /* parser */
   10.61  
   10.62 +  val chapter_default = "Unsorted"
   10.63 +
   10.64 +  private val CHAPTER = "chapter"
   10.65    private val SESSION = "session"
   10.66    private val IN = "in"
   10.67    private val DESCRIPTION = "description"
   10.68 @@ -189,10 +197,20 @@
   10.69  
   10.70    lazy val root_syntax =
   10.71      Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   10.72 -      (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   10.73 +      (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
   10.74 +      IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   10.75  
   10.76    private object Parser extends Parse.Parser
   10.77    {
   10.78 +    def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos)
   10.79 +
   10.80 +    def chapter(pos: Position.T): Parser[Chapter] =
   10.81 +    {
   10.82 +      val chapter_name = atom("chapter name", _.is_name)
   10.83 +
   10.84 +      command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
   10.85 +    }
   10.86 +
   10.87      def session_entry(pos: Position.T): Parser[Session_Entry] =
   10.88      {
   10.89        val session_name = atom("session name", _.is_name)
   10.90 @@ -219,11 +237,19 @@
   10.91              Session_Entry(pos, a, b, c, d, e, f, g, h) }
   10.92      }
   10.93  
   10.94 -    def parse_entries(root: Path): List[Session_Entry] =
   10.95 +    def parse_entries(root: Path): List[(String, Session_Entry)] =
   10.96      {
   10.97        val toks = root_syntax.scan(File.read(root))
   10.98 -      parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
   10.99 -        case Success(result, _) => result
  10.100 +
  10.101 +      parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match {
  10.102 +        case Success(result, _) =>
  10.103 +          var chapter = chapter_default
  10.104 +          val entries = new mutable.ListBuffer[(String, Session_Entry)]
  10.105 +          result.foreach {
  10.106 +            case Chapter(name) => chapter = name
  10.107 +            case session_entry: Session_Entry => entries += ((chapter, session_entry))
  10.108 +          }
  10.109 +          entries.toList
  10.110          case bad => error(bad.toString)
  10.111        }
  10.112      }
  10.113 @@ -250,7 +276,8 @@
  10.114      def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
  10.115      {
  10.116        val root = dir + ROOT
  10.117 -      if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
  10.118 +      if (root.is_file)
  10.119 +        Parser.parse_entries(root).map(p => session_info(options, select, dir, p._1, p._2))
  10.120        else Nil
  10.121      }
  10.122  
  10.123 @@ -398,7 +425,7 @@
  10.124              val groups =
  10.125                if (info.groups.isEmpty) ""
  10.126                else info.groups.mkString(" (", " ", ")")
  10.127 -            progress.echo("Session " + name + groups)
  10.128 +            progress.echo("Session " + info.chapter + "/" + name + groups)
  10.129            }
  10.130  
  10.131            val thy_deps =
    11.1 --- a/src/Sequents/ROOT	Mon Mar 11 12:27:31 2013 +0100
    11.2 +++ b/src/Sequents/ROOT	Mon Mar 11 13:28:46 2013 +0100
    11.3 @@ -1,3 +1,5 @@
    11.4 +chapter Sequents
    11.5 +
    11.6  session Sequents = Pure +
    11.7    description {*
    11.8      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.1 --- a/src/ZF/ROOT	Mon Mar 11 12:27:31 2013 +0100
    12.2 +++ b/src/ZF/ROOT	Mon Mar 11 13:28:46 2013 +0100
    12.3 @@ -1,3 +1,5 @@
    12.4 +chapter ZF
    12.5 +
    12.6  session ZF (main) = Pure +
    12.7    description {*
    12.8      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory