--- a/NEWS Sat Sep 26 11:43:25 2020 +0200
+++ b/NEWS Sat Sep 26 14:29:46 2020 +0200
@@ -38,6 +38,9 @@
* Antiquotations @{scala}, @{scala_object}, @{scala_type},
@{scala_method} refer to checked Isabelle/Scala entities.
+* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
+document output is always PDF.
+
*** Pure ***
@@ -158,6 +161,9 @@
*** System ***
+* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
+variable.
+
* The shell function "isabelle_directory" (within etc/settings of
components) augments the list of special directories for persistent
symbolic path names. This improves portability of heap images and
--- a/etc/settings Sat Sep 26 11:43:25 2020 +0200
+++ b/etc/settings Sat Sep 26 14:29:46 2020 +0200
@@ -59,14 +59,12 @@
### Document preparation (cf. isabelle latex/document)
###
-ISABELLE_LATEX="latex -file-line-error"
ISABELLE_PDFLATEX="pdflatex -file-line-error"
ISABELLE_BIBTEX="bibtex"
ISABELLE_MAKEINDEX="makeindex"
ISABELLE_EPSTOPDF="epstopdf"
if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
- ISABELLE_LATEX="latex -c-style-errors"
ISABELLE_PDFLATEX="pdflatex -c-style-errors"
fi
@@ -140,7 +138,6 @@
esac
PDF_VIEWER="$ISABELLE_OPEN"
-DVI_VIEWER="$ISABELLE_OPEN"
###
--- a/lib/Tools/display Sat Sep 26 11:43:25 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: display document (in DVI or PDF format)
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG DOCUMENT"
- echo
- echo " Display DOCUMENT (in DVI or PDF format)."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## main
-
-[ "$#" -ne 1 -o "$1" = "-?" ] && usage
-
-DOCUMENT="$1"; shift
-
-[ -f "$DOCUMENT" ] || fail "Bad document: \"$DOCUMENT\""
-
-case "$DOCUMENT" in
- *.dvi)
- exec "$DVI_VIEWER" "$DOCUMENT"
- ;;
- *.pdf)
- exec "$PDF_VIEWER" "$DOCUMENT"
- ;;
- *)
- fail "Unknown document type: \"$DOCUMENT\"";
-esac
-
--- a/lib/Tools/latex Sat Sep 26 11:43:25 2020 +0200
+++ b/lib/Tools/latex Sat Sep 26 14:29:46 2020 +0200
@@ -13,7 +13,7 @@
echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
echo
echo " Options are:"
- echo " -o FORMAT specify output format: pdf (default), dvi, bbl, idx, sty"
+ echo " -o FORMAT specify output format: pdf (default), bbl, idx, sty"
echo
echo " Run LaTeX (and related tools) on FILE (default root.tex),"
echo " producing the specified output format."
@@ -70,7 +70,6 @@
# operations
-function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_bibtex () {
$ISABELLE_BIBTEX </dev/null "$FILEBASE"
@@ -96,11 +95,6 @@
run_pdflatex
RC="$?"
;;
- dvi)
- check_root && \
- run_latex
- RC="$?"
- ;;
bbl)
check_root && \
run_bibtex
--- a/src/Doc/System/Environment.thy Sat Sep 26 11:43:25 2020 +0200
+++ b/src/Doc/System/Environment.thy Sat Sep 26 14:29:46 2020 +0200
@@ -192,9 +192,9 @@
\<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
@{tool_ref console} interface.
- \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
- @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
- document preparation (see also \secref{sec:tool-latex}).
+ \<^descr>[@{setting_def ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to
+ {\LaTeX} related tools for Isabelle document preparation (see also
+ \secref{sec:tool-latex}).
\<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
that are scanned by @{executable isabelle} for external utility programs
@@ -206,9 +206,6 @@
\<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
\<^verbatim>\<open>pdf\<close> files.
- \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
- \<^verbatim>\<open>dvi\<close> files.
-
\<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
running Isabelle ML process derives an individual directory for temporary
files.
--- a/src/Doc/System/Misc.thy Sat Sep 26 11:43:25 2020 +0200
+++ b/src/Doc/System/Misc.thy Sat Sep 26 14:29:46 2020 +0200
@@ -163,23 +163,6 @@
\<close>
-section \<open>Displaying documents \label{sec:tool-display}\<close>
-
-text \<open>
- The @{tool_def display} tool displays documents in DVI or PDF format:
- @{verbatim [display]
-\<open>Usage: isabelle display DOCUMENT
-
- Display DOCUMENT (in DVI or PDF format).\<close>}
-
- \<^medskip>
- The settings @{setting DVI_VIEWER} and @{setting PDF_VIEWER} determine the
- programs for viewing the corresponding file formats. Normally this opens the
- document via the desktop environment, potentially in an asynchronous manner
- with re-use of previews views.
-\<close>
-
-
section \<open>Viewing documentation \label{sec:tool-doc}\<close>
text \<open>
@@ -192,7 +175,7 @@
If called without arguments, it lists all available documents. Each line
starts with an identifier, followed by a short description. Any of these
identifiers may be specified as arguments, in order to display the
- corresponding document (see also \secref{sec:tool-display}).
+ corresponding document.
\<^medskip>
The @{setting ISABELLE_DOCS} setting specifies the list of directories
--- a/src/Doc/System/Presentation.thy Sat Sep 26 11:43:25 2020 +0200
+++ b/src/Doc/System/Presentation.thy Sat Sep 26 14:29:46 2020 +0200
@@ -153,7 +153,6 @@
Options are:
-d DIR document output directory (default "output/document")
-n NAME document name (default "document")
- -o FORMAT document format: pdf (default), dvi
-t TAGS markup for tagged regions
Prepare the theory session document in document directory, producing the
@@ -172,8 +171,8 @@
will appear in the parent of this directory.
\<^medskip>
- The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
- the default is ``\<^verbatim>\<open>document.pdf\<close>''.
+ Option \<^verbatim>\<open>-n\<close> specifies the resulting document file name, the default is
+ ``\<^verbatim>\<open>document\<close>'' (leading to ``\<^verbatim>\<open>document.pdf\<close>'').
\<^medskip>
The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
@@ -229,7 +228,7 @@
just by providing {\LaTeX} macros in a similar fashion as in
\<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
- For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
+ For proper setup of PDF documents (with hyperlinks and bookmarks),
we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
\<^medskip>
@@ -254,16 +253,16 @@
\<open>Usage: isabelle latex [OPTIONS] [FILE]
Options are:
- -o FORMAT specify output format: pdf (default), dvi, bbl, idx, sty
+ -o FORMAT specify output format: pdf (default), bbl, idx, sty
Run LaTeX (and related tools) on FILE (default root.tex),
producing the specified output format.\<close>}
Appropriate {\LaTeX}-related programs are run on the input file, according
- to the given output format: @{executable latex}, @{executable pdflatex},
- @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable
- makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the
- settings environment (@{setting ISABELLE_PDFLATEX} etc.).
+ to the given output format: @{executable pdflatex}, @{executable bibtex}
+ (for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands
+ are determined from the settings environment (@{setting ISABELLE_PDFLATEX}
+ etc.).
The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
the distribution. This is useful in special situations where the document
--- a/src/Pure/PIDE/session.ML Sat Sep 26 11:43:25 2020 +0200
+++ b/src/Pure/PIDE/session.ML Sat Sep 26 14:29:46 2020 +0200
@@ -46,13 +46,17 @@
(* init *)
+val document =
+ fn "" => false | "false" => false | "pdf" => true
+ | doc => error ("Bad document specification " ^ quote doc);
+
fun init symbols info info_path doc doc_output doc_variants doc_files graph_file
parent (chapter, name) verbose =
(Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
if parent_name <> parent orelse not parent_finished then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
else ({chapter = chapter, name = name}, false));
- Present.init symbols info info_path (if doc = "false" then "" else doc)
+ Present.init symbols info info_path (document doc)
doc_output doc_variants doc_files graph_file (chapter, name) verbose);
--- a/src/Pure/Thy/present.ML Sat Sep 26 11:43:25 2020 +0200
+++ b/src/Pure/Thy/present.ML Sat Sep 26 14:29:46 2020 +0200
@@ -10,7 +10,7 @@
val theory_qualifier: theory -> string
val document_option: Options.T -> {enabled: bool, disabled: bool}
val document_variants: Options.T -> (string * string) list
- val init: HTML.symbols -> bool -> Path.T -> string -> string -> (string * string) list ->
+ val init: HTML.symbols -> bool -> Path.T -> bool -> string -> (string * string) list ->
(Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
val finish: unit -> unit
val theory_output: theory -> string list -> unit
@@ -31,6 +31,7 @@
val readme_html_path = Path.basic "README.html";
val doc_indexN = "session";
val session_graph_path = Path.basic "session_graph.pdf";
+fun document_path name = Path.basic name |> Path.ext "pdf";
fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));
@@ -123,14 +124,14 @@
type session_info =
{symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool,
- doc_format: string, doc_output: Path.T option, doc_files: (Path.T * Path.T) list,
+ document: bool, doc_output: Path.T option, doc_files: (Path.T * Path.T) list,
graph_file: Path.T, documents: (string * string) list, verbose: bool, readme: Path.T option};
fun make_session_info
- (symbols, name, chapter, info_path, info, doc_format, doc_output, doc_files,
+ (symbols, name, chapter, info_path, info, document, doc_output, doc_files,
graph_file, documents, verbose, readme) =
{symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info,
- doc_format = doc_format, doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
+ document = document, doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
documents = documents, verbose = verbose, readme = readme}: session_info;
@@ -175,21 +176,21 @@
(* init session *)
-fun init symbols info info_path doc document_output doc_variants doc_files graph_file
+fun init symbols info info_path document document_output doc_variants doc_files graph_file
(chapter, name) verbose =
let
val doc_output =
if document_output = "" then NONE else SOME (Path.explode document_output);
- val documents = if doc = "" orelse null doc_files then [] else doc_variants;
+ val documents = if not document orelse null doc_files then [] else doc_variants;
val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
val docs =
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
- map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
+ map (fn (name, _) => (Url.File (document_path name), name)) documents;
in
session_info :=
- SOME (make_session_info (symbols, name, chapter, info_path, info, doc,
+ SOME (make_session_info (symbols, name, chapter, info_path, info, document,
doc_output, doc_files, graph_file, documents, verbose, readme));
Synchronized.change browser_info (K empty_browser_info);
add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs)
@@ -198,12 +199,12 @@
(* isabelle tool wrappers *)
-fun isabelle_document {verbose} format name tags dir =
+fun isabelle_document {verbose} doc_name tags dir =
let
val script =
- "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
- " -n " ^ Bash.string name ^ (if tags = "" then "" else " -t " ^ Bash.string tags);
- val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
+ "isabelle document -d " ^ File.bash_path dir ^ " -n " ^ Bash.string doc_name ^
+ (if tags = "" then "" else " -t " ^ Bash.string tags);
+ val doc_path = Path.appends [dir, Path.parent, document_path doc_name];
val _ = if verbose then writeln script else ();
val {out, err, rc, ...} = Bash.process script;
val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
@@ -223,7 +224,7 @@
write_tex (index_buffer tex_index) doc_indexN path;
fun finish () =
- with_session_info () (fn {name, chapter, info, info_path, doc_format,
+ with_session_info () (fn {name, chapter, info, info_path, document,
doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
let
val {theories, tex_index, html_index} = Synchronized.value browser_info;
@@ -264,7 +265,7 @@
write_tex (fold Buffer.add tex_source Buffer.empty) a doc_dir) thys;
in
fn () =>
- (isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (),
+ (isabelle_document {verbose = true} doc_name tags doc_dir before purge (),
fn doc =>
if verbose orelse not backdrop then
Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
--- a/src/Pure/Thy/present.scala Sat Sep 26 11:43:25 2020 +0200
+++ b/src/Pure/Thy/present.scala Sat Sep 26 14:29:46 2020 +0200
@@ -196,9 +196,9 @@
/** build document **/
+ val document_format = "pdf"
+
val default_document_name = "document"
- val default_document_format = "pdf"
- val document_formats = List("pdf", "dvi")
def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name)
def document_tags(tags: List[String]): String =
@@ -215,15 +215,11 @@
def build_document(
document_name: String = default_document_name,
- document_format: String = default_document_format,
document_dir: Option[Path] = None,
tags: List[String] = Nil)
{
val document_target = Path.parent + Path.explode(document_name).ext(document_format)
- if (!document_formats.contains(document_format))
- error("Bad document output format: " + quote(document_format))
-
val dir = document_dir getOrElse default_document_dir(document_name)
if (!dir.is_dir) error("Bad document output directory " + dir)
@@ -288,7 +284,6 @@
{
var document_dir: Option[Path] = None
var document_name = default_document_name
- var document_format = default_document_format
var tags: List[String] = Nil
val getopts = Getopts("""
@@ -298,9 +293,6 @@
-d DIR document output directory (default """ +
default_document_dir(default_document_name) + """)
-n NAME document name (default """ + quote(default_document_name) + """)
- -o FORMAT document format: """ +
- commas(document_formats.map(fmt =>
- fmt + (if (fmt == default_document_format) " (default)" else ""))) + """
-t TAGS markup for tagged regions
Prepare the theory session document in document directory, producing the
@@ -308,15 +300,13 @@
""",
"d:" -> (arg => document_dir = Some(Path.explode(arg))),
"n:" -> (arg => document_name = arg),
- "o:" -> (arg => document_format = arg),
"t:" -> (arg => tags = space_explode(',', arg)))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
try {
- build_document(document_dir = document_dir, document_name = document_name,
- document_format = document_format, tags = tags)
+ build_document(document_dir = document_dir, document_name = document_name, tags = tags)
}
catch { case ERROR(msg) => Output.writeln(msg); sys.exit(2) }
})