clarified Doc entry: more explicit path;
authorwenzelm
Sat Apr 05 18:14:54 2014 +0200 (2014-04-05)
changeset 564227490555d7dff
parent 56421 1ffd7eaa778b
child 56423 c2f52824dbb2
clarified Doc entry: more explicit path;
allow plain files as Doc;
refer to official jEdit documentation;
src/Pure/Tools/doc.scala
src/Tools/jEdit/etc/settings
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/documentation_dockable.scala
     1.1 --- a/src/Pure/Tools/doc.scala	Sat Apr 05 15:03:40 2014 +0200
     1.2 +++ b/src/Pure/Tools/doc.scala	Sat Apr 05 18:14:54 2014 +0200
     1.3 @@ -22,17 +22,17 @@
     1.4  
     1.5    /* contents */
     1.6  
     1.7 -  private def contents_lines(): List[String] =
     1.8 +  private def contents_lines(): List[(Path, String)] =
     1.9      for {
    1.10        dir <- dirs()
    1.11        catalog = dir + Path.basic("Contents")
    1.12        if catalog.is_file
    1.13        line <- split_lines(Library.trim_line(File.read(catalog)))
    1.14 -    } yield line
    1.15 +    } yield (dir, line)
    1.16  
    1.17    sealed abstract class Entry
    1.18    case class Section(text: String) extends Entry
    1.19 -  case class Doc(name: String, title: String) extends Entry
    1.20 +  case class Doc(name: String, title: String, path: Path) extends Entry
    1.21    case class Text_File(name: String, path: Path) extends Entry
    1.22  
    1.23    def text_file(name: String): Option[Text_File] =
    1.24 @@ -68,11 +68,11 @@
    1.25  
    1.26    def contents(): List[Entry] =
    1.27      (for {
    1.28 -      line <- contents_lines()
    1.29 +      (dir, line) <- contents_lines()
    1.30        entry <-
    1.31          line match {
    1.32            case Section_Entry(text) => Some(Section(text))
    1.33 -          case Doc_Entry(name, title) => Some(Doc(name, title))
    1.34 +          case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
    1.35            case _ => None
    1.36          }
    1.37      } yield entry) ::: release_notes() ::: examples()
    1.38 @@ -80,12 +80,13 @@
    1.39  
    1.40    /* view */
    1.41  
    1.42 -  def view(name: String)
    1.43 +  def view(path: Path)
    1.44    {
    1.45 -    val doc = Path.basic(name + ".pdf")
    1.46 -    dirs().find(dir => (dir + doc).is_file) match {
    1.47 -      case Some(dir) => Isabelle_System.pdf_viewer(dir + doc)
    1.48 -      case None => error("Missing Isabelle documentation file: " + doc)
    1.49 +    if (path.is_file) Console.println(File.read(path))
    1.50 +    else {
    1.51 +      val pdf = path.ext("pdf")
    1.52 +      if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
    1.53 +      else error("Bad Isabelle documentation file: " + pdf)
    1.54      }
    1.55    }
    1.56  
    1.57 @@ -95,8 +96,16 @@
    1.58    def main(args: Array[String])
    1.59    {
    1.60      Command_Line.tool {
    1.61 -      if (args.isEmpty) Console.println(cat_lines(contents_lines()))
    1.62 -      else args.foreach(view)
    1.63 +      if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
    1.64 +      else {
    1.65 +        val entries = contents()
    1.66 +        args.foreach(arg =>
    1.67 +          entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
    1.68 +            case Some(path) => view(path)
    1.69 +            case None => error("No Isabelle documentation entry: " + quote(arg))
    1.70 +          }
    1.71 +        )
    1.72 +      }
    1.73        0
    1.74      }
    1.75    }
     2.1 --- a/src/Tools/jEdit/etc/settings	Sat Apr 05 15:03:40 2014 +0200
     2.2 +++ b/src/Tools/jEdit/etc/settings	Sat Apr 05 18:14:54 2014 +0200
     2.3 @@ -12,4 +12,5 @@
     2.4  ISABELLE_JEDIT_OPTIONS=""
     2.5  
     2.6  ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
     2.7 +ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/dist/doc"
     2.8  
     3.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sat Apr 05 15:03:40 2014 +0200
     3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Apr 05 18:14:54 2014 +0200
     3.3 @@ -326,6 +326,16 @@
     3.4    isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
     3.5    cd ../..
     3.6    rm -rf dist/classes
     3.7 +
     3.8 +  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.1.0manual-a4.pdf" dist/doc/jedit-manual.pdf
     3.9 +  cp dist/doc/CHANGES.txt dist/doc/jedit-changes
    3.10 +  cat > dist/doc/Contents <<EOF
    3.11 +jEdit Documentation
    3.12 +  jedit-manual    jEdit 5.1 User's Guide
    3.13 +  jedit-changes   jEdit 5.1 Version History
    3.14 +
    3.15 +EOF
    3.16 +
    3.17  fi
    3.18  
    3.19  popd >/dev/null
     4.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Apr 05 15:03:40 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Apr 05 18:14:54 2014 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4  {
     4.5    private val docs = Doc.contents()
     4.6  
     4.7 -  private case class Documentation(name: String, title: String)
     4.8 +  private case class Documentation(name: String, title: String, path: Path)
     4.9    {
    4.10      override def toString =
    4.11        "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
    4.12 @@ -37,9 +37,9 @@
    4.13    docs foreach {
    4.14      case Doc.Section(text) =>
    4.15        root.add(new DefaultMutableTreeNode(text))
    4.16 -    case Doc.Doc(name, title) =>
    4.17 +    case Doc.Doc(name, title, path) =>
    4.18        root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    4.19 -        .add(new DefaultMutableTreeNode(Documentation(name, title)))
    4.20 +        .add(new DefaultMutableTreeNode(Documentation(name, title, path)))
    4.21      case Doc.Text_File(name: String, path: Path) =>
    4.22        root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    4.23          .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
    4.24 @@ -62,16 +62,20 @@
    4.25          (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
    4.26            case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
    4.27              node.getUserObject match {
    4.28 -              case Documentation(name, _) =>
    4.29 -                default_thread_pool.submit(() =>
    4.30 -                  try { Doc.view(name) }
    4.31 -                  catch {
    4.32 -                    case exn: Throwable =>
    4.33 -                      GUI.error_dialog(view,
    4.34 -                        "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    4.35 -                  })
    4.36                case Text_File(_, path) =>
    4.37                  PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    4.38 +              case Documentation(_, _, path) =>
    4.39 +                if (path.is_file)
    4.40 +                  PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    4.41 +                else {
    4.42 +                  default_thread_pool.submit(() =>
    4.43 +                    try { Doc.view(path) }
    4.44 +                    catch {
    4.45 +                      case exn: Throwable =>
    4.46 +                        GUI.error_dialog(view,
    4.47 +                          "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    4.48 +                    })
    4.49 +                }
    4.50                case _ =>
    4.51              }
    4.52            case _ =>