# HG changeset patch
# User wenzelm
# Date 1373215394 -7200
# Node ID 09e52d4a850ade6f43b37e14d44625cea8c114dd
# Parent  80257685652722a490f2e52cb8f961f6c942e916
discontinued obsolete "isabelle print";

diff -r 802576856527 -r 09e52d4a850a NEWS
--- a/NEWS	Sun Jul 07 18:34:29 2013 +0200
+++ b/NEWS	Sun Jul 07 18:43:14 2013 +0200
@@ -307,6 +307,9 @@
 * Discontinued obsolete isabelle-process options -f and -u (former
 administrative aliases of option -e).  Minor INCOMPATIBILITY.
 
+* Discontinued obsolete isabelle print tool, and PRINT_COMMAND
+settings variable.
+
 * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
 specify global resources of the JVM process run by isabelle build.
 
diff -r 802576856527 -r 09e52d4a850a etc/settings
--- a/etc/settings	Sun Jul 07 18:34:29 2013 +0200
+++ b/etc/settings	Sun Jul 07 18:43:14 2013 +0200
@@ -116,10 +116,6 @@
 #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
 
 
-# Printer spool command for PS files
-PRINT_COMMAND=lp
-
-
 ###
 ### Rendering information
 ###
diff -r 802576856527 -r 09e52d4a850a lib/Tools/print
--- a/lib/Tools/print	Sun Jul 07 18:34:29 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: print document
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] FILE"
-  echo
-  echo "  Options are:"
-  echo "    -c           cleanup -- remove FILE after use"
-  echo
-  echo "  Print document FILE."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-CLEAN=""
-
-while getopts "c" OPT
-do
-  case "$OPT" in
-    c)
-      CLEAN=true
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 1 ] && usage
-
-FILE="$1"; shift
-
-
-## main
-
-[ -f "$FILE" ] || fail "Bad file: $FILE"
-$PRINT_COMMAND "$FILE"
-[ -n "$CLEAN" ] && rm -f "$FILE"
diff -r 802576856527 -r 09e52d4a850a src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Sun Jul 07 18:34:29 2013 +0200
+++ b/src/Doc/System/Basics.thy	Sun Jul 07 18:43:14 2013 +0200
@@ -277,9 +277,6 @@
   \item[@{setting_def DVI_VIEWER}] specifies the command-line to be
   used for displaying @{verbatim dvi} files.
   
-  \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
-  spool command, which is expected to accept @{verbatim ps} files.
-  
   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
   prefix from which any running @{executable "isabelle-process"}
   derives an individual directory for temporary files.  The default is
diff -r 802576856527 -r 09e52d4a850a src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sun Jul 07 18:34:29 2013 +0200
+++ b/src/Doc/System/Misc.thy	Sun Jul 07 18:43:14 2013 +0200
@@ -238,25 +238,6 @@
   using this template.  *}
 
 
-section {* Printing documents *}
-
-text {*
-  The @{tool_def print} tool prints documents:
-\begin{ttbox}
-Usage: isabelle print [OPTIONS] FILE
-
-  Options are:
-    -c           cleanup -- remove FILE after use
-
-  Print document FILE.
-\end{ttbox}
-
-  The @{verbatim "-c"} option causes the input file to be removed
-  after use.  The printer spool command is determined by the @{setting
-  PRINT_COMMAND} setting.
-*}
-
-
 section {* Remove awkward symbol names from theory sources *}
 
 text {*