--- a/NEWS Sun Dec 10 14:50:44 2017 +0100
+++ b/NEWS Sun Dec 10 18:31:41 2017 +0100
@@ -86,7 +86,9 @@
* Document preparation with skip_proofs option now preserves the content
more accurately: only terminal proof steps ('by' etc.) are skipped.
-* More explicit errors from latex process.
+* Command-line tool "isabelle document" has been re-implemented in
+Isabelle/Scala, with simplified arguments and explicit errors from the
+latex process. Minor INCOMPATIBILITY.
*** HOL ***
--- a/lib/Tools/document Sun Dec 10 14:50:44 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,158 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: prepare theory session document
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
- echo
- echo " Options are:"
- echo " -c cleanup -- be aggressive in removing old stuff"
- echo " -n NAME specify document name (default 'document')"
- echo " -o FORMAT specify output format: pdf (default), dvi"
- echo " -t TAGS specify tagged region markup"
- echo
- echo " Prepare the theory session document in DIR (default 'document')"
- echo " producing the specified output format."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-CLEAN=""
-NAME="document"
-OUTFORMAT=pdf
-declare -a TAGS=()
-
-while getopts "cn:o:t:" OPT
-do
- case "$OPT" in
- c)
- CLEAN=true
- ;;
- n)
- NAME="$OPTARG"
- ;;
- o)
- OUTFORMAT="$OPTARG"
- ;;
- t)
- splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}")
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-DIR="document"
-[ "$#" -ge 1 ] && { DIR="$1"; shift; }
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-# check format
-
-case "$OUTFORMAT" in
- pdf | dvi)
- ;;
- *)
- fail "Bad output format '$OUTFORMAT'"
- ;;
-esac
-
-
-# document variants
-
-ROOT_NAME="root_$NAME"
-[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
-
-function prep_tags ()
-{
- (
- for TAG in "${TAGS[@]}"
- do
- case "$TAG" in
- /*)
- echo "\\isafoldtag{${TAG:1}}"
- ;;
- -*)
- echo "\\isadroptag{${TAG:1}}"
- ;;
- +*)
- echo "\\isakeeptag{${TAG:1}}"
- ;;
- *)
- echo "\\isakeeptag{${TAG}}"
- ;;
- esac
- done
- echo
- ) > isabelletags.sty
-}
-
-
-# prepare document
-
-(
- cd "$DIR" || fail "Bad directory '$DIR'"
-
- [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
-
- prep_tags
-
- if [ -f build ]; then
- ./build "$OUTFORMAT" "$NAME"
- RC="$?"
- else
- isabelle latex -o sty "$ROOT_NAME.tex" && \
- isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
- { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
- { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
- isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
- isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
- RC="$?"
- fi
-
- if [ "$RC" -ne 0 ]; then
- isabelle latex_errors -n "$ROOT_NAME"
- elif [ -f "$ROOT_NAME.$OUTFORMAT" ]; then
- cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
- fi
-
- exit "$RC"
-)
-RC="$?"
-
-
-# install
-
-[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
-
-#beware!
-[ -n "$CLEAN" ] && rm -rf "$DIR"
-
-exit "$RC"
--- a/src/Doc/System/Presentation.thy Sun Dec 10 14:50:44 2017 +0100
+++ b/src/Doc/System/Presentation.thy Sun Dec 10 18:31:41 2017 +0100
@@ -148,16 +148,18 @@
The @{tool_def document} tool prepares logic session documents, processing
the sources as provided by the user and generated by Isabelle. Its usage is:
@{verbatim [display]
-\<open>Usage: isabelle document [OPTIONS] [DIR]
+\<open>Usage: isabelle document [OPTIONS]
Options are:
- -c cleanup -- be aggressive in removing old stuff
- -n NAME specify document name (default 'document')
- -o FORMAT specify output format: pdf (default), dvi
- -t TAGS specify tagged region markup
+ -c aggressive cleanup of -d DIR content
+ -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 DIR (default 'document')
- producing the specified output format.\<close>}
+ Prepare the theory session document in document directory, producing the
+ specified output format.
+\<close>}
This tool is usually run automatically as part of the Isabelle build
process, provided document preparation has been enabled via suitable
@@ -172,9 +174,13 @@
document preparation!
\<^medskip>
+ Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
+ is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
+ 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.dvi\<close>''. Note that the result will appear in the
- parent of the target \<^verbatim>\<open>DIR\<close>.
+ the default is ``\<^verbatim>\<open>document.pdf\<close>''.
\<^medskip>
The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
--- a/src/Pure/System/isabelle_tool.scala Sun Dec 10 14:50:44 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala Sun Dec 10 18:31:41 2017 +0100
@@ -110,11 +110,11 @@
Check_Sources.isabelle_tool,
Doc.isabelle_tool,
Imports.isabelle_tool,
- Latex.isabelle_tool,
Mkroot.isabelle_tool,
ML_Process.isabelle_tool,
NEWS.isabelle_tool,
Options.isabelle_tool,
+ Present.isabelle_tool,
Profiling_Report.isabelle_tool,
Remote_DMG.isabelle_tool,
Server.isabelle_tool,
--- a/src/Pure/Thy/latex.scala Sun Dec 10 14:50:44 2017 +0100
+++ b/src/Pure/Thy/latex.scala Sun Dec 10 18:31:41 2017 +0100
@@ -16,6 +16,17 @@
{
/** latex errors **/
+ def latex_errors(dir: Path, root_name: String): List[String] =
+ {
+ val root_log_path = dir + Path.explode(root_name).ext("log")
+ if (root_log_path.is_file) {
+ for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
+ yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map(" " + _))
+ }
+ else Nil
+ }
+
+
/* generated .tex file */
private val File_Pattern = """^.*%:%file=(.+)%:%$""".r
@@ -144,49 +155,4 @@
filter(Line.logical_lines(root_log), Nil)
}
-
-
- /* errors */
-
- val default_root_name: String = "root"
-
- def latex_errors(dir: Path = Path.current, root_name: String = default_root_name)
- {
- val root_log_path = dir + Path.explode(root_name).ext("log")
- val errors =
- if (root_log_path.is_file) {
- for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
- yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map(" " + _))
- }
- else Nil
- if (errors.nonEmpty) Output.writeln(cat_lines(errors))
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool =
- Isabelle_Tool("latex_errors", "print latex errors for Isabelle document output", args =>
- {
- var dir = Path.current
- var root_name = default_root_name
-
- val getopts = Getopts("""
-Usage: isabelle latex_errors
-
- Options are:
- -d DIR alternative document directory (default: current)
- -n NAME alternative root name (default: """ + quote(default_root_name) + """)
-
- Print latex errors for Isabelle document output directory (with root.tex,
- root.log etc.).
-""",
- "d:" -> (arg => dir = Path.explode(arg)),
- "n:" -> (arg => root_name = arg))
-
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
-
- latex_errors(dir = dir, root_name = root_name)
- })
}
--- a/src/Pure/Thy/present.ML Sun Dec 10 14:50:44 2017 +0100
+++ b/src/Pure/Thy/present.ML Sun Dec 10 18:31:41 2017 +0100
@@ -190,11 +190,12 @@
fun isabelle_document {verbose, purge} format name tags dir =
let
- val s = "isabelle document -o '" ^ format ^ "' \
- \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir;
+ val script =
+ "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
+ " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
- val _ = if verbose then writeln s else ();
- val {out, err, rc, ...} = Bash.process s;
+ val _ = if verbose then writeln script else ();
+ val {out, err, rc, ...} = Bash.process script;
val _ = if verbose then writeln out else ();
val _ =
if not (File.exists doc_path) orelse rc <> 0 then
--- a/src/Pure/Thy/present.scala Sun Dec 10 14:50:44 2017 +0100
+++ b/src/Pure/Thy/present.scala Sun Dec 10 18:31:41 2017 +0100
@@ -131,4 +131,144 @@
{
make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
}
+
+
+
+ /** build document **/
+
+ 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 =
+ {
+ cat_lines(
+ tags.map(tag =>
+ tag.toList match {
+ case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
+ case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
+ case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
+ case cs => "\\isafoldtag{" + cs.mkString + "}"
+ })) + "\n"
+ }
+
+ def build_document(
+ document_name: String = default_document_name,
+ document_format: String = default_document_format,
+ document_dir: Option[Path] = None,
+ clean: Boolean = false,
+ tags: List[String] = Nil)
+ {
+ 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)
+
+ val root_name =
+ {
+ val root1 = "root_" + document_name
+ if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root"
+ }
+
+
+ /* bash scripts */
+
+ def root_bash(ext: String): String = Bash.string(root_name + "." + ext)
+
+ def latex_bash(fmt: String, ext: String = "tex"): String =
+ "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext)
+
+ def bash(script: String): Process_Result =
+ {
+ Output.writeln(script) // FIXME
+ Isabelle_System.bash(script, cwd = dir.file)
+ }
+
+
+ /* clean target */
+
+ val document_target = Path.parent + Path.explode(document_name).ext(document_format)
+
+ if (clean) {
+ bash("rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log " +
+ File.bash_path(document_target)).check
+ }
+
+
+ /* prepare document */
+
+ File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags))
+
+ val result =
+ if ((dir + Path.explode("build")).is_file) {
+ bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name))
+ }
+ else {
+ bash(
+ List(
+ latex_bash("sty"),
+ latex_bash(document_format),
+ "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
+ "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
+ latex_bash(document_format),
+ latex_bash(document_format)).mkString(" && "))
+ }
+
+
+ /* result */
+
+ if (!result.ok) {
+ cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
+ "Document preparation failure in directory " + dir)
+ }
+
+ bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
+ root_bash(document_format) + " " + File.bash_path(document_target)).check
+
+ // beware!
+ if (clean) Isabelle_System.rm_tree(dir)
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("document", "prepare theory session document", args =>
+ {
+ var clean = false
+ 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("""
+Usage: isabelle document [OPTIONS]
+
+ Options are:
+ -c aggressive cleanup of -d DIR content
+ -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
+ specified output format.
+""",
+ "c" -> (_ => clean = true),
+ "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()
+
+ build_document(document_dir = document_dir, document_name = document_name,
+ document_format = document_format, clean = clean, tags = tags)
+ })
}