src/Pure/Tools/doc.scala
changeset 56425 d12653fbd5b1
parent 56424 7032378cc097
child 56631 89269bb8e7ca
equal deleted inserted replaced
56424:7032378cc097 56425:d12653fbd5b1
    52   private def examples(): List[Entry] =
    52   private def examples(): List[Entry] =
    53     Section("Examples", true) ::
    53     Section("Examples", true) ::
    54       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
    54       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
    55         text_file(file) match {
    55         text_file(file) match {
    56           case Some(entry) => entry
    56           case Some(entry) => entry
    57           case None => error("Bad ISABELLE_DOCS_EXAMPLES entry: " + file)
    57           case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
    58         })
    58         })
    59 
    59 
    60   def contents(): List[Entry] =
    60   def contents(): List[Entry] =
    61     (for {
    61     (for {
    62       (dir, line) <- contents_lines()
    62       (dir, line) <- contents_lines()
    89   /* command line entry point */
    89   /* command line entry point */
    90 
    90 
    91   def main(args: Array[String])
    91   def main(args: Array[String])
    92   {
    92   {
    93     Command_Line.tool {
    93     Command_Line.tool {
       
    94       val entries = contents()
    94       if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
    95       if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
    95       else {
    96       else {
    96         val entries = contents()
       
    97         args.foreach(arg =>
    97         args.foreach(arg =>
    98           entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
    98           entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
    99             case Some(path) => view(path)
    99             case Some(path) => view(path)
   100             case None => error("No Isabelle documentation entry: " + quote(arg))
   100             case None => error("No Isabelle documentation entry: " + quote(arg))
   101           }
   101           }