prefer internal tool;
authorwenzelm
Sun Apr 03 22:31:16 2016 +0200 (2016-04-03)
changeset 628315560905a32ae
parent 62830 85024c0e953d
child 62832 c1410bcf6e87
prefer internal tool;
lib/Tools/doc
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/doc.scala
     1.1 --- a/lib/Tools/doc	Sun Apr 03 22:15:40 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,9 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Author: Markus Wenzel, TU Muenchen
     1.7 -#
     1.8 -# DESCRIPTION: view Isabelle documentation
     1.9 -
    1.10 -isabelle_admin_build jars || exit $?
    1.11 -
    1.12 -exec isabelle java isabelle.Doc "$@"
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:15:40 2016 +0200
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:31:16 2016 +0200
     2.3 @@ -68,6 +68,8 @@
     2.4              args => Command_Line.tool0 { isabelle_tool.body(args) }))
     2.5      }
     2.6  
     2.7 +  register(Doc.isabelle_tool)
     2.8 +
     2.9  
    2.10    /* command line entry point */
    2.11  
     3.1 --- a/src/Pure/Tools/doc.scala	Sun Apr 03 22:15:40 2016 +0200
     3.2 +++ b/src/Pure/Tools/doc.scala	Sun Apr 03 22:31:16 2016 +0200
     3.3 @@ -91,28 +91,26 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* command line entry point */
     3.8 +  /* Isabelle tool wrapper */
     3.9  
    3.10 -  def main(args: Array[String])
    3.11 +  val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args =>
    3.12    {
    3.13 -    Command_Line.tool0 {
    3.14 -      val getopts = Getopts("""
    3.15 +    val getopts = Getopts("""
    3.16  Usage: isabelle doc [DOC ...]
    3.17  
    3.18    View Isabelle documentation.
    3.19  """)
    3.20 -      val docs = getopts(args)
    3.21 +    val docs = getopts(args)
    3.22  
    3.23 -      val entries = contents()
    3.24 -      if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
    3.25 -      else {
    3.26 -        docs.foreach(doc =>
    3.27 -          entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
    3.28 -            case Some(path) => view(path)
    3.29 -            case None => error("No Isabelle documentation entry: " + quote(doc))
    3.30 -          }
    3.31 -        )
    3.32 -      }
    3.33 +    val entries = contents()
    3.34 +    if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
    3.35 +    else {
    3.36 +      docs.foreach(doc =>
    3.37 +        entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
    3.38 +          case Some(path) => view(path)
    3.39 +          case None => error("No Isabelle documentation entry: " + quote(doc))
    3.40 +        }
    3.41 +      )
    3.42      }
    3.43 -  }
    3.44 +  })
    3.45  }