# HG changeset patch
# User wenzelm
# Date 1372011121 -7200
# Node ID 9d1cc9a22177cdb10d0e8a3cbe11c1f605044fc5
# Parent  81e27230a8b71c993b77908f42efb65f56fb2f46
Scala version of "isabelle doc";
discontinued slightly odd / unused ">>" comments within Contents (see also b077b79061b6);

diff -r 81e27230a8b7 -r 9d1cc9a22177 lib/Tools/doc
--- a/lib/Tools/doc	Sun Jun 23 18:11:38 2013 +0200
+++ b/lib/Tools/doc	Sun Jun 23 20:12:01 2013 +0200
@@ -39,18 +39,18 @@
 if [ -z "$DOC" ]; then
   for DIR in "${DOCS[@]}"
   do
-    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
-    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
+    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
+    [ -f "$DIR/Contents" ] && cat "$DIR/Contents"
   done
 else
   for DIR in "${DOCS[@]}"
   do
-    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
+    [ -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 "Unknown Isabelle document: $DOC"  
+  fail "Missing Isabelle documentation: \"$DOC\""
 fi
 
diff -r 81e27230a8b7 -r 9d1cc9a22177 src/Pure/System/doc.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/doc.scala	Sun Jun 23 20:12:01 2013 +0200
@@ -0,0 +1,68 @@
+/*  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) + " &")
+      case Nil => error("Missing Isabelle documentation: " + quote(name))
+    }
+  }
+}
+
diff -r 81e27230a8b7 -r 9d1cc9a22177 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Jun 23 18:11:38 2013 +0200
+++ b/src/Pure/build-jars	Sun Jun 23 20:12:01 2013 +0200
@@ -41,6 +41,7 @@
   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