# HG changeset patch
# User wenzelm
# Date 1363114984 -3600
# Node ID b05cd411d3d3d833b486a7e4dd3cee8dde2fa81d
# Parent  f390b59b4b4a9769ef311d092e51038a0cb86000
include session description in chapter index;
prefer alphabetical order;

diff -r f390b59b4b4a -r b05cd411d3d3 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Tue Mar 12 18:44:48 2013 +0100
+++ b/src/Pure/Thy/html.scala	Tue Mar 12 20:03:04 2013 +0100
@@ -51,13 +51,19 @@
 
   /* common markup elements */
 
-  def session_entry(name: String): String =
+  private def session_entry(entry: (String, String)): String =
+  {
+    val (name, description) = entry
+    val descr =
+      if (description == "") Nil
+      else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description))))
     XML.string_of_tree(
       XML.elem("li",
         List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
-          List(XML.Text(name)))))) + "\n"
+          List(XML.Text(name)))) ::: descr)) + "\n"
+  }
 
-  def chapter_index(chapter: String, sessions: List[String]): String =
+  def chapter_index(chapter: String, sessions: List[(String, String)]): String =
   {
     begin_document("Isabelle/" + chapter + " sessions") +
       (if (sessions.isEmpty) ""
diff -r f390b59b4b4a -r b05cd411d3d3 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Tue Mar 12 18:44:48 2013 +0100
+++ b/src/Pure/Thy/present.scala	Tue Mar 12 20:03:04 2013 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.collection.immutable.SortedMap
+
+
 object Present
 {
   /* maintain chapter index -- NOT thread-safe */
@@ -14,22 +17,29 @@
   private val index_path = Path.basic("index.html")
   private val sessions_path = Path.basic(".sessions")
 
-  private def read_sessions(dir: Path): List[String] =
-    split_lines(File.read(dir + sessions_path))
+  private def read_sessions(dir: Path): List[(String, String)] =
+  {
+    import XML.Decode._
+    list(pair(string, string))(YXML.parse_body(File.read(dir + sessions_path)))
+  }
 
-  private def write_sessions(dir: Path, sessions: List[String]): Unit =
-    File.write(dir + sessions_path, cat_lines(sessions))
+  private def write_sessions(dir: Path, sessions: List[(String, String)])
+  {
+    import XML.Encode._
+    File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
+  }
 
-  def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[String]): Unit =
+  def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
   {
     val dir = info_path + Path.basic(chapter)
     Isabelle_System.mkdirs(dir)
 
     val sessions0 =
-      try { split_lines(File.read(dir + sessions_path)) }
-      catch { case ERROR(_) => Nil }
+      try { read_sessions(dir + sessions_path) }
+      catch { case ERROR(_) => Nil case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
 
-    val sessions = sessions0.filterNot(new_sessions.contains) ::: new_sessions
+    val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
+
     write_sessions(dir, sessions)
     File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
   }
diff -r f390b59b4b4a -r b05cd411d3d3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 12 18:44:48 2013 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 12 20:03:04 2013 +0100
@@ -868,11 +868,11 @@
       else loop(queue, Map.empty, Map.empty)
 
     val session_entries =
-      (for ((name, res) <- results.iterator)
-        yield (full_tree(name).chapter, name)).toList.groupBy(_._1).map(
-          { case (chapter, es) => (chapter, es.map(_._2).sorted) })
-    for ((chapter, names) <- session_entries)
-      Present.update_chapter_index(browser_info, chapter, names)
+      (for { (name, res) <- results.iterator; info = full_tree(name) }
+        yield (info.chapter, (name, info.description))).toList.groupBy(_._1).map(
+          { case (chapter, es) => (chapter, es.map(_._2)) })
+    for ((chapter, entries) <- session_entries)
+      Present.update_chapter_index(browser_info, chapter, entries)
 
     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
     if (rc != 0 && (verbose || !no_build)) {