# HG changeset patch
# User wenzelm
# Date 1372155439 -7200
# Node ID 2cfe6656d6d6becf8275a703a40bb8bbd26fe624
# Parent  725916b7dee57fd6bb3404bc0fe0efcf3ab05d0f
slightly improved "isabelle doc" based on Isabelle/Scala;
updated documentation of "isabelle display";

diff -r 725916b7dee5 -r 2cfe6656d6d6 lib/Tools/doc
--- a/lib/Tools/doc	Tue Jun 25 11:41:16 2013 +0200
+++ b/lib/Tools/doc	Tue Jun 25 12:17:19 2013 +0200
@@ -10,9 +10,9 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG [DOC]"
+  echo "Usage: isabelle $PRG [DOC ...]"
   echo
-  echo "  View Isabelle documentation DOC, or show list of available documents."
+  echo "  View Isabelle documentation."
   echo
   exit 1
 }
@@ -26,31 +26,12 @@
 
 ## args
 
-DOC=""
-[ "$#" -ge 1 ] && { DOC="$1"; shift; }
-
-[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
+[ "$#" -eq 1 -a "$1" = "-?" ] && usage
 
 
 ## main
 
-splitarray ":" "$ISABELLE_DOCS"; DOCS=("${SPLITARRAY[@]}")
+isabelle_admin_build jars || exit $?
 
-if [ -z "$DOC" ]; then
-  for DIR in "${DOCS[@]}"
-  do
-    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
-    [ -f "$DIR/Contents" ] && cat "$DIR/Contents"
-  done
-else
-  for DIR in "${DOCS[@]}"
-  do
-    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
-    for FMT in "$ISABELLE_DOC_FORMAT" dvi
-    do
-      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
-    done
-  done
-  fail "Missing Isabelle documentation: \"$DOC\""
-fi
+"$ISABELLE_TOOL" java isabelle.Doc "$@"
 
diff -r 725916b7dee5 -r 2cfe6656d6d6 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Tue Jun 25 11:41:16 2013 +0200
+++ b/src/Doc/System/Misc.thy	Tue Jun 25 12:17:19 2013 +0200
@@ -60,7 +60,7 @@
 *}
 
 
-section {* Displaying documents *}
+section {* Displaying documents \label{sec:tool-display} *}
 
 text {* The @{tool_def display} tool displays documents in DVI or PDF
   format:
@@ -70,33 +70,35 @@
   Options are:
     -c           cleanup -- remove FILE after use
 
-  Display document FILE (in DVI format).
+  Display document FILE (in DVI or PDF format).
 \end{ttbox}
 
   \medskip The @{verbatim "-c"} option causes the input file to be
-  removed after use.  The program for viewing @{verbatim dvi} files is
-  determined by the @{setting DVI_VIEWER} setting.
+  removed after use.
+
+  \medskip The settings @{setting DVI_VIEWER} and @{setting
+  PDF_VIEWER} determine the programs for viewing the corresponding
+  file formats.
 *}
 
 
 section {* Viewing documentation \label{sec:tool-doc} *}
 
 text {*
-  The @{tool_def doc} tool displays online documentation:
+  The @{tool_def doc} tool displays Isabelle documentation:
 \begin{ttbox}
-Usage: isabelle doc [DOC]
+Usage: isabelle doc [DOC ...]
 
-  View Isabelle documentation DOC, or show list of available documents.
+  View Isabelle documentation.
 \end{ttbox}
   If called without arguments, it lists all available documents. Each
   line starts with an identifier, followed by a short description. Any
-  of these identifiers may be specified as the first argument in order
-  to have the corresponding document displayed.
+  of these identifiers may be specified as arguments, in order to
+  display the corresponding document (see also
+  \secref{sec:tool-display}).
 
   \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
   directories (separated by colons) to be scanned for documentations.
-  The program for viewing @{verbatim dvi} files is determined by the
-  @{setting DVI_VIEWER} setting.
 *}
 
 
diff -r 725916b7dee5 -r 2cfe6656d6d6 src/Pure/System/doc.scala
--- a/src/Pure/System/doc.scala	Tue Jun 25 11:41:16 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-/*  Title:      Pure/System/doc.scala
-    Author:     Makarius
-
-View Isabelle documentation (see also "isabelle doc").
-*/
-
-package isabelle
-
-
-import scala.util.matching.Regex
-
-
-object Doc
-{
-  /* dirs */
-
-  def dirs(): List[Path] =
-    Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
-      if (dir.is_dir) dir
-      else error("Bad documentation directory: " + dir))
-
-
-  /* contents */
-
-  sealed abstract class Entry
-  case class Section(text: String) extends Entry
-  case class Doc(name: String, title: String) extends Entry
-
-  def contents(): List[Entry] =
-  {
-    val Section_Entry = new Regex("""^(\S.*)\s*$""")
-    val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
-
-    for {
-      dir <- dirs()
-      catalog = dir + Path.basic("Contents")
-      if catalog.is_file
-      line <- split_lines(File.read(catalog))
-      entry <-
-        line match {
-          case Section_Entry(text) => Some(Section(text))
-          case Doc_Entry(name, title) => Some(Doc(name, title))
-          case _ => None
-        }
-    } yield entry
-  }
-
-
-  /* view */
-
-  def view(name: String)
-  {
-    val formats = List(Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT"), "dvi")
-    val docs =
-      for {
-        dir <- dirs()
-        fmt <- formats
-        doc = name + "." + fmt
-        if (dir + Path.basic(doc)).is_file
-      } yield (dir, doc)
-    docs match {
-      case (dir, doc) :: _ =>
-        Isabelle_System.bash_env(dir.file, null,
-          "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
-      case Nil => error("Missing Isabelle documentation: " + quote(name))
-    }
-  }
-}
-
diff -r 725916b7dee5 -r 2cfe6656d6d6 src/Pure/Tools/doc.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/doc.scala	Tue Jun 25 12:17:19 2013 +0200
@@ -0,0 +1,84 @@
+/*  Title:      Pure/Tools/doc.scala
+    Author:     Makarius
+
+View Isabelle documentation.
+*/
+
+package isabelle
+
+
+import scala.util.matching.Regex
+
+
+object Doc
+{
+  /* dirs */
+
+  def dirs(): List[Path] =
+    Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
+      if (dir.is_dir) dir
+      else error("Bad documentation directory: " + dir))
+
+
+  /* contents */
+
+  private def contents_lines(): List[String] =
+    for {
+      dir <- dirs()
+      catalog = dir + Path.basic("Contents")
+      if catalog.is_file
+      line <- split_lines(Library.trim_line(File.read(catalog)))
+    } yield line
+
+  sealed abstract class Entry
+  case class Section(text: String) extends Entry
+  case class Doc(name: String, title: String) extends Entry
+
+  private val Section_Entry = new Regex("""^(\S.*)\s*$""")
+  private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
+
+  def contents(): List[Entry] =
+    for {
+      line <- contents_lines()
+      entry <-
+        line match {
+          case Section_Entry(text) => Some(Section(text))
+          case Doc_Entry(name, title) => Some(Doc(name, title))
+          case _ => None
+        }
+    } yield entry
+
+
+  /* view */
+
+  def view(name: String)
+  {
+    val formats = List(Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT"), "dvi")
+    val docs =
+      for {
+        dir <- dirs()
+        fmt <- formats
+        doc = name + "." + fmt
+        if (dir + Path.basic(doc)).is_file
+      } yield (dir, doc)
+    docs match {
+      case (dir, doc) :: _ =>
+        Isabelle_System.bash_env(dir.file, null,
+          "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
+      case Nil => error("Missing Isabelle documentation: " + quote(name))
+    }
+  }
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool {
+      if (args.isEmpty) Console.println(cat_lines(contents_lines()))
+      else args.foreach(view)
+      0
+    }
+  }
+}
+
diff -r 725916b7dee5 -r 2cfe6656d6d6 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Jun 25 11:41:16 2013 +0200
+++ b/src/Pure/build-jars	Tue Jun 25 12:17:19 2013 +0200
@@ -41,7 +41,6 @@
   PIDE/yxml.scala
   System/color_value.scala
   System/command_line.scala
-  System/doc.scala
   System/event_bus.scala
   System/gui.scala
   System/gui_setup.scala
@@ -68,6 +67,7 @@
   Thy/thy_syntax.scala
   Tools/build.scala
   Tools/build_dialog.scala
+  Tools/doc.scala
   Tools/keywords.scala
   Tools/main.scala
   Tools/ml_statistics.scala
diff -r 725916b7dee5 -r 2cfe6656d6d6 src/Pure/library.scala
--- a/src/Pure/library.scala	Tue Jun 25 11:41:16 2013 +0200
+++ b/src/Pure/library.scala	Tue Jun 25 12:17:19 2013 +0200
@@ -107,6 +107,11 @@
   def try_unprefix(prfx: String, s: String): Option[String] =
     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
 
+  def trim_line(s: String): String =
+    if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
+    else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
+    else s
+
 
   /* quote */