# HG changeset patch # User wenzelm # Date 1396734150 -7200 # Node ID 4eb88149c7b2beaeeb78041dd30a04ff0293ba89 # Parent b266e7a864851f4a9c068ab8c99394e5638212c1# Parent 92fb6be9a4601a2858df0f367b550e63b74dd1f4 merged diff -r b266e7a86485 -r 4eb88149c7b2 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sat Apr 05 11:37:00 2014 +0200 +++ b/Admin/components/components.sha1 Sat Apr 05 23:42:30 2014 +0200 @@ -39,6 +39,7 @@ c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz 65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz 30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz +054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz 6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz diff -r b266e7a86485 -r 4eb88149c7b2 Admin/components/main --- a/Admin/components/main Sat Apr 05 11:37:00 2014 +0200 +++ b/Admin/components/main Sat Apr 05 23:42:30 2014 +0200 @@ -4,7 +4,7 @@ exec_process-1.0.3 Haskabelle-2013 jdk-7u40 -jedit_build-20131106 +jedit_build-20140405 jfreechart-1.0.14-1 kodkodi-1.5.2 polyml-5.5.1-1 diff -r b266e7a86485 -r 4eb88149c7b2 Admin/lib/Tools/build_doc --- a/Admin/lib/Tools/build_doc Sat Apr 05 11:37:00 2014 +0200 +++ b/Admin/lib/Tools/build_doc Sat Apr 05 23:42:30 2014 +0200 @@ -12,14 +12,15 @@ function usage() { echo - echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]" + echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]" echo echo " Options are:" echo " -a select all doc sessions" echo " -j INT maximum number of parallel jobs (default 1)" echo " -s system build mode" echo - echo " Build Isabelle documentation from (doc) sessions." + echo " Build Isabelle documentation from doc sessions with suitable" + echo " document_variants." echo exit 1 } @@ -38,12 +39,9 @@ ## process command line -declare -a BUILD_ARGS=() - - -# options - ALL_DOCS="false" +MAX_JOBS="1" +SYSTEM_MODE="false" while getopts "aj:s" OPT do @@ -53,11 +51,10 @@ ;; j) check_number "$OPTARG" - BUILD_ARGS["${#BUILD_ARGS[@]}"]="-j" - BUILD_ARGS["${#BUILD_ARGS[@]}"]="$OPTARG" + MAX_JOBS="$OPTARG" ;; s) - BUILD_ARGS["${#BUILD_ARGS[@]}"]="-s" + SYSTEM_MODE="true" ;; \?) usage @@ -67,42 +64,15 @@ shift $(($OPTIND - 1)) - -# arguments - -if [ "$ALL_DOCS" = true ]; then - BUILD_ARGS["${#BUILD_ARGS[@]}"]="-g" - BUILD_ARGS["${#BUILD_ARGS[@]}"]="doc" -else - [ "$#" -eq 0 ] && usage -fi - -BUILD_ARGS["${#BUILD_ARGS[@]}"]="--" - -while [ "$#" -ne 0 ]; do - BUILD_ARGS["${#BUILD_ARGS[@]}"]="$1" - shift -done +[ "$ALL_DOCS" = false -a "$#" -eq 0 ] && usage ## main -OUTPUT="$ISABELLE_TMP_PREFIX$$" -mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\"" +isabelle_admin_build jars || exit $? -"$ISABELLE_TOOL" build -R -b "${BUILD_ARGS[@]}" -RC=$? +declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" -if [ "$RC" = 0 ]; then - "$ISABELLE_TOOL" build -o browser_info=false -o "document=pdf" \ - -o "document_output=$OUTPUT" -c "${BUILD_ARGS[@]}" - RC=$? -fi +"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc \ + "$ALL_DOCS" "$MAX_JOBS" "$SYSTEM_MODE" "$@" -if [ "$RC" = 0 ]; then - cp -f "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc" -fi - -rm -rf "$OUTPUT" - -exit $RC diff -r b266e7a86485 -r 4eb88149c7b2 Admin/lib/scripts/churn_pie --- a/Admin/lib/scripts/churn_pie Sat Apr 05 11:37:00 2014 +0200 +++ b/Admin/lib/scripts/churn_pie Sat Apr 05 23:42:30 2014 +0200 @@ -1,4 +1,4 @@ -#!/usr/bin/python +#!/usr/bin/env python import re from pychart import theme, pie_plot, area, fill_style, arrow, legend diff -r b266e7a86485 -r 4eb88149c7b2 doc/Contents --- a/doc/Contents Sat Apr 05 11:37:00 2014 +0200 +++ b/doc/Contents Sat Apr 05 23:42:30 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,14 +10,14 @@ 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 system The Isabelle System Manual jedit Isabelle/jEdit -Old Manuals (outdated) +Old Manuals intro Old Introduction to Isabelle logics Isabelle's Logics: HOL and misc logics logics-ZF Isabelle's Logics: FOL and ZF diff -r b266e7a86485 -r 4eb88149c7b2 etc/settings --- a/etc/settings Sat Apr 05 11:37:00 2014 +0200 +++ b/etc/settings Sat Apr 05 23:42:30 2014 +0200 @@ -101,6 +101,9 @@ # Where to look for docs (multiple dirs separated by ':'). ISABELLE_DOCS="$ISABELLE_HOME/doc" +ISABELLE_DOCS_RELEASE_NOTES="ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:README_REPOSITORY" +ISABELLE_DOCS_EXAMPLES="src/HOL/ex/Seq.thy:src/HOL/ex/ML.thy:src/HOL/Unix/Unix.thy:src/HOL/Isar_Examples/Drinker.thy:src/Tools/SML/Examples.thy" + # "open" within desktop environment (potentially asynchronous) case "$ISABELLE_PLATFORM_FAMILY" in linux) diff -r b266e7a86485 -r 4eb88149c7b2 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Pure/General/file.scala Sat Apr 05 23:42:30 2014 +0200 @@ -142,21 +142,5 @@ } def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) - - - /* tmp files */ - - def tmp_file(prefix: String): JFile = - { - val file = JFile.createTempFile(prefix, null) - file.deleteOnExit - file - } - - def with_tmp_file[A](prefix: String)(body: JFile => A): A = - { - val file = tmp_file(prefix) - try { body(file) } finally { file.delete } - } } diff -r b266e7a86485 -r 4eb88149c7b2 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Pure/System/isabelle_system.scala Sat Apr 05 23:42:30 2014 +0200 @@ -11,6 +11,7 @@ import java.util.regex.Pattern import java.io.{File => JFile, BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter} +import java.nio.file.Files import scala.util.matching.Regex @@ -91,7 +92,10 @@ } val settings = - File.with_tmp_file("settings") { dump => + { + val dump = JFile.createTempFile("settings", null) + dump.deleteOnExit + try { val shell_prefix = if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l") else Nil @@ -108,6 +112,8 @@ }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } + finally { dump.delete } + } _settings = Some(settings) set_cygwin_root() } @@ -202,6 +208,9 @@ else "file:///" + s.replace('\\', '/') } + def shell_path(path: Path): String = "'" + standard_path(path) + "'" + def shell_path(file: JFile): String = "'" + posix_path(file) + "'" + /* source files of Isabelle/ML bootstrap */ @@ -351,6 +360,30 @@ } + /* tmp files */ + + private def isabelle_tmp_prefix(): JFile = + { + val path = Path.explode("$ISABELLE_TMP_PREFIX") + mkdirs(path) + platform_file(path) + } + + def tmp_file[A](name: String, ext: String = ""): JFile = + { + val suffix = if (ext == "") "" else "." + ext + val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile + file.deleteOnExit + file + } + + def with_tmp_file[A](name: String, ext: String = "")(body: JFile => A): A = + { + val file = tmp_file(name, ext) + try { body(file) } finally { file.delete } + } + + /* bash */ final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int) @@ -366,7 +399,7 @@ progress_stderr: String => Unit = (_: String) => (), progress_limit: Option[Long] = None): Bash_Result = { - File.with_tmp_file("isabelle_script") { script_file => + with_tmp_file("isabelle_script") { script_file => File.write(script_file, script) val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file)) proc.stdin.close @@ -401,6 +434,35 @@ def bash(script: String): Bash_Result = bash_env(null, null, script) + /* tmp dirs */ + + private def system_command(cmd: String) + { + val res = bash(cmd) + if (res.rc != 0) + error(cat_lines(("System command failed: " + cmd) :: res.out_lines ::: res.err_lines)) + } + + def rm_tree(dir: JFile) + { + dir.delete + if (dir.isDirectory) system_command("rm -r -f " + shell_path(dir)) + } + + def tmp_dir(name: String): JFile = + { + val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile + dir.deleteOnExit + dir + } + + def with_tmp_dir[A](name: String)(body: JFile => A): A = + { + val dir = tmp_dir(name) + try { body(dir) } finally { rm_tree(dir) } + } + + /* system tools */ def isabelle_tool(name: String, args: String*): (String, Int) = diff -r b266e7a86485 -r 4eb88149c7b2 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Pure/Tools/build.scala Sat Apr 05 23:42:30 2014 +0200 @@ -508,7 +508,7 @@ private val parent = info.parent.getOrElse("") - private val args_file = File.tmp_file("args") + private val args_file = Isabelle_System.tmp_file("args") File.write(args_file, YXML.string_of_body( if (is_pure(name)) Options.encode(info.options) else diff -r b266e7a86485 -r 4eb88149c7b2 src/Pure/Tools/build_doc.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/build_doc.scala Sat Apr 05 23:42:30 2014 +0200 @@ -0,0 +1,91 @@ +/* Title: Pure/Tools/build_doc.scala + Author: Makarius + +Build Isabelle documentation. +*/ + +package isabelle + + +import java.io.{File => JFile} + + +object Build_Doc +{ + /* build_doc */ + + def build_doc( + options: Options, + progress: Build.Progress = Build.Ignore_Progress, + all_docs: Boolean = false, + max_jobs: Int = 1, + system_mode: Boolean = false, + docs: List[String] = Nil): Int = + { + val selection = + for { + (name, info) <- Build.find_sessions(options, Nil).topological_order + if info.groups.contains("doc") + doc = info.options.string("document_variants") + if all_docs || docs.contains(doc) + } yield (doc, name) + + val selected_docs = selection.map(_._1) + val sessions = selection.map(_._2) + + docs.filter(doc => !selected_docs.contains(doc)) match { + case Nil => + case bad => error("No doc session for " + commas_quote(bad)) + } + + + progress.echo("Build started for documentation " + commas_quote(selected_docs)) + val rc1 = + Build.build(options, progress, requirements = true, build_heap = true, + max_jobs = max_jobs, system_mode = system_mode, sessions = sessions) + if (rc1 == 0) { + Isabelle_System.with_tmp_dir("document_output")(output => + { + val rc2 = + Build.build( + options.bool.update("browser_info", false). + string.update("document", "pdf"). + string.update("document_output", Isabelle_System.posix_path(output)), + progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode, + sessions = sessions) + if (rc2 == 0) { + val doc_dir = Path.explode("$ISABELLE_HOME/doc").file + for (doc <- selected_docs) { + val name = doc + ".pdf" + File.copy(new JFile(output, name), new JFile(doc_dir, name)) + } + } + rc2 + }) + } + else rc1 + } + + + /* command line entry point */ + + def main(args: Array[String]) + { + Command_Line.tool { + args.toList match { + case + Properties.Value.Boolean(all_docs) :: + Properties.Value.Int(max_jobs) :: + Properties.Value.Boolean(system_mode) :: + Command_Line.Chunks(docs) => + val options = Options.init() + val progress = new Build.Console_Progress(false) + progress.interrupt_handler { + build_doc(options, progress, all_docs, max_jobs, system_mode, docs) + } + case _ => error("Bad arguments:\n" + cat_lines(args)) + } + } + } +} + diff -r b266e7a86485 -r 4eb88149c7b2 src/Pure/Tools/doc.scala --- a/src/Pure/Tools/doc.scala Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Pure/Tools/doc.scala Sat Apr 05 23:42:30 2014 +0200 @@ -1,7 +1,7 @@ /* Title: Pure/Tools/doc.scala Author: Makarius -View Isabelle documentation. +Access to Isabelle documentation. */ package isabelle @@ -22,23 +22,23 @@ /* contents */ - private def contents_lines(): List[String] = + private def contents_lines(): List[(Path, String)] = for { dir <- dirs() catalog = dir + Path.basic("Contents") if catalog.is_file line <- split_lines(Library.trim_line(File.read(catalog))) - } yield line + } yield (dir, line) sealed abstract class Entry - case class Section(text: String) extends Entry - case class Doc(name: String, title: 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 - def text_file(name: String): Option[Text_File] = + def text_file(name: Path): Option[Text_File] = { - val path = Path.variable("ISABELLE_HOME") + Path.explode(name) - if (path.is_file) Some(Text_File(name, path)) + val path = Path.variable("ISABELLE_HOME") + name + if (path.is_file) Some(Text_File(name.implode, path)) else None } @@ -46,33 +46,28 @@ private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""") private def release_notes(): List[Entry] = - { - val names = - List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS", - "contrib/README", "README_REPOSITORY") - Section("Release notes") :: - (for (name <- names; entry <- text_file(name)) yield entry) - } + Section("Release notes", true) :: + Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_)) private def examples(): List[Entry] = - { - val names = - List( - "src/HOL/ex/Seq.thy", - "src/HOL/ex/ML.thy", - "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) :: + Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => + text_file(file) match { + case Some(entry) => entry + case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file) + }) def contents(): List[Entry] = (for { - line <- contents_lines() + (dir, line) <- contents_lines() entry <- line match { - case Section_Entry(text) => Some(Section(text)) - case Doc_Entry(name, title) => Some(Doc(name, title)) + 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() @@ -80,12 +75,13 @@ /* view */ - def view(name: String) + def view(path: Path) { - val doc = Path.basic(name + ".pdf") - dirs().find(dir => (dir + doc).is_file) match { - case Some(dir) => Isabelle_System.pdf_viewer(dir + doc) - case None => error("Missing Isabelle documentation file: " + doc) + if (path.is_file) Console.println(File.read(path)) + else { + val pdf = path.ext("pdf") + if (pdf.is_file) Isabelle_System.pdf_viewer(pdf) + else error("Bad Isabelle documentation file: " + pdf) } } @@ -95,8 +91,16 @@ def main(args: Array[String]) { Command_Line.tool { - if (args.isEmpty) Console.println(cat_lines(contents_lines())) - else args.foreach(view) + val entries = contents() + if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2))) + else { + args.foreach(arg => + entries.collectFirst { case Doc(name, _, path) if arg == name => path } match { + case Some(path) => view(path) + case None => error("No Isabelle documentation entry: " + quote(arg)) + } + ) + } 0 } } diff -r b266e7a86485 -r 4eb88149c7b2 src/Pure/build-jars --- a/src/Pure/build-jars Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Pure/build-jars Sat Apr 05 23:42:30 2014 +0200 @@ -77,6 +77,7 @@ Thy/thy_info.scala Thy/thy_syntax.scala Tools/build.scala + Tools/build_doc.scala Tools/doc.scala Tools/keywords.scala Tools/main.scala diff -r b266e7a86485 -r 4eb88149c7b2 src/Tools/jEdit/etc/settings --- a/src/Tools/jEdit/etc/settings Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Tools/jEdit/etc/settings Sat Apr 05 23:42:30 2014 +0200 @@ -12,4 +12,5 @@ ISABELLE_JEDIT_OPTIONS="" ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools" +ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/dist/doc" diff -r b266e7a86485 -r 4eb88149c7b2 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sat Apr 05 23:42:30 2014 +0200 @@ -207,10 +207,14 @@ JEDIT_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar" JEDIT_JARS=( + "$ISABELLE_JEDIT_BUILD_HOME/contrib/Code2HTML.jar" + "$ISABELLE_JEDIT_BUILD_HOME/contrib/CommonControls.jar" "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar" "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar" "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar" + "$ISABELLE_JEDIT_BUILD_HOME/contrib/kappalayout.jar" "$ISABELLE_JEDIT_BUILD_HOME/contrib/MacOSX.jar" + "$ISABELLE_JEDIT_BUILD_HOME/contrib/Navigator.jar" "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar" "$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar" "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar" @@ -322,6 +326,16 @@ isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed cd ../.. rm -rf dist/classes + + cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.1.0manual-a4.pdf" dist/doc/jedit-manual.pdf + cp dist/doc/CHANGES.txt dist/doc/jedit-changes + cat > dist/doc/Contents </dev/null diff -r b266e7a86485 -r 4eb88149c7b2 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Tools/jEdit/src/active.scala Sat Apr 05 23:42:30 2014 +0200 @@ -32,7 +32,7 @@ case XML.Elem(Markup(Markup.BROWSER, _), body) => default_thread_pool.submit(() => { - val graph_file = File.tmp_file("graph") + val graph_file = Isabelle_System.tmp_file("graph") File.write(graph_file, XML.content(body)) Isabelle_System.bash_env(null, Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)), diff -r b266e7a86485 -r 4eb88149c7b2 src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Sat Apr 05 11:37:00 2014 +0200 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Apr 05 23:42:30 2014 +0200 @@ -22,7 +22,7 @@ { private val docs = Doc.contents() - private case class Documentation(name: String, title: String) + private case class Documentation(name: String, title: String, path: Path) { override def toString = "" + HTML.encode(name) + ": " + HTML.encode(title) + "" @@ -35,11 +35,11 @@ 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) => + case Doc.Doc(name, title, path) => root.getLastChild.asInstanceOf[DefaultMutableTreeNode] - .add(new DefaultMutableTreeNode(Documentation(name, title))) + .add(new DefaultMutableTreeNode(Documentation(name, title, path))) case Doc.Text_File(name: String, path: Path) => root.getLastChild.asInstanceOf[DefaultMutableTreeNode] .add(new DefaultMutableTreeNode(Text_File(name, path.expand))) @@ -62,16 +62,20 @@ (click.getLastPathComponent, tree.getLastSelectedPathComponent) match { case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 => node.getUserObject match { - case Documentation(name, _) => - default_thread_pool.submit(() => - try { Doc.view(name) } - catch { - case exn: Throwable => - GUI.error_dialog(view, - "Documentation error", GUI.scrollable_text(Exn.message(exn))) - }) case Text_File(_, path) => PIDE.editor.goto_file(view, Isabelle_System.platform_path(path)) + case Documentation(_, _, path) => + if (path.is_file) + PIDE.editor.goto_file(view, Isabelle_System.platform_path(path)) + else { + default_thread_pool.submit(() => + try { Doc.view(path) } + catch { + case exn: Throwable => + GUI.error_dialog(view, + "Documentation error", GUI.scrollable_text(Exn.message(exn))) + }) + } case _ => } case _ => @@ -79,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))