--- 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
--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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 }
- }
}
--- 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) =
--- 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
--- /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))
+ }
+ }
+ }
+}
+
--- 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
}
}
--- 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
--- 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"
--- 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 <<EOF
+jEdit Documentation
+ jedit-manual jEdit 5.1 User's Guide
+ jedit-changes jEdit 5.1 Version History
+
+EOF
+
fi
popd >/dev/null
--- 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)),
--- 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><b>" + HTML.encode(name) + "</b>: " + HTML.encode(title) + "</html>"
@@ -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))