slightly improved "isabelle doc" based on Isabelle/Scala;
authorwenzelm
Tue Jun 25 12:17:19 2013 +0200 (2013-06-25)
changeset 524442cfe6656d6d6
parent 52443 725916b7dee5
child 52445 18a720984855
slightly improved "isabelle doc" based on Isabelle/Scala;
updated documentation of "isabelle display";
lib/Tools/doc
src/Doc/System/Misc.thy
src/Pure/System/doc.scala
src/Pure/Tools/doc.scala
src/Pure/build-jars
src/Pure/library.scala
     1.1 --- a/lib/Tools/doc	Tue Jun 25 11:41:16 2013 +0200
     1.2 +++ b/lib/Tools/doc	Tue Jun 25 12:17:19 2013 +0200
     1.3 @@ -10,9 +10,9 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: isabelle $PRG [DOC]"
     1.8 +  echo "Usage: isabelle $PRG [DOC ...]"
     1.9    echo
    1.10 -  echo "  View Isabelle documentation DOC, or show list of available documents."
    1.11 +  echo "  View Isabelle documentation."
    1.12    echo
    1.13    exit 1
    1.14  }
    1.15 @@ -26,31 +26,12 @@
    1.16  
    1.17  ## args
    1.18  
    1.19 -DOC=""
    1.20 -[ "$#" -ge 1 ] && { DOC="$1"; shift; }
    1.21 -
    1.22 -[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
    1.23 +[ "$#" -eq 1 -a "$1" = "-?" ] && usage
    1.24  
    1.25  
    1.26  ## main
    1.27  
    1.28 -splitarray ":" "$ISABELLE_DOCS"; DOCS=("${SPLITARRAY[@]}")
    1.29 +isabelle_admin_build jars || exit $?
    1.30  
    1.31 -if [ -z "$DOC" ]; then
    1.32 -  for DIR in "${DOCS[@]}"
    1.33 -  do
    1.34 -    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
    1.35 -    [ -f "$DIR/Contents" ] && cat "$DIR/Contents"
    1.36 -  done
    1.37 -else
    1.38 -  for DIR in "${DOCS[@]}"
    1.39 -  do
    1.40 -    [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\""
    1.41 -    for FMT in "$ISABELLE_DOC_FORMAT" dvi
    1.42 -    do
    1.43 -      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
    1.44 -    done
    1.45 -  done
    1.46 -  fail "Missing Isabelle documentation: \"$DOC\""
    1.47 -fi
    1.48 +"$ISABELLE_TOOL" java isabelle.Doc "$@"
    1.49  
     2.1 --- a/src/Doc/System/Misc.thy	Tue Jun 25 11:41:16 2013 +0200
     2.2 +++ b/src/Doc/System/Misc.thy	Tue Jun 25 12:17:19 2013 +0200
     2.3 @@ -60,7 +60,7 @@
     2.4  *}
     2.5  
     2.6  
     2.7 -section {* Displaying documents *}
     2.8 +section {* Displaying documents \label{sec:tool-display} *}
     2.9  
    2.10  text {* The @{tool_def display} tool displays documents in DVI or PDF
    2.11    format:
    2.12 @@ -70,33 +70,35 @@
    2.13    Options are:
    2.14      -c           cleanup -- remove FILE after use
    2.15  
    2.16 -  Display document FILE (in DVI format).
    2.17 +  Display document FILE (in DVI or PDF format).
    2.18  \end{ttbox}
    2.19  
    2.20    \medskip The @{verbatim "-c"} option causes the input file to be
    2.21 -  removed after use.  The program for viewing @{verbatim dvi} files is
    2.22 -  determined by the @{setting DVI_VIEWER} setting.
    2.23 +  removed after use.
    2.24 +
    2.25 +  \medskip The settings @{setting DVI_VIEWER} and @{setting
    2.26 +  PDF_VIEWER} determine the programs for viewing the corresponding
    2.27 +  file formats.
    2.28  *}
    2.29  
    2.30  
    2.31  section {* Viewing documentation \label{sec:tool-doc} *}
    2.32  
    2.33  text {*
    2.34 -  The @{tool_def doc} tool displays online documentation:
    2.35 +  The @{tool_def doc} tool displays Isabelle documentation:
    2.36  \begin{ttbox}
    2.37 -Usage: isabelle doc [DOC]
    2.38 +Usage: isabelle doc [DOC ...]
    2.39  
    2.40 -  View Isabelle documentation DOC, or show list of available documents.
    2.41 +  View Isabelle documentation.
    2.42  \end{ttbox}
    2.43    If called without arguments, it lists all available documents. Each
    2.44    line starts with an identifier, followed by a short description. Any
    2.45 -  of these identifiers may be specified as the first argument in order
    2.46 -  to have the corresponding document displayed.
    2.47 +  of these identifiers may be specified as arguments, in order to
    2.48 +  display the corresponding document (see also
    2.49 +  \secref{sec:tool-display}).
    2.50  
    2.51    \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
    2.52    directories (separated by colons) to be scanned for documentations.
    2.53 -  The program for viewing @{verbatim dvi} files is determined by the
    2.54 -  @{setting DVI_VIEWER} setting.
    2.55  *}
    2.56  
    2.57  
     3.1 --- a/src/Pure/System/doc.scala	Tue Jun 25 11:41:16 2013 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,69 +0,0 @@
     3.4 -/*  Title:      Pure/System/doc.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -View Isabelle documentation (see also "isabelle doc").
     3.8 -*/
     3.9 -
    3.10 -package isabelle
    3.11 -
    3.12 -
    3.13 -import scala.util.matching.Regex
    3.14 -
    3.15 -
    3.16 -object Doc
    3.17 -{
    3.18 -  /* dirs */
    3.19 -
    3.20 -  def dirs(): List[Path] =
    3.21 -    Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
    3.22 -      if (dir.is_dir) dir
    3.23 -      else error("Bad documentation directory: " + dir))
    3.24 -
    3.25 -
    3.26 -  /* contents */
    3.27 -
    3.28 -  sealed abstract class Entry
    3.29 -  case class Section(text: String) extends Entry
    3.30 -  case class Doc(name: String, title: String) extends Entry
    3.31 -
    3.32 -  def contents(): List[Entry] =
    3.33 -  {
    3.34 -    val Section_Entry = new Regex("""^(\S.*)\s*$""")
    3.35 -    val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    3.36 -
    3.37 -    for {
    3.38 -      dir <- dirs()
    3.39 -      catalog = dir + Path.basic("Contents")
    3.40 -      if catalog.is_file
    3.41 -      line <- split_lines(File.read(catalog))
    3.42 -      entry <-
    3.43 -        line match {
    3.44 -          case Section_Entry(text) => Some(Section(text))
    3.45 -          case Doc_Entry(name, title) => Some(Doc(name, title))
    3.46 -          case _ => None
    3.47 -        }
    3.48 -    } yield entry
    3.49 -  }
    3.50 -
    3.51 -
    3.52 -  /* view */
    3.53 -
    3.54 -  def view(name: String)
    3.55 -  {
    3.56 -    val formats = List(Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT"), "dvi")
    3.57 -    val docs =
    3.58 -      for {
    3.59 -        dir <- dirs()
    3.60 -        fmt <- formats
    3.61 -        doc = name + "." + fmt
    3.62 -        if (dir + Path.basic(doc)).is_file
    3.63 -      } yield (dir, doc)
    3.64 -    docs match {
    3.65 -      case (dir, doc) :: _ =>
    3.66 -        Isabelle_System.bash_env(dir.file, null,
    3.67 -          "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
    3.68 -      case Nil => error("Missing Isabelle documentation: " + quote(name))
    3.69 -    }
    3.70 -  }
    3.71 -}
    3.72 -
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Tools/doc.scala	Tue Jun 25 12:17:19 2013 +0200
     4.3 @@ -0,0 +1,84 @@
     4.4 +/*  Title:      Pure/Tools/doc.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +View Isabelle documentation.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +import scala.util.matching.Regex
    4.14 +
    4.15 +
    4.16 +object Doc
    4.17 +{
    4.18 +  /* dirs */
    4.19 +
    4.20 +  def dirs(): List[Path] =
    4.21 +    Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
    4.22 +      if (dir.is_dir) dir
    4.23 +      else error("Bad documentation directory: " + dir))
    4.24 +
    4.25 +
    4.26 +  /* contents */
    4.27 +
    4.28 +  private def contents_lines(): List[String] =
    4.29 +    for {
    4.30 +      dir <- dirs()
    4.31 +      catalog = dir + Path.basic("Contents")
    4.32 +      if catalog.is_file
    4.33 +      line <- split_lines(Library.trim_line(File.read(catalog)))
    4.34 +    } yield line
    4.35 +
    4.36 +  sealed abstract class Entry
    4.37 +  case class Section(text: String) extends Entry
    4.38 +  case class Doc(name: String, title: String) extends Entry
    4.39 +
    4.40 +  private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    4.41 +  private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    4.42 +
    4.43 +  def contents(): List[Entry] =
    4.44 +    for {
    4.45 +      line <- contents_lines()
    4.46 +      entry <-
    4.47 +        line match {
    4.48 +          case Section_Entry(text) => Some(Section(text))
    4.49 +          case Doc_Entry(name, title) => Some(Doc(name, title))
    4.50 +          case _ => None
    4.51 +        }
    4.52 +    } yield entry
    4.53 +
    4.54 +
    4.55 +  /* view */
    4.56 +
    4.57 +  def view(name: String)
    4.58 +  {
    4.59 +    val formats = List(Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT"), "dvi")
    4.60 +    val docs =
    4.61 +      for {
    4.62 +        dir <- dirs()
    4.63 +        fmt <- formats
    4.64 +        doc = name + "." + fmt
    4.65 +        if (dir + Path.basic(doc)).is_file
    4.66 +      } yield (dir, doc)
    4.67 +    docs match {
    4.68 +      case (dir, doc) :: _ =>
    4.69 +        Isabelle_System.bash_env(dir.file, null,
    4.70 +          "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
    4.71 +      case Nil => error("Missing Isabelle documentation: " + quote(name))
    4.72 +    }
    4.73 +  }
    4.74 +
    4.75 +
    4.76 +  /* command line entry point */
    4.77 +
    4.78 +  def main(args: Array[String])
    4.79 +  {
    4.80 +    Command_Line.tool {
    4.81 +      if (args.isEmpty) Console.println(cat_lines(contents_lines()))
    4.82 +      else args.foreach(view)
    4.83 +      0
    4.84 +    }
    4.85 +  }
    4.86 +}
    4.87 +
     5.1 --- a/src/Pure/build-jars	Tue Jun 25 11:41:16 2013 +0200
     5.2 +++ b/src/Pure/build-jars	Tue Jun 25 12:17:19 2013 +0200
     5.3 @@ -41,7 +41,6 @@
     5.4    PIDE/yxml.scala
     5.5    System/color_value.scala
     5.6    System/command_line.scala
     5.7 -  System/doc.scala
     5.8    System/event_bus.scala
     5.9    System/gui.scala
    5.10    System/gui_setup.scala
    5.11 @@ -68,6 +67,7 @@
    5.12    Thy/thy_syntax.scala
    5.13    Tools/build.scala
    5.14    Tools/build_dialog.scala
    5.15 +  Tools/doc.scala
    5.16    Tools/keywords.scala
    5.17    Tools/main.scala
    5.18    Tools/ml_statistics.scala
     6.1 --- a/src/Pure/library.scala	Tue Jun 25 11:41:16 2013 +0200
     6.2 +++ b/src/Pure/library.scala	Tue Jun 25 12:17:19 2013 +0200
     6.3 @@ -107,6 +107,11 @@
     6.4    def try_unprefix(prfx: String, s: String): Option[String] =
     6.5      if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
     6.6  
     6.7 +  def trim_line(s: String): String =
     6.8 +    if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
     6.9 +    else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
    6.10 +    else s
    6.11 +
    6.12  
    6.13    /* quote */
    6.14