# HG changeset patch
# User wenzelm
# Date 1459715476 -7200
# Node ID 5560905a32ae562448bf8828f5de46e232bf997c
# Parent  85024c0e953df333d442a45b61c2489287d17e71
prefer internal tool;

diff -r 85024c0e953d -r 5560905a32ae lib/Tools/doc
--- a/lib/Tools/doc	Sun Apr 03 22:15:40 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: view Isabelle documentation
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Doc "$@"
diff -r 85024c0e953d -r 5560905a32ae src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:15:40 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:31:16 2016 +0200
@@ -68,6 +68,8 @@
             args => Command_Line.tool0 { isabelle_tool.body(args) }))
     }
 
+  register(Doc.isabelle_tool)
+
 
   /* command line entry point */
 
diff -r 85024c0e953d -r 5560905a32ae src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sun Apr 03 22:15:40 2016 +0200
+++ b/src/Pure/Tools/doc.scala	Sun Apr 03 22:31:16 2016 +0200
@@ -91,28 +91,26 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
+  val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args =>
   {
-    Command_Line.tool0 {
-      val getopts = Getopts("""
+    val getopts = Getopts("""
 Usage: isabelle doc [DOC ...]
 
   View Isabelle documentation.
 """)
-      val docs = getopts(args)
+    val docs = getopts(args)
 
-      val entries = contents()
-      if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
-      else {
-        docs.foreach(doc =>
-          entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
-            case Some(path) => view(path)
-            case None => error("No Isabelle documentation entry: " + quote(doc))
-          }
-        )
-      }
+    val entries = contents()
+    if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
+    else {
+      docs.foreach(doc =>
+        entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
+          case Some(path) => view(path)
+          case None => error("No Isabelle documentation entry: " + quote(doc))
+        }
+      )
     }
-  }
+  })
 }