# HG changeset patch
# User wenzelm
# Date 1396714494 -7200
# Node ID 7490555d7dff566eba6ada8e2f7f5120c12c6411
# Parent  1ffd7eaa778be198f73f3026810b56820cd9eacd
clarified Doc entry: more explicit path;
allow plain files as Doc;
refer to official jEdit documentation;

diff -r 1ffd7eaa778b -r 7490555d7dff src/Pure/Tools/doc.scala
--- 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
     }
   }
diff -r 1ffd7eaa778b -r 7490555d7dff src/Tools/jEdit/etc/settings
--- 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"
 
diff -r 1ffd7eaa778b -r 7490555d7dff src/Tools/jEdit/lib/Tools/jedit
--- 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
diff -r 1ffd7eaa778b -r 7490555d7dff src/Tools/jEdit/src/documentation_dockable.scala
--- 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 _ =>