immediate access to some elementary examples;
authorwenzelm
Sat Sep 21 19:48:46 2013 +0200 (2013-09-21)
changeset 5377706a6216f733e
parent 53776 3806bf1d2a33
child 53778 29eaacff4078
immediate access to some elementary examples;
src/Pure/Tools/doc.scala
     1.1 --- a/src/Pure/Tools/doc.scala	Sat Sep 21 17:37:02 2013 +0200
     1.2 +++ b/src/Pure/Tools/doc.scala	Sat Sep 21 19:48:46 2013 +0200
     1.3 @@ -35,17 +35,18 @@
     1.4    case class Doc(name: String, title: String) extends Entry
     1.5    case class Text_File(name: String, path: Path) extends Entry
     1.6  
     1.7 +  def text_file(name: String): Option[Text_File] =
     1.8 +  {
     1.9 +    val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
    1.10 +    if (path.is_file) Some(Text_File(name, path))
    1.11 +    else None
    1.12 +  }
    1.13 +
    1.14    private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    1.15    private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    1.16  
    1.17    private def release_notes(): List[Entry] =
    1.18    {
    1.19 -    def text_file(name: String): Option[Text_File] =
    1.20 -    {
    1.21 -      val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
    1.22 -      if (path.is_file) Some(Text_File(name, path))
    1.23 -      else None
    1.24 -    }
    1.25      val names =
    1.26        List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
    1.27          "contrib/README", "README_REPOSITORY")
    1.28 @@ -53,6 +54,16 @@
    1.29        (for (name <- names; entry <- text_file(name)) yield entry)
    1.30    }
    1.31  
    1.32 +  private def examples(): List[Entry] =
    1.33 +  {
    1.34 +    val names =
    1.35 +      List(
    1.36 +        "src/HOL/ex/Seq.thy",
    1.37 +        "src/HOL/Unix/Unix.thy",
    1.38 +        "src/HOL/Isar_Examples/Drinker.thy")
    1.39 +    Section("Examples") :: names.map(name => text_file(name).get)
    1.40 +  }
    1.41 +
    1.42    def contents(): List[Entry] =
    1.43      (for {
    1.44        line <- contents_lines()
    1.45 @@ -62,7 +73,7 @@
    1.46            case Doc_Entry(name, title) => Some(Doc(name, title))
    1.47            case _ => None
    1.48          }
    1.49 -    } yield entry) ::: release_notes()
    1.50 +    } yield entry) ::: release_notes() ::: examples()
    1.51  
    1.52  
    1.53    /* view */