explicit indication of important doc sections ("!"), which are expanded in the tree view;
authorwenzelm
Sat Apr 05 18:52:03 2014 +0200 (2014-04-05)
changeset 56423c2f52824dbb2
parent 56422 7490555d7dff
child 56424 7032378cc097
explicit indication of important doc sections ("!"), which are expanded in the tree view;
doc/Contents
src/Pure/Tools/doc.scala
src/Tools/jEdit/src/documentation_dockable.scala
     1.1 --- a/doc/Contents	Sat Apr 05 18:14:54 2014 +0200
     1.2 +++ b/doc/Contents	Sat Apr 05 18:52:03 2014 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -Tutorials
     1.5 +Tutorials!
     1.6    prog-prove      Programming and Proving in Isabelle/HOL
     1.7    tutorial        Tutorial on Isabelle/HOL
     1.8    locales         Tutorial on Locales
     1.9 @@ -10,7 +10,7 @@
    1.10    sledgehammer    User's Guide to Sledgehammer
    1.11    sugar           LaTeX Sugar for Isabelle documents
    1.12  
    1.13 -Reference Manuals
    1.14 +Reference Manuals!
    1.15    main            What's in Main
    1.16    isar-ref        The Isabelle/Isar Reference Manual
    1.17    implementation  The Isabelle/Isar Implementation Manual
     2.1 --- a/src/Pure/Tools/doc.scala	Sat Apr 05 18:14:54 2014 +0200
     2.2 +++ b/src/Pure/Tools/doc.scala	Sat Apr 05 18:52:03 2014 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4      } yield (dir, line)
     2.5  
     2.6    sealed abstract class Entry
     2.7 -  case class Section(text: String) extends Entry
     2.8 +  case class Section(text: String, important: Boolean) extends Entry
     2.9    case class Doc(name: String, title: String, path: Path) extends Entry
    2.10    case class Text_File(name: String, path: Path) extends Entry
    2.11  
    2.12 @@ -50,7 +50,7 @@
    2.13      val names =
    2.14        List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
    2.15          "contrib/README", "README_REPOSITORY")
    2.16 -    Section("Release notes") ::
    2.17 +    Section("Release notes", true) ::
    2.18        (for (name <- names; entry <- text_file(name)) yield entry)
    2.19    }
    2.20  
    2.21 @@ -63,7 +63,7 @@
    2.22          "src/HOL/Unix/Unix.thy",
    2.23          "src/HOL/Isar_Examples/Drinker.thy",
    2.24          "src/Tools/SML/Examples.thy")
    2.25 -    Section("Examples") :: names.map(name => text_file(name).get)
    2.26 +    Section("Examples", true) :: names.map(name => text_file(name).get)
    2.27    }
    2.28  
    2.29    def contents(): List[Entry] =
    2.30 @@ -71,7 +71,11 @@
    2.31        (dir, line) <- contents_lines()
    2.32        entry <-
    2.33          line match {
    2.34 -          case Section_Entry(text) => Some(Section(text))
    2.35 +          case Section_Entry(text) =>
    2.36 +            Library.try_unsuffix("!", text) match {
    2.37 +              case None => Some(Section(text, false))
    2.38 +              case Some(txt) => Some(Section(txt, true))
    2.39 +            }
    2.40            case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
    2.41            case _ => None
    2.42          }
     3.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Apr 05 18:14:54 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Apr 05 18:52:03 2014 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4  
     3.5    private val root = new DefaultMutableTreeNode
     3.6    docs foreach {
     3.7 -    case Doc.Section(text) =>
     3.8 +    case Doc.Section(text, _) =>
     3.9        root.add(new DefaultMutableTreeNode(text))
    3.10      case Doc.Doc(name, title, path) =>
    3.11        root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    3.12 @@ -83,9 +83,23 @@
    3.13        }
    3.14      }
    3.15    })
    3.16 -  tree.setRootVisible(false)
    3.17 -  tree.setVisibleRowCount(docs.length)
    3.18 -  (0 until docs.length).foreach(tree.expandRow)
    3.19 +
    3.20 +  {
    3.21 +    var expand = true
    3.22 +    var visible = 0
    3.23 +    def make_visible(row: Int) { visible += 1; tree.expandRow(row) }
    3.24 +    for ((entry, row) <- docs.zipWithIndex) {
    3.25 +      entry match {
    3.26 +        case Doc.Section(_, important) =>
    3.27 +          expand = important
    3.28 +          make_visible(row)
    3.29 +        case _ =>
    3.30 +          if (expand) make_visible(row)
    3.31 +      }
    3.32 +    }
    3.33 +    tree.setRootVisible(false)
    3.34 +    tree.setVisibleRowCount(visible)
    3.35 +  }
    3.36  
    3.37    private val tree_view = new JScrollPane(tree)
    3.38    tree_view.setMinimumSize(new Dimension(100, 50))