clarified Doc entry: more explicit path;
allow plain files as Doc;
refer to official jEdit documentation;
--- a/src/Pure/Tools/doc.scala Sat Apr 05 15:03:40 2014 +0200
+++ b/src/Pure/Tools/doc.scala Sat Apr 05 18:14:54 2014 +0200
@@ -22,17 +22,17 @@
/* 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 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] =
@@ -68,11 +68,11 @@
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 Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
case _ => None
}
} yield entry) ::: release_notes() ::: examples()
@@ -80,12 +80,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 +96,16 @@
def main(args: Array[String])
{
Command_Line.tool {
- if (args.isEmpty) Console.println(cat_lines(contents_lines()))
- else args.foreach(view)
+ if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
+ else {
+ val entries = contents()
+ 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/Tools/jEdit/etc/settings Sat Apr 05 15:03:40 2014 +0200
+++ b/src/Tools/jEdit/etc/settings Sat Apr 05 18:14:54 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 15:03:40 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Apr 05 18:14:54 2014 +0200
@@ -326,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/documentation_dockable.scala Sat Apr 05 15:03:40 2014 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Apr 05 18:14:54 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>"
@@ -37,9 +37,9 @@
docs foreach {
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 _ =>