# HG changeset patch # User wenzelm # Date 1512927101 -3600 # Node ID 13b5c3ff195489593c108d7e09ba47a4ef44084d # Parent 4e5ba4b23731be5556ebe8aebbe664dfe67c102f re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here; diff -r 4e5ba4b23731 -r 13b5c3ff1954 NEWS --- 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 *** diff -r 4e5ba4b23731 -r 13b5c3ff1954 lib/Tools/document --- 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" diff -r 4e5ba4b23731 -r 13b5c3ff1954 src/Doc/System/Presentation.thy --- 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] -\Usage: isabelle document [OPTIONS] [DIR] +\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.\} + Prepare the theory session document in document directory, producing the + specified output format. +\} 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>\-d\ specifies an laternative document output directory. The default + is \<^verbatim>\output/document\ (derived from the document name). Note that the result + 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.dvi\''. Note that the result will appear in the - parent of the target \<^verbatim>\DIR\. + the default is ``\<^verbatim>\document.pdf\''. \<^medskip> The \<^verbatim>\-t\ option tells {\LaTeX} how to interpret tagged Isabelle command diff -r 4e5ba4b23731 -r 13b5c3ff1954 src/Pure/System/isabelle_tool.scala --- 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, diff -r 4e5ba4b23731 -r 13b5c3ff1954 src/Pure/Thy/latex.scala --- 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) - }) } diff -r 4e5ba4b23731 -r 13b5c3ff1954 src/Pure/Thy/present.ML --- 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 diff -r 4e5ba4b23731 -r 13b5c3ff1954 src/Pure/Thy/present.scala --- 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) + }) }