src/Pure/Tools/doc.scala
changeset 56425 d12653fbd5b1
parent 56424 7032378cc097
child 56631 89269bb8e7ca
     1.1 --- a/src/Pure/Tools/doc.scala	Sat Apr 05 19:07:05 2014 +0200
     1.2 +++ b/src/Pure/Tools/doc.scala	Sat Apr 05 19:16:16 2014 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4        Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
     1.5          text_file(file) match {
     1.6            case Some(entry) => entry
     1.7 -          case None => error("Bad ISABELLE_DOCS_EXAMPLES entry: " + file)
     1.8 +          case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
     1.9          })
    1.10  
    1.11    def contents(): List[Entry] =
    1.12 @@ -91,9 +91,9 @@
    1.13    def main(args: Array[String])
    1.14    {
    1.15      Command_Line.tool {
    1.16 +      val entries = contents()
    1.17        if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
    1.18        else {
    1.19 -        val entries = contents()
    1.20          args.foreach(arg =>
    1.21            entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
    1.22              case Some(path) => view(path)