# HG changeset patch
# User wenzelm
# Date 1396716723 -7200
# Node ID c2f52824dbb297e3e8cf751e3d33c20f82b8b325
# Parent  7490555d7dff566eba6ada8e2f7f5120c12c6411
explicit indication of important doc sections ("!"), which are expanded in the tree view;

diff -r 7490555d7dff -r c2f52824dbb2 doc/Contents
--- a/doc/Contents	Sat Apr 05 18:14:54 2014 +0200
+++ b/doc/Contents	Sat Apr 05 18:52:03 2014 +0200
@@ -1,4 +1,4 @@
-Tutorials
+Tutorials!
   prog-prove      Programming and Proving in Isabelle/HOL
   tutorial        Tutorial on Isabelle/HOL
   locales         Tutorial on Locales
@@ -10,7 +10,7 @@
   sledgehammer    User's Guide to Sledgehammer
   sugar           LaTeX Sugar for Isabelle documents
 
-Reference Manuals
+Reference Manuals!
   main            What's in Main
   isar-ref        The Isabelle/Isar Reference Manual
   implementation  The Isabelle/Isar Implementation Manual
diff -r 7490555d7dff -r c2f52824dbb2 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sat Apr 05 18:14:54 2014 +0200
+++ b/src/Pure/Tools/doc.scala	Sat Apr 05 18:52:03 2014 +0200
@@ -31,7 +31,7 @@
     } yield (dir, line)
 
   sealed abstract class Entry
-  case class Section(text: String) extends Entry
+  case class Section(text: String, important: Boolean) extends Entry
   case class Doc(name: String, title: String, path: Path) extends Entry
   case class Text_File(name: String, path: Path) extends Entry
 
@@ -50,7 +50,7 @@
     val names =
       List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
         "contrib/README", "README_REPOSITORY")
-    Section("Release notes") ::
+    Section("Release notes", true) ::
       (for (name <- names; entry <- text_file(name)) yield entry)
   }
 
@@ -63,7 +63,7 @@
         "src/HOL/Unix/Unix.thy",
         "src/HOL/Isar_Examples/Drinker.thy",
         "src/Tools/SML/Examples.thy")
-    Section("Examples") :: names.map(name => text_file(name).get)
+    Section("Examples", true) :: names.map(name => text_file(name).get)
   }
 
   def contents(): List[Entry] =
@@ -71,7 +71,11 @@
       (dir, line) <- contents_lines()
       entry <-
         line match {
-          case Section_Entry(text) => Some(Section(text))
+          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
         }
diff -r 7490555d7dff -r c2f52824dbb2 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Apr 05 18:14:54 2014 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Apr 05 18:52:03 2014 +0200
@@ -35,7 +35,7 @@
 
   private val root = new DefaultMutableTreeNode
   docs foreach {
-    case Doc.Section(text) =>
+    case Doc.Section(text, _) =>
       root.add(new DefaultMutableTreeNode(text))
     case Doc.Doc(name, title, path) =>
       root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
@@ -83,9 +83,23 @@
       }
     }
   })
-  tree.setRootVisible(false)
-  tree.setVisibleRowCount(docs.length)
-  (0 until docs.length).foreach(tree.expandRow)
+
+  {
+    var expand = true
+    var visible = 0
+    def make_visible(row: Int) { visible += 1; tree.expandRow(row) }
+    for ((entry, row) <- docs.zipWithIndex) {
+      entry match {
+        case Doc.Section(_, important) =>
+          expand = important
+          make_visible(row)
+        case _ =>
+          if (expand) make_visible(row)
+      }
+    }
+    tree.setRootVisible(false)
+    tree.setVisibleRowCount(visible)
+  }
 
   private val tree_view = new JScrollPane(tree)
   tree_view.setMinimumSize(new Dimension(100, 50))