src/Pure/Tools/doc.scala
changeset 62438 42e13a4f52f5
parent 61157 13f4056c42d7
child 62454 38c89353b349
     1.1 --- a/src/Pure/Tools/doc.scala	Sat Feb 27 19:47:53 2016 +0100
     1.2 +++ b/src/Pure/Tools/doc.scala	Sat Feb 27 19:57:36 2016 +0100
     1.3 @@ -96,13 +96,20 @@
     1.4    def main(args: Array[String])
     1.5    {
     1.6      Command_Line.tool0 {
     1.7 +      val getopts = Getopts(() => """
     1.8 +Usage: isabelle doc [DOC ...]
     1.9 +
    1.10 +  View Isabelle documentation.
    1.11 +""")
    1.12 +      val docs = getopts(args)
    1.13 +
    1.14        val entries = contents()
    1.15 -      if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
    1.16 +      if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
    1.17        else {
    1.18 -        args.foreach(arg =>
    1.19 -          entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
    1.20 +        docs.foreach(doc =>
    1.21 +          entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
    1.22              case Some(path) => view(path)
    1.23 -            case None => error("No Isabelle documentation entry: " + quote(arg))
    1.24 +            case None => error("No Isabelle documentation entry: " + quote(doc))
    1.25            }
    1.26          )
    1.27        }