# HG changeset patch
# User wenzelm
# Date 1373141478 -7200
# Node ID 19d674acb7649eed272ac55fd261d48e1579b6a7
# Parent 97c950217d7f34e838174d7432e122a02ddc6a5b
more release notes according to availability in proper release vs. repository clone;
discontinued generated HTML for files that are accessible in 1 click;
diff -r 97c950217d7f -r 19d674acb764 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle Sat Jul 06 21:51:35 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle Sat Jul 06 22:11:18 2013 +0200
@@ -164,24 +164,6 @@
perl -pi -e "s,/bin/rebaseall.*,/isabelle/rebaseall,g;" \
"$ISABELLE_TARGET/contrib/cygwin/etc/postinstall/autorebase.bat.done"
- for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
- do
- FILE="$ISABELLE_TARGET/$NAME"
- {
- echo ''
- echo ''
- echo ''
- echo ''
- echo ''
- echo "${NAME}"
- echo ''
- echo ''
- echo ''
- perl -w -p -e "s/&/&/g; s//>/g; s/'/'/g; s/\"/"/g;" "$FILE"
- echo '
'
- echo ''
- } > "${FILE}.html"
- done
;;
*)
;;
diff -r 97c950217d7f -r 19d674acb764 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala Sat Jul 06 21:51:35 2013 +0200
+++ b/src/Pure/Tools/doc.scala Sat Jul 06 22:11:18 2013 +0200
@@ -33,18 +33,25 @@
sealed abstract class Entry
case class Section(text: String) extends Entry
case class Doc(name: String, title: String) extends Entry
- case class Text_File(path: Path) extends Entry
+ case class Text_File(name: String, path: Path) extends Entry
private val Section_Entry = new Regex("""^(\S.*)\s*$""")
private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
- private val release_notes =
- List(Section("Release notes"),
- Text_File(Path.explode("~~/ANNOUNCE")),
- Text_File(Path.explode("~~/README")),
- Text_File(Path.explode("~~/NEWS")),
- Text_File(Path.explode("~~/COPYRIGHT")),
- Text_File(Path.explode("~~/CONTRIBUTORS")))
+ private def release_notes(): List[Entry] =
+ {
+ def text_file(name: String): Option[Text_File] =
+ {
+ val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
+ if (path.is_file) Some(Text_File(name, path))
+ else None
+ }
+ val names =
+ List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
+ "contrib/README", "README_REPOSITORY")
+ Section("Release notes") ::
+ (for (name <- names; entry <- text_file(name)) yield entry)
+ }
def contents(): List[Entry] =
(for {
@@ -55,7 +62,7 @@
case Doc_Entry(name, title) => Some(Doc(name, title))
case _ => None
}
- } yield entry) ::: release_notes
+ } yield entry) ::: release_notes()
/* view */
diff -r 97c950217d7f -r 19d674acb764 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala Sat Jul 06 21:51:35 2013 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Jul 06 22:11:18 2013 +0200
@@ -29,9 +29,9 @@
"" + HTML.encode(name) + ": " + HTML.encode(title) + ""
}
- private case class Text_File(path: Path)
+ private case class Text_File(name: String, path: Path)
{
- override def toString = path.base.implode
+ override def toString = name
}
private val root = new DefaultMutableTreeNode
@@ -41,9 +41,9 @@
case Doc.Doc(name, title) =>
root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
.add(new DefaultMutableTreeNode(Documentation(name, title)))
- case Doc.Text_File(path: Path) =>
+ case Doc.Text_File(name: String, path: Path) =>
root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
- .add(new DefaultMutableTreeNode(Text_File(path.expand)))
+ .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
}
private def documentation_error(exn: Throwable) {
@@ -65,7 +65,7 @@
default_thread_pool.submit(() =>
try { Doc.view(name) }
catch { case exn: Throwable => documentation_error(exn) })
- case Text_File(path) =>
+ case Text_File(_, path) =>
try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) }
catch { case exn: Throwable => documentation_error(exn) }
case _ =>