# HG changeset patch
# User wenzelm
# Date 1441986529 -7200
# Node ID 13f4056c42d7e3db79247746e1cc31d74715efad
# Parent  931b732617a2bb3cfc97a2b734efd8896c371405
clarified order;

diff -r 931b732617a2 -r 13f4056c42d7 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Fri Sep 11 11:12:08 2015 +0200
+++ b/src/Pure/Tools/doc.scala	Fri Sep 11 17:48:49 2015 +0200
@@ -58,19 +58,24 @@
         })
 
   def contents(): List[Entry] =
-    (for {
-      (dir, line) <- contents_lines()
-      entry <-
-        line match {
-          case Section_Entry(text) =>
-            Library.try_unsuffix("!", text) match {
-              case None => Some(Section(text, false))
-              case Some(txt) => Some(Section(txt, true))
-            }
-          case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
-          case _ => None
-        }
-    } yield entry) ::: release_notes() ::: examples()
+  {
+    val main_contents =
+      for {
+        (dir, line) <- contents_lines()
+        entry <-
+          line match {
+            case Section_Entry(text) =>
+              Library.try_unsuffix("!", text) match {
+                case None => Some(Section(text, false))
+                case Some(txt) => Some(Section(txt, true))
+              }
+            case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
+            case _ => None
+          }
+      } yield entry
+
+    examples() ::: release_notes() ::: main_contents
+  }
 
 
   /* view */
@@ -104,4 +109,3 @@
     }
   }
 }
-