# HG changeset patch
# User wenzelm
# Date 1396718176 -7200
# Node ID d12653fbd5b1290cf60fafc48b2e216285d97e92
# Parent  7032378cc0975264fc6fb9c2c49f12ca09d2d81a
tuned error;

diff -r 7032378cc097 -r d12653fbd5b1 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sat Apr 05 19:07:05 2014 +0200
+++ b/src/Pure/Tools/doc.scala	Sat Apr 05 19:16:16 2014 +0200
@@ -54,7 +54,7 @@
       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
         text_file(file) match {
           case Some(entry) => entry
-          case None => error("Bad ISABELLE_DOCS_EXAMPLES entry: " + file)
+          case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
         })
 
   def contents(): List[Entry] =
@@ -91,9 +91,9 @@
   def main(args: Array[String])
   {
     Command_Line.tool {
+      val entries = contents()
       if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
       else {
-        val entries = contents()
         args.foreach(arg =>
           entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
             case Some(path) => view(path)