explicit indication of important doc sections ("!"), which are expanded in the tree view;
--- 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
--- 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
}
--- 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))