more release notes according to availability in proper release vs. repository clone;
authorwenzelm
Sat Jul 06 22:11:18 2013 +0200 (2013-07-06)
changeset 5254219d674acb764
parent 52541 97c950217d7f
child 52543 6f5678b97c4e
more release notes according to availability in proper release vs. repository clone;
discontinued generated HTML for files that are accessible in 1 click;
Admin/lib/Tools/makedist_bundle
src/Pure/Tools/doc.scala
src/Tools/jEdit/src/documentation_dockable.scala
     1.1 --- a/Admin/lib/Tools/makedist_bundle	Sat Jul 06 21:51:35 2013 +0200
     1.2 +++ b/Admin/lib/Tools/makedist_bundle	Sat Jul 06 22:11:18 2013 +0200
     1.3 @@ -164,24 +164,6 @@
     1.4      perl -pi -e "s,/bin/rebaseall.*,/isabelle/rebaseall,g;" \
     1.5        "$ISABELLE_TARGET/contrib/cygwin/etc/postinstall/autorebase.bat.done"
     1.6  
     1.7 -    for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
     1.8 -    do
     1.9 -      FILE="$ISABELLE_TARGET/$NAME"
    1.10 -      {
    1.11 -        echo '<?xml version="1.0" encoding="utf-8" ?>'
    1.12 -        echo '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">'
    1.13 -        echo '<html xmlns="http://www.w3.org/1999/xhtml">'
    1.14 -        echo '<head>'
    1.15 -        echo '<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>'
    1.16 -        echo "<title>${NAME}</title>"
    1.17 -        echo '</head>'
    1.18 -        echo '<body>'
    1.19 -        echo '<pre>'
    1.20 -        perl -w -p -e "s/&/&amp;/g; s/</&lt;/g; s/>/&gt;/g; s/'/&apos;/g; s/\"/&quot;/g;" "$FILE"
    1.21 -        echo '</pre>'
    1.22 -        echo '</body>'
    1.23 -      } > "${FILE}.html"
    1.24 -    done
    1.25      ;;
    1.26    *)
    1.27      ;;
     2.1 --- a/src/Pure/Tools/doc.scala	Sat Jul 06 21:51:35 2013 +0200
     2.2 +++ b/src/Pure/Tools/doc.scala	Sat Jul 06 22:11:18 2013 +0200
     2.3 @@ -33,18 +33,25 @@
     2.4    sealed abstract class Entry
     2.5    case class Section(text: String) extends Entry
     2.6    case class Doc(name: String, title: String) extends Entry
     2.7 -  case class Text_File(path: Path) extends Entry
     2.8 +  case class Text_File(name: String, path: Path) extends Entry
     2.9  
    2.10    private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    2.11    private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    2.12  
    2.13 -  private val release_notes =
    2.14 -    List(Section("Release notes"),
    2.15 -      Text_File(Path.explode("~~/ANNOUNCE")),
    2.16 -      Text_File(Path.explode("~~/README")),
    2.17 -      Text_File(Path.explode("~~/NEWS")),
    2.18 -      Text_File(Path.explode("~~/COPYRIGHT")),
    2.19 -      Text_File(Path.explode("~~/CONTRIBUTORS")))
    2.20 +  private def release_notes(): List[Entry] =
    2.21 +  {
    2.22 +    def text_file(name: String): Option[Text_File] =
    2.23 +    {
    2.24 +      val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
    2.25 +      if (path.is_file) Some(Text_File(name, path))
    2.26 +      else None
    2.27 +    }
    2.28 +    val names =
    2.29 +      List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
    2.30 +        "contrib/README", "README_REPOSITORY")
    2.31 +    Section("Release notes") ::
    2.32 +      (for (name <- names; entry <- text_file(name)) yield entry)
    2.33 +  }
    2.34  
    2.35    def contents(): List[Entry] =
    2.36      (for {
    2.37 @@ -55,7 +62,7 @@
    2.38            case Doc_Entry(name, title) => Some(Doc(name, title))
    2.39            case _ => None
    2.40          }
    2.41 -    } yield entry) ::: release_notes
    2.42 +    } yield entry) ::: release_notes()
    2.43  
    2.44  
    2.45    /* view */
     3.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Jul 06 21:51:35 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Jul 06 22:11:18 2013 +0200
     3.3 @@ -29,9 +29,9 @@
     3.4        "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
     3.5    }
     3.6  
     3.7 -  private case class Text_File(path: Path)
     3.8 +  private case class Text_File(name: String, path: Path)
     3.9    {
    3.10 -    override def toString = path.base.implode
    3.11 +    override def toString = name
    3.12    }
    3.13  
    3.14    private val root = new DefaultMutableTreeNode
    3.15 @@ -41,9 +41,9 @@
    3.16      case Doc.Doc(name, title) =>
    3.17        root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    3.18          .add(new DefaultMutableTreeNode(Documentation(name, title)))
    3.19 -    case Doc.Text_File(path: Path) =>
    3.20 +    case Doc.Text_File(name: String, path: Path) =>
    3.21        root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    3.22 -        .add(new DefaultMutableTreeNode(Text_File(path.expand)))
    3.23 +        .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
    3.24    }
    3.25  
    3.26    private def documentation_error(exn: Throwable) {
    3.27 @@ -65,7 +65,7 @@
    3.28                  default_thread_pool.submit(() =>
    3.29                    try { Doc.view(name) }
    3.30                    catch { case exn: Throwable => documentation_error(exn) })
    3.31 -              case Text_File(path) =>
    3.32 +              case Text_File(_, path) =>
    3.33                    try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) }
    3.34                    catch { case exn: Throwable => documentation_error(exn) }
    3.35                case _ =>