# HG changeset patch # User wenzelm # Date 1601123386 -7200 # Node ID 564012e31db17aa7d7a56fac38706787b21b6b69 # Parent aa14f630d8ef841fe3135c38d3d7d214f5268c50 discontinued obsolete DVI document format and related settings/tools; diff -r aa14f630d8ef -r 564012e31db1 NEWS --- 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 diff -r aa14f630d8ef -r 564012e31db1 etc/settings --- 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" ### diff -r aa14f630d8ef -r 564012e31db1 lib/Tools/display --- 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 - diff -r aa14f630d8ef -r 564012e31db1 lib/Tools/latex --- 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 [@{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>\pdf\ files. - \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying - \<^verbatim>\dvi\ files. - \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\\<^sup>*\] is the prefix from which any running Isabelle ML process derives an individual directory for temporary files. diff -r aa14f630d8ef -r 564012e31db1 src/Doc/System/Misc.thy --- 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 @@ \ -section \Displaying documents \label{sec:tool-display}\ - -text \ - The @{tool_def display} tool displays documents in DVI or PDF format: - @{verbatim [display] -\Usage: isabelle display DOCUMENT - - Display DOCUMENT (in DVI or PDF format).\} - - \<^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. -\ - - section \Viewing documentation \label{sec:tool-doc}\ text \ @@ -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 diff -r aa14f630d8ef -r 564012e31db1 src/Doc/System/Presentation.thy --- 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>\-n\ and \<^verbatim>\-o\ option specify the final output file name and format, - the default is ``\<^verbatim>\document.pdf\''. + Option \<^verbatim>\-n\ specifies the resulting document file name, the default is + ``\<^verbatim>\document\'' (leading to ``\<^verbatim>\document.pdf\''). \<^medskip> The \<^verbatim>\-t\ 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>\~~/lib/texinputs/isabellesym.sty\ 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>\~~/lib/texinputs/pdfsetup.sty\ as well. \<^medskip> @@ -254,16 +253,16 @@ \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.\} 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>\bbl\), and @{executable - makeindex} (for \<^verbatim>\idx\). The actual commands are determined from the - settings environment (@{setting ISABELLE_PDFLATEX} etc.). + to the given output format: @{executable pdflatex}, @{executable bibtex} + (for \<^verbatim>\bbl\), and @{executable makeindex} (for \<^verbatim>\idx\). The actual commands + are determined from the settings environment (@{setting ISABELLE_PDFLATEX} + etc.). The \<^verbatim>\sty\ output format causes the Isabelle style files to be updated from the distribution. This is useful in special situations where the document diff -r aa14f630d8ef -r 564012e31db1 src/Pure/PIDE/session.ML --- 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); diff -r aa14f630d8ef -r 564012e31db1 src/Pure/Thy/present.ML --- 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") diff -r aa14f630d8ef -r 564012e31db1 src/Pure/Thy/present.scala --- 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) } })