re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
authorwenzelm
Sun Dec 10 18:31:41 2017 +0100 (17 months ago)
changeset 6717613b5c3ff1954
parent 67175 4e5ba4b23731
child 67177 af5b89bc065c
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
NEWS
lib/Tools/document
src/Doc/System/Presentation.thy
src/Pure/System/isabelle_tool.scala
src/Pure/Thy/latex.scala
src/Pure/Thy/present.ML
src/Pure/Thy/present.scala
     1.1 --- a/NEWS	Sun Dec 10 14:50:44 2017 +0100
     1.2 +++ b/NEWS	Sun Dec 10 18:31:41 2017 +0100
     1.3 @@ -86,7 +86,9 @@
     1.4  * Document preparation with skip_proofs option now preserves the content
     1.5  more accurately: only terminal proof steps ('by' etc.) are skipped.
     1.6  
     1.7 -* More explicit errors from latex process.
     1.8 +* Command-line tool "isabelle document" has been re-implemented in
     1.9 +Isabelle/Scala, with simplified arguments and explicit errors from the
    1.10 +latex process. Minor INCOMPATIBILITY.
    1.11  
    1.12  
    1.13  *** HOL ***
     2.1 --- a/lib/Tools/document	Sun Dec 10 14:50:44 2017 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,158 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Author: Markus Wenzel, TU Muenchen
     2.7 -#
     2.8 -# DESCRIPTION: prepare theory session document
     2.9 -
    2.10 -
    2.11 -PRG="$(basename "$0")"
    2.12 -
    2.13 -function usage()
    2.14 -{
    2.15 -  echo
    2.16 -  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
    2.17 -  echo
    2.18 -  echo "  Options are:"
    2.19 -  echo "    -c           cleanup -- be aggressive in removing old stuff"
    2.20 -  echo "    -n NAME      specify document name (default 'document')"
    2.21 -  echo "    -o FORMAT    specify output format: pdf (default), dvi"
    2.22 -  echo "    -t TAGS      specify tagged region markup"
    2.23 -  echo
    2.24 -  echo "  Prepare the theory session document in DIR (default 'document')"
    2.25 -  echo "  producing the specified output format."
    2.26 -  echo
    2.27 -  exit 1
    2.28 -}
    2.29 -
    2.30 -function fail()
    2.31 -{
    2.32 -  echo "$1" >&2
    2.33 -  exit 2
    2.34 -}
    2.35 -
    2.36 -
    2.37 -## process command line
    2.38 -
    2.39 -# options
    2.40 -
    2.41 -CLEAN=""
    2.42 -NAME="document"
    2.43 -OUTFORMAT=pdf
    2.44 -declare -a TAGS=()
    2.45 -
    2.46 -while getopts "cn:o:t:" OPT
    2.47 -do
    2.48 -  case "$OPT" in
    2.49 -    c)
    2.50 -      CLEAN=true
    2.51 -      ;;
    2.52 -    n)
    2.53 -      NAME="$OPTARG"
    2.54 -      ;;
    2.55 -    o)
    2.56 -      OUTFORMAT="$OPTARG"
    2.57 -      ;;
    2.58 -    t)
    2.59 -      splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}")
    2.60 -      ;;
    2.61 -    \?)
    2.62 -      usage
    2.63 -      ;;
    2.64 -  esac
    2.65 -done
    2.66 -
    2.67 -shift $(($OPTIND - 1))
    2.68 -
    2.69 -
    2.70 -# args
    2.71 -
    2.72 -DIR="document"
    2.73 -[ "$#" -ge 1 ] && { DIR="$1"; shift; }
    2.74 -
    2.75 -[ "$#" -ne 0 ] && usage
    2.76 -
    2.77 -
    2.78 -## main
    2.79 -
    2.80 -# check format
    2.81 -
    2.82 -case "$OUTFORMAT" in
    2.83 -  pdf | dvi)
    2.84 -    ;;
    2.85 -  *)
    2.86 -    fail "Bad output format '$OUTFORMAT'"
    2.87 -    ;;
    2.88 -esac
    2.89 -
    2.90 -
    2.91 -# document variants
    2.92 -
    2.93 -ROOT_NAME="root_$NAME"
    2.94 -[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
    2.95 -
    2.96 -function prep_tags ()
    2.97 -{
    2.98 -  (
    2.99 -    for TAG in "${TAGS[@]}"
   2.100 -    do
   2.101 -      case "$TAG" in
   2.102 -        /*)
   2.103 -          echo "\\isafoldtag{${TAG:1}}"
   2.104 -          ;;
   2.105 -        -*)
   2.106 -          echo "\\isadroptag{${TAG:1}}"
   2.107 -          ;;
   2.108 -        +*)
   2.109 -          echo "\\isakeeptag{${TAG:1}}"
   2.110 -          ;;
   2.111 -        *)
   2.112 -          echo "\\isakeeptag{${TAG}}"
   2.113 -          ;;
   2.114 -      esac
   2.115 -    done
   2.116 -    echo
   2.117 -  ) > isabelletags.sty
   2.118 -}
   2.119 -
   2.120 -
   2.121 -# prepare document
   2.122 -
   2.123 -(
   2.124 -  cd "$DIR" || fail "Bad directory '$DIR'"
   2.125 -
   2.126 -  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
   2.127 -
   2.128 -  prep_tags
   2.129 -
   2.130 -  if [ -f build ]; then
   2.131 -    ./build "$OUTFORMAT" "$NAME"
   2.132 -    RC="$?"
   2.133 -  else
   2.134 -    isabelle latex -o sty "$ROOT_NAME.tex" && \
   2.135 -    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
   2.136 -    { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
   2.137 -    { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
   2.138 -    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
   2.139 -    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
   2.140 -    RC="$?"
   2.141 -  fi
   2.142 -
   2.143 -  if [ "$RC" -ne 0 ]; then
   2.144 -    isabelle latex_errors -n "$ROOT_NAME"
   2.145 -  elif [ -f "$ROOT_NAME.$OUTFORMAT" ]; then
   2.146 -    cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
   2.147 -  fi
   2.148 -
   2.149 -  exit "$RC"
   2.150 -)
   2.151 -RC="$?"
   2.152 -
   2.153 -
   2.154 -# install
   2.155 -
   2.156 -[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
   2.157 -
   2.158 -#beware!
   2.159 -[ -n "$CLEAN" ] && rm -rf "$DIR"
   2.160 -
   2.161 -exit "$RC"
     3.1 --- a/src/Doc/System/Presentation.thy	Sun Dec 10 14:50:44 2017 +0100
     3.2 +++ b/src/Doc/System/Presentation.thy	Sun Dec 10 18:31:41 2017 +0100
     3.3 @@ -148,16 +148,18 @@
     3.4    The @{tool_def document} tool prepares logic session documents, processing
     3.5    the sources as provided by the user and generated by Isabelle. Its usage is:
     3.6    @{verbatim [display]
     3.7 -\<open>Usage: isabelle document [OPTIONS] [DIR]
     3.8 +\<open>Usage: isabelle document [OPTIONS]
     3.9  
    3.10    Options are:
    3.11 -    -c           cleanup -- be aggressive in removing old stuff
    3.12 -    -n NAME      specify document name (default 'document')
    3.13 -    -o FORMAT    specify output format: pdf (default), dvi
    3.14 -    -t TAGS      specify tagged region markup
    3.15 +    -c           aggressive cleanup of -d DIR content
    3.16 +    -d DIR       document output directory (default "output/document")
    3.17 +    -n NAME      document name (default "document")
    3.18 +    -o FORMAT    document format: pdf (default), dvi
    3.19 +    -t TAGS      markup for tagged regions
    3.20  
    3.21 -  Prepare the theory session document in DIR (default 'document')
    3.22 -  producing the specified output format.\<close>}
    3.23 +  Prepare the theory session document in document directory, producing the
    3.24 +  specified output format.
    3.25 +\<close>}
    3.26  
    3.27    This tool is usually run automatically as part of the Isabelle build
    3.28    process, provided document preparation has been enabled via suitable
    3.29 @@ -172,9 +174,13 @@
    3.30    document preparation!
    3.31  
    3.32    \<^medskip>
    3.33 +  Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
    3.34 +  is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
    3.35 +  will appear in the parent of this directory.
    3.36 +
    3.37 +  \<^medskip>
    3.38    The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
    3.39 -  the default is ``\<^verbatim>\<open>document.dvi\<close>''. Note that the result will appear in the
    3.40 -  parent of the target \<^verbatim>\<open>DIR\<close>.
    3.41 +  the default is ``\<^verbatim>\<open>document.pdf\<close>''.
    3.42  
    3.43    \<^medskip>
    3.44    The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
     4.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Dec 10 14:50:44 2017 +0100
     4.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Dec 10 18:31:41 2017 +0100
     4.3 @@ -110,11 +110,11 @@
     4.4        Check_Sources.isabelle_tool,
     4.5        Doc.isabelle_tool,
     4.6        Imports.isabelle_tool,
     4.7 -      Latex.isabelle_tool,
     4.8        Mkroot.isabelle_tool,
     4.9        ML_Process.isabelle_tool,
    4.10        NEWS.isabelle_tool,
    4.11        Options.isabelle_tool,
    4.12 +      Present.isabelle_tool,
    4.13        Profiling_Report.isabelle_tool,
    4.14        Remote_DMG.isabelle_tool,
    4.15        Server.isabelle_tool,
     5.1 --- a/src/Pure/Thy/latex.scala	Sun Dec 10 14:50:44 2017 +0100
     5.2 +++ b/src/Pure/Thy/latex.scala	Sun Dec 10 18:31:41 2017 +0100
     5.3 @@ -16,6 +16,17 @@
     5.4  {
     5.5    /** latex errors **/
     5.6  
     5.7 +  def latex_errors(dir: Path, root_name: String): List[String] =
     5.8 +  {
     5.9 +    val root_log_path = dir + Path.explode(root_name).ext("log")
    5.10 +    if (root_log_path.is_file) {
    5.11 +      for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
    5.12 +      yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map("  " + _))
    5.13 +    }
    5.14 +    else Nil
    5.15 +  }
    5.16 +
    5.17 +
    5.18    /* generated .tex file */
    5.19  
    5.20    private val File_Pattern = """^.*%:%file=(.+)%:%$""".r
    5.21 @@ -144,49 +155,4 @@
    5.22  
    5.23      filter(Line.logical_lines(root_log), Nil)
    5.24    }
    5.25 -
    5.26 -
    5.27 -  /* errors */
    5.28 -
    5.29 -  val default_root_name: String = "root"
    5.30 -
    5.31 -  def latex_errors(dir: Path = Path.current, root_name: String = default_root_name)
    5.32 -  {
    5.33 -    val root_log_path = dir + Path.explode(root_name).ext("log")
    5.34 -    val errors =
    5.35 -      if (root_log_path.is_file) {
    5.36 -        for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
    5.37 -        yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map("  " + _))
    5.38 -      }
    5.39 -      else Nil
    5.40 -    if (errors.nonEmpty) Output.writeln(cat_lines(errors))
    5.41 -  }
    5.42 -
    5.43 -
    5.44 -  /* Isabelle tool wrapper */
    5.45 -
    5.46 -  val isabelle_tool =
    5.47 -    Isabelle_Tool("latex_errors", "print latex errors for Isabelle document output", args =>
    5.48 -  {
    5.49 -    var dir = Path.current
    5.50 -    var root_name = default_root_name
    5.51 -
    5.52 -    val getopts = Getopts("""
    5.53 -Usage: isabelle latex_errors
    5.54 -
    5.55 -  Options are:
    5.56 -    -d DIR       alternative document directory (default: current)
    5.57 -    -n NAME      alternative root name (default: """ + quote(default_root_name) + """)
    5.58 -
    5.59 -  Print latex errors for Isabelle document output directory (with root.tex,
    5.60 -  root.log etc.).
    5.61 -""",
    5.62 -      "d:" -> (arg => dir = Path.explode(arg)),
    5.63 -      "n:" -> (arg => root_name = arg))
    5.64 -
    5.65 -    val more_args = getopts(args)
    5.66 -    if (more_args.nonEmpty) getopts.usage()
    5.67 -
    5.68 -    latex_errors(dir = dir, root_name = root_name)
    5.69 -  })
    5.70  }
     6.1 --- a/src/Pure/Thy/present.ML	Sun Dec 10 14:50:44 2017 +0100
     6.2 +++ b/src/Pure/Thy/present.ML	Sun Dec 10 18:31:41 2017 +0100
     6.3 @@ -190,11 +190,12 @@
     6.4  
     6.5  fun isabelle_document {verbose, purge} format name tags dir =
     6.6    let
     6.7 -    val s = "isabelle document -o '" ^ format ^ "' \
     6.8 -      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir;
     6.9 +    val script =
    6.10 +      "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
    6.11 +        " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
    6.12      val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
    6.13 -    val _ = if verbose then writeln s else ();
    6.14 -    val {out, err, rc, ...} = Bash.process s;
    6.15 +    val _ = if verbose then writeln script else ();
    6.16 +    val {out, err, rc, ...} = Bash.process script;
    6.17      val _ = if verbose then writeln out else ();
    6.18      val _ =
    6.19        if not (File.exists doc_path) orelse rc <> 0 then
     7.1 --- a/src/Pure/Thy/present.scala	Sun Dec 10 14:50:44 2017 +0100
     7.2 +++ b/src/Pure/Thy/present.scala	Sun Dec 10 18:31:41 2017 +0100
     7.3 @@ -131,4 +131,144 @@
     7.4    {
     7.5      make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
     7.6    }
     7.7 +
     7.8 +
     7.9 +
    7.10 +  /** build document **/
    7.11 +
    7.12 +  val default_document_name = "document"
    7.13 +  val default_document_format = "pdf"
    7.14 +  val document_formats = List("pdf", "dvi")
    7.15 +  def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name)
    7.16 +
    7.17 +  def document_tags(tags: List[String]): String =
    7.18 +  {
    7.19 +    cat_lines(
    7.20 +      tags.map(tag =>
    7.21 +        tag.toList match {
    7.22 +          case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
    7.23 +          case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
    7.24 +          case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
    7.25 +          case cs => "\\isafoldtag{" + cs.mkString + "}"
    7.26 +        })) + "\n"
    7.27 +  }
    7.28 +
    7.29 +  def build_document(
    7.30 +    document_name: String = default_document_name,
    7.31 +    document_format: String = default_document_format,
    7.32 +    document_dir: Option[Path] = None,
    7.33 +    clean: Boolean = false,
    7.34 +    tags: List[String] = Nil)
    7.35 +  {
    7.36 +    if (!document_formats.contains(document_format))
    7.37 +      error("Bad document output format: " + quote(document_format))
    7.38 +
    7.39 +    val dir = document_dir getOrElse default_document_dir(document_name)
    7.40 +    if (!dir.is_dir) error("Bad document output directory " + dir)
    7.41 +
    7.42 +    val root_name =
    7.43 +    {
    7.44 +      val root1 = "root_" + document_name
    7.45 +      if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root"
    7.46 +    }
    7.47 +
    7.48 +
    7.49 +    /* bash scripts */
    7.50 +
    7.51 +    def root_bash(ext: String): String = Bash.string(root_name + "." + ext)
    7.52 +
    7.53 +    def latex_bash(fmt: String, ext: String = "tex"): String =
    7.54 +      "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext)
    7.55 +
    7.56 +    def bash(script: String): Process_Result =
    7.57 +    {
    7.58 +      Output.writeln(script)  // FIXME
    7.59 +      Isabelle_System.bash(script, cwd = dir.file)
    7.60 +    }
    7.61 +
    7.62 +
    7.63 +    /* clean target */
    7.64 +
    7.65 +    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
    7.66 +
    7.67 +    if (clean) {
    7.68 +      bash("rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log " +
    7.69 +        File.bash_path(document_target)).check
    7.70 +    }
    7.71 +
    7.72 +
    7.73 +    /* prepare document */
    7.74 +
    7.75 +    File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags))
    7.76 +
    7.77 +    val result =
    7.78 +      if ((dir + Path.explode("build")).is_file) {
    7.79 +        bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name))
    7.80 +      }
    7.81 +      else {
    7.82 +        bash(
    7.83 +          List(
    7.84 +            latex_bash("sty"),
    7.85 +            latex_bash(document_format),
    7.86 +            "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
    7.87 +            "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
    7.88 +            latex_bash(document_format),
    7.89 +            latex_bash(document_format)).mkString(" && "))
    7.90 +      }
    7.91 +
    7.92 +
    7.93 +    /* result */
    7.94 +
    7.95 +    if (!result.ok) {
    7.96 +      cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
    7.97 +        "Document preparation failure in directory " + dir)
    7.98 +    }
    7.99 +
   7.100 +    bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
   7.101 +      root_bash(document_format) + " " + File.bash_path(document_target)).check
   7.102 +
   7.103 +    // beware!
   7.104 +    if (clean) Isabelle_System.rm_tree(dir)
   7.105 +  }
   7.106 +
   7.107 +
   7.108 +  /* Isabelle tool wrapper */
   7.109 +
   7.110 +  val isabelle_tool =
   7.111 +    Isabelle_Tool("document", "prepare theory session document", args =>
   7.112 +  {
   7.113 +    var clean = false
   7.114 +    var document_dir: Option[Path] = None
   7.115 +    var document_name = default_document_name
   7.116 +    var document_format = default_document_format
   7.117 +    var tags: List[String] = Nil
   7.118 +
   7.119 +    val getopts = Getopts("""
   7.120 +Usage: isabelle document [OPTIONS]
   7.121 +
   7.122 +  Options are:
   7.123 +    -c           aggressive cleanup of -d DIR content
   7.124 +    -d DIR       document output directory (default """ +
   7.125 +      default_document_dir(default_document_name) + """)
   7.126 +    -n NAME      document name (default """ + quote(default_document_name) + """)
   7.127 +    -o FORMAT    document format: """ +
   7.128 +      commas(document_formats.map(fmt =>
   7.129 +        fmt + (if (fmt == default_document_format) " (default)" else ""))) + """
   7.130 +    -t TAGS      markup for tagged regions
   7.131 +
   7.132 +  Prepare the theory session document in document directory, producing the
   7.133 +  specified output format.
   7.134 +""",
   7.135 +      "c" -> (_ => clean = true),
   7.136 +      "d:" -> (arg => document_dir = Some(Path.explode(arg))),
   7.137 +      "n:" -> (arg => document_name = arg),
   7.138 +      "o:" -> (arg => document_format = arg),
   7.139 +      "t:" -> (arg => tags = space_explode(',', arg)))
   7.140 +
   7.141 +    val more_args = getopts(args)
   7.142 +    if (more_args.nonEmpty) getopts.usage()
   7.143 +
   7.144 +    build_document(document_dir = document_dir, document_name = document_name,
   7.145 +      document_format = document_format, clean = clean, tags = tags)
   7.146 +  })
   7.147  }