--- a/NEWS Wed Dec 13 19:28:19 2017 +0100
+++ b/NEWS Thu Dec 14 11:24:26 2017 +0100
@@ -86,6 +86,10 @@
* Document preparation with skip_proofs option now preserves the content
more accurately: only terminal proof steps ('by' etc.) are skipped.
+* 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/etc/settings Wed Dec 13 19:28:19 2017 +0100
+++ b/etc/settings Thu Dec 14 11:24:26 2017 +0100
@@ -46,12 +46,17 @@
### Document preparation (cf. isabelle latex/document)
###
-ISABELLE_LATEX="latex"
-ISABELLE_PDFLATEX="pdflatex"
+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
+
###
### Misc path settings
--- a/lib/Tools/document Wed Dec 13 19:28:19 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,156 +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" -eq 0 -a -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 Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Doc/System/Presentation.thy Thu Dec 14 11:24:26 2017 +0100
@@ -148,16 +148,17 @@
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
+ -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
@@ -166,15 +167,13 @@
run.
\<^medskip>
- The \<^verbatim>\<open>-c\<close> option tells @{tool document} to dispose the document sources
- after successful operation! This is the right thing to do for sources
- generated by an Isabelle process, but take care of your files in manual
- document preparation!
+ 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
@@ -234,10 +233,10 @@
we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
\<^medskip>
- As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
- run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual
- output document is built and installed in its proper place. The generated
- sources are deleted after successful run of {\LaTeX} and friends.
+ As a final step of Isabelle document preparation, @{tool document} is run on
+ the generated \<^verbatim>\<open>output/document\<close> directory. Thus the actual output document
+ is built and installed in its proper place. The generated sources are
+ deleted after successful run of {\LaTeX} and friends.
Some care is needed if the document output location is configured
differently, say within a directory whose content is still required
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Dec 14 11:24:26 2017 +0100
@@ -346,7 +346,7 @@
res match {
case Exn.Res(_) => None
case Exn.Exn(exn) =>
- System.err.println("Exception trace for " + quote(task.name) + ":")
+ Output.writeln("Exception trace for " + quote(task.name) + ":")
exn.printStackTrace()
val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
Some(first_line)
--- a/src/Pure/General/antiquote.ML Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/General/antiquote.ML Thu Dec 14 11:24:26 2017 +0100
@@ -76,11 +76,15 @@
val err_prefix = "Antiquotation lexical error: ";
+val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
+
val scan_txt =
+ scan_nl ||
Scan.repeats1
(Scan.many1 (fn (s, _) =>
- not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso Symbol.not_eof s) ||
- $$$ "@" --| Scan.ahead (~$$ "{"));
+ not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso
+ s <> "\n" andalso Symbol.not_eof s) ||
+ $$$ "@" --| Scan.ahead (~$$ "{")) @@@ Scan.optional scan_nl [];
val scan_antiq_body =
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
--- a/src/Pure/General/output.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/General/output.scala Thu Dec 14 11:24:26 2017 +0100
@@ -24,24 +24,24 @@
def writeln(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(writeln_text(msg))
- else Console.err.println(writeln_text(msg))
+ if (stdout) Console.print(writeln_text(msg) + "\n")
+ else Console.err.print(writeln_text(msg) + "\n")
}
}
def warning(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(warning_text(msg))
- else Console.err.println(warning_text(msg))
+ if (stdout) Console.print(warning_text(msg) + "\n")
+ else Console.err.print(warning_text(msg) + "\n")
}
}
def error_message(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(error_message_text(msg))
- else Console.err.println(error_message_text(msg))
+ if (stdout) Console.print(error_message_text(msg) + "\n")
+ else Console.err.print(error_message_text(msg) + "\n")
}
}
}
--- a/src/Pure/General/path.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/General/path.scala Thu Dec 14 11:24:26 2017 +0100
@@ -215,4 +215,7 @@
def absolute_file: JFile = File.absolute(file)
def canonical_file: JFile = File.canonical(file)
+
+ def absolute: Path = File.path(absolute_file)
+ def canonical: Path = File.path(canonical_file)
}
--- a/src/Pure/System/getopts.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/System/getopts.scala Thu Dec 14 11:24:26 2017 +0100
@@ -29,7 +29,7 @@
{
def usage(): Nothing =
{
- Console.println(usage_text)
+ Output.writeln(usage_text, stdout = true)
sys.exit(1)
}
--- a/src/Pure/System/isabelle_process.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/System/isabelle_process.scala Thu Dec 14 11:24:26 2017 +0100
@@ -41,7 +41,7 @@
modes: List[String] = Nil,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
- receiver: Prover.Receiver = Console.println(_),
+ receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
xml_cache: XML.Cache = new XML.Cache(),
sessions: Option[Sessions.Structure] = None,
store: Sessions.Store = Sessions.store()): Prover =
--- a/src/Pure/System/isabelle_tool.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala Thu Dec 14 11:24:26 2017 +0100
@@ -114,6 +114,7 @@
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/System/options.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/System/options.scala Thu Dec 14 11:24:26 2017 +0100
@@ -185,13 +185,13 @@
}
if (get_option != "")
- Console.println(options.check_name(get_option).value)
+ Output.writeln(options.check_name(get_option).value, stdout = true)
if (export_file != "")
File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
if (get_option == "" && export_file == "")
- Console.println(options.print)
+ Output.writeln(options.print, stdout = true)
})
}
--- a/src/Pure/System/progress.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/System/progress.scala Thu Dec 14 11:24:26 2017 +0100
@@ -45,7 +45,7 @@
{
override def echo(msg: String)
{
- if (stderr) Console.err.println(msg) else Console.println(msg)
+ Output.writeln(msg, stdout = !stderr)
}
override def theory(session: String, theory: String): Unit =
--- a/src/Pure/Thy/document_antiquotations.ML Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Thu Dec 14 11:24:26 2017 +0100
@@ -44,7 +44,8 @@
fun control_antiquotation name s1 s2 =
Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
- (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
+ (fn {state, ...} =>
+ enclose s1 s2 o Latex.output_text o Thy_Output.output_text state {markdown = false});
in
--- a/src/Pure/Thy/latex.ML Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Thy/latex.ML Thu Dec 14 11:24:26 2017 +0100
@@ -6,6 +6,13 @@
signature LATEX =
sig
+ type text
+ val string: string -> text
+ val text: string * Position.T -> text
+ val block: text list -> text
+ val enclose_body: string -> string -> text list -> text list
+ val output_text: text list -> string
+ val output_positions: Position.T -> text list -> string
val output_name: string -> string
val output_ascii: string -> string
val latex_control: Symbol.symbol
@@ -20,9 +27,9 @@
val end_delim: string -> string
val begin_tag: string -> string
val end_tag: string -> string
+ val environment_block: string -> text list -> text
val environment: string -> string -> string
- val tex_trailer: string
- val isabelle_theory: string -> string -> string
+ val isabelle_body: string -> text list -> text list
val symbol_source: (string -> bool) * (string -> bool) ->
string -> Symbol.symbol list -> string
val theory_entry: string -> string
@@ -32,6 +39,50 @@
structure Latex: LATEX =
struct
+(* text with positions *)
+
+abstype text = Text of string * Position.T | Block of text list
+with
+
+fun string s = Text (s, Position.none);
+val text = Text;
+val block = Block;
+
+fun output_text texts =
+ let
+ fun output (Text (s, _)) = Buffer.add s
+ | output (Block body) = fold output body;
+ in Buffer.empty |> fold output texts |> Buffer.content end;
+
+fun output_positions file_pos texts =
+ let
+ fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b);
+ fun add_position p positions =
+ let val s = position (apply2 Value.print_int p)
+ in positions |> s <> hd positions ? cons s end;
+
+ fun output (Text (s, pos)) (positions, line) =
+ let
+ val positions' =
+ (case Position.line_of pos of
+ NONE => positions
+ | SOME l => add_position (line, l) positions);
+ val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line;
+ in (positions', line') end
+ | output (Block body) res = fold output body res;
+ in
+ (case Position.file_of file_pos of
+ NONE => ""
+ | SOME file =>
+ ([position (Markup.fileN, file), "\\endinput"], 1)
+ |> fold output texts |> #1 |> rev |> cat_lines)
+ end;
+
+end;
+
+fun enclose_body bg en body = string bg :: body @ [string en];
+
+
(* output name for LaTeX macros *)
val output_name =
@@ -173,25 +224,28 @@
(* output token *)
fun output_token tok =
- let val s = Token.content_of tok in
- if Token.is_kind Token.Comment tok then ""
- else if Token.is_command tok then
- "\\isacommand{" ^ output_syms s ^ "}"
- else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
- "\\isakeyword{" ^ output_syms s ^ "}"
- else if Token.is_kind Token.String tok then
- enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
- else if Token.is_kind Token.Alt_String tok then
- enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
- else if Token.is_kind Token.Verbatim tok then
- let
- val ants = Antiquote.read (Token.input_of tok);
- val out = implode (map output_syms_antiq ants);
- in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
- else if Token.is_kind Token.Cartouche tok then
- enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
- else output_syms s
- end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
+ let
+ val s = Token.content_of tok;
+ val output =
+ if Token.is_kind Token.Comment tok then ""
+ else if Token.is_command tok then
+ "\\isacommand{" ^ output_syms s ^ "}"
+ else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
+ "\\isakeyword{" ^ output_syms s ^ "}"
+ else if Token.is_kind Token.String tok then
+ enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
+ else if Token.is_kind Token.Alt_String tok then
+ enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
+ else if Token.is_kind Token.Verbatim tok then
+ let
+ val ants = Antiquote.read (Token.input_of tok);
+ val out = implode (map output_syms_antiq ants);
+ in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
+ else if Token.is_kind Token.Cartouche tok then
+ enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
+ else output_syms s;
+ in output end
+ handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
(* tags *)
@@ -204,22 +258,21 @@
(* theory presentation *)
-fun environment name =
- enclose ("%\n\\begin{" ^ output_name name ^ "}%\n") ("%\n\\end{" ^ output_name name ^ "}");
+fun environment_delim name =
+ ("%\n\\begin{" ^ output_name name ^ "}%\n",
+ "%\n\\end{" ^ output_name name ^ "}");
-val tex_trailer =
- "%%% Local Variables:\n\
- \%%% mode: latex\n\
- \%%% TeX-master: \"root\"\n\
- \%%% End:\n";
+fun environment_block name = environment_delim name |-> enclose_body #> block;
+fun environment name = environment_delim name |-> enclose;
-fun isabelle_theory name txt =
- "%\n\\begin{isabellebody}%\n\
- \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
- "%\n\\end{isabellebody}%\n" ^ tex_trailer;
+fun isabelle_body_delim name =
+ ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n",
+ "%\n\\end{isabellebody}%\n");
+
+fun isabelle_body name = isabelle_body_delim name |-> enclose_body;
fun symbol_source known name syms =
- isabelle_theory name
+ uncurry enclose (isabelle_body_delim name)
("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
output_known_symbols known syms);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/latex.scala Thu Dec 14 11:24:26 2017 +0100
@@ -0,0 +1,158 @@
+/* Title: Pure/Thy/latex.scala
+ Author: Makarius
+
+Support for LaTeX.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+import scala.annotation.tailrec
+
+
+object Latex
+{
+ /** 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
+ private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
+
+ def read_tex_file(tex_file: Path): Tex_File =
+ {
+ val positions =
+ Line.logical_lines(File.read(tex_file)).reverse.
+ takeWhile(_ != "\\endinput").reverse
+
+ val source_file =
+ positions match {
+ case File_Pattern(file) :: _ => Some(file)
+ case _ => None
+ }
+
+ val source_lines =
+ if (source_file.isEmpty) Nil
+ else
+ positions.flatMap(line =>
+ line match {
+ case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
+ case _ => None
+ })
+
+ new Tex_File(tex_file, source_file, source_lines)
+ }
+
+ final class Tex_File private[Latex](
+ tex_file: Path, source_file: Option[String], source_lines: List[(Int, Int)])
+ {
+ override def toString: String = tex_file.toString
+
+ def source_position(l: Int): Option[Position.T] =
+ source_file match {
+ case None => None
+ case Some(file) =>
+ val source_line =
+ (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))(
+ { case (_, (_, n)) => n })
+ if (source_line == 0) None else Some(Position.Line_File(source_line, file))
+ }
+
+ def position(line: Int): Position.T =
+ source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
+ }
+
+
+ /* latex log */
+
+ def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
+ {
+ val seen_files = Synchronized(Map.empty[JFile, Tex_File])
+
+ def check_tex_file(path: Path): Option[Tex_File] =
+ seen_files.change_result(seen =>
+ seen.get(path.file) match {
+ case None =>
+ if (path.is_file) {
+ val tex_file = read_tex_file(path)
+ (Some(tex_file), seen + (path.file -> tex_file))
+ }
+ else (None, seen)
+ case some => (some, seen)
+ })
+
+ def tex_file_position(path: Path, line: Int): Position.T =
+ check_tex_file(path) match {
+ case Some(tex_file) => tex_file.position(line)
+ case None => Position.Line_File(line, path.implode)
+ }
+
+ object File_Line_Error
+ {
+ val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
+ def unapply(line: String): Option[(Path, Int, String)] =
+ line match {
+ case Pattern(file, Value.Int(line), message) =>
+ val path = File.standard_path(file)
+ if (Path.is_wellformed(path)) {
+ val file = (dir + Path.explode(path)).canonical
+ if (file.is_file) Some((file, line, message)) else None
+ }
+ else None
+ case _ => None
+ }
+ }
+
+ val More_Error =
+ List(
+ """l\.\d+""",
+ "<argument>",
+ "<template>",
+ "<recently read>",
+ "<to be read again>",
+ "<inserted text>",
+ "<output>",
+ "<everypar>",
+ "<everymath>",
+ "<everydisplay>",
+ "<everyhbox>",
+ "<everyvbox>",
+ "<everyjob>",
+ "<everycr>",
+ "<mark>",
+ "<everyeof>",
+ "<write>").mkString("^(?:", "|", ") (.*)$").r
+
+ @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
+ : List[(String, Position.T)] =
+ {
+ lines match {
+ case File_Line_Error((file, line, msg1)) :: rest1 =>
+ val pos = tex_file_position(file, line)
+ rest1 match {
+ case More_Error(msg2) :: rest2 =>
+ filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
+ case _ =>
+ filter(rest1, (msg1, pos) :: result)
+ }
+ case _ :: rest => filter(rest, result)
+ case Nil => result.reverse
+ }
+ }
+
+ filter(Line.logical_lines(root_log), Nil)
+ }
+}
--- a/src/Pure/Thy/present.ML Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Thy/present.ML Thu Dec 14 11:24:26 2017 +0100
@@ -12,7 +12,7 @@
val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
(Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
val finish: unit -> unit
- val theory_output: theory -> string -> unit
+ val theory_output: Position.T -> theory -> Latex.text list -> unit
val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
val display_drafts: Path.T list -> int
end;
@@ -188,19 +188,16 @@
(* isabelle tool wrappers *)
-fun isabelle_document {verbose, purge} format name tags dir =
+fun isabelle_document {verbose} format name tags dir =
let
- val s = "isabelle document -o '" ^ format ^ "' \
- \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
+ 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, rc) = Isabelle_System.bash_output s;
- val _ =
- if not (File.exists doc_path) orelse rc <> 0 then
- cat_error out ("Failed to build document " ^ quote (show_path doc_path))
- else if verbose then writeln out
- else ();
- val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
+ 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 ();
+ val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
in doc_path end;
@@ -213,7 +210,7 @@
File.write_buffer (Path.append path (tex_path name)) src;
fun write_tex_index tex_index path =
- write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
+ write_tex (index_buffer tex_index) doc_indexN path;
fun finish () =
with_session_info () (fn {name, chapter, info, info_path, doc_format,
@@ -243,6 +240,8 @@
fun document_job doc_prefix backdrop (doc_name, tags) =
let
val doc_dir = Path.append doc_prefix (Path.basic doc_name);
+ fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else ();
+ val _ = purge ();
val _ = Isabelle_System.mkdirs doc_dir;
val _ =
Isabelle_System.bash ("isabelle latex -o sty " ^
@@ -255,7 +254,7 @@
write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
in
fn () =>
- (isabelle_document {verbose = true, purge = backdrop} doc_format doc_name tags doc_dir,
+ (isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (),
fn doc =>
if verbose orelse not backdrop then
Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
@@ -279,11 +278,15 @@
(* theory elements *)
-fun theory_output thy tex =
+fun theory_output pos thy body =
with_session_info () (fn _ =>
if is_session_theory thy then
- let val name = Context.theory_name thy;
- in change_theory_info name (fn (_, html) => (Latex.isabelle_theory name tex, html)) end
+ let val name = Context.theory_name thy in
+ (change_theory_info name o apfst)
+ (fn _ =>
+ let val latex = Latex.isabelle_body name body
+ in Latex.output_text latex ^ Latex.output_positions pos latex end)
+ end
else ());
fun theory_link (curr_chapter, curr_session) thy =
@@ -356,8 +359,7 @@
|> File.write (Path.append doc_path (tex_path name)));
val _ = write_tex_index tex_index doc_path;
- val result =
- isabelle_document {verbose = false, purge = true} "pdf" documentN "" doc_path;
+ val result = isabelle_document {verbose = false} "pdf" documentN "" doc_path;
val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
--- a/src/Pure/Thy/present.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Thy/present.scala Thu Dec 14 11:24:26 2017 +0100
@@ -131,4 +131,129 @@
{
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,
+ 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)
+
+ 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 =
+ Isabelle_System.bash(script, cwd = dir.file)
+
+
+ /* 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)),
+ "Failed to build document in " + File.path(dir.absolute_file))
+ }
+
+ bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
+ root_bash(document_format) + " " + File.bash_path(document_target)).check
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("document", "prepare theory session document", args =>
+ {
+ 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:
+ -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.
+""",
+ "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)
+ }
+ catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) }
+ })
}
--- a/src/Pure/Thy/thy_info.ML Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Thy/thy_info.ML Thu Dec 14 11:24:26 2017 +0100
@@ -268,8 +268,8 @@
in
if exists (Toplevel.is_skipped_proof o #2) res then ()
else
- let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
- in if document then Present.theory_output thy tex_source else () end
+ let val body = Thy_Output.present_thy thy res toks;
+ in if document then Present.theory_output text_pos thy body else () end
end;
in (thy, present, size text) end;
--- a/src/Pure/Thy/thy_output.ML Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML Thu Dec 14 11:24:26 2017 +0100
@@ -24,8 +24,9 @@
val boolean: string -> bool
val integer: string -> int
val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
- val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string
- val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
+ val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
+ val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
+ Token.T list -> Latex.text list
val pretty_text: Proof.context -> string -> Pretty.T
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
@@ -35,8 +36,8 @@
val string_of_margin: Proof.context -> Pretty.T -> string
val output: Proof.context -> Pretty.T list -> string
val verbatim_text: Proof.context -> string -> string
- val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
- Toplevel.transition -> Toplevel.transition
+ val document_command: {markdown: bool} ->
+ (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
end;
structure Thy_Output: THY_OUTPUT =
@@ -208,18 +209,20 @@
Position.report pos (Markup.language_document (Input.is_delimited source))
else ();
- val output_antiquotes = map (eval_antiquote state) #> implode;
+ val output_antiquotes =
+ map (fn ant => Latex.text (eval_antiquote state ant, #1 (Antiquote.range [ant])));
fun output_line line =
- (if Markdown.line_is_item line then "\\item " else "") ^
+ (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
output_antiquotes (Markdown.line_content line);
- fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
- and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
+ fun output_block (Markdown.Par lines) =
+ Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines))
| output_block (Markdown.List {kind, body, ...}) =
- Latex.environment (Markdown.print_kind kind) (output_blocks body);
+ Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
+ and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
in
- if Toplevel.is_skipped_proof state then ""
+ if Toplevel.is_skipped_proof state then []
else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
then
let
@@ -259,19 +262,17 @@
val blank_token = basic_token Token.is_blank;
val newline_token = basic_token Token.is_newline;
-
-(* output token *)
-
-fun output_token state tok =
+fun present_token state tok =
(case tok of
- No_Token => ""
- | Basic_Token tok => Latex.output_token tok
+ No_Token => []
+ | Basic_Token tok => [Latex.text (Latex.output_token tok, Token.pos_of tok)]
| Markup_Token (cmd, source) =>
- "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
+ Latex.string ("%\n\\isamarkup" ^ cmd ^ "{") ::
+ output_text state {markdown = false} source @ [Latex.string "%\n}\n"]
| Markup_Env_Token (cmd, source) =>
- Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source)
+ [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
| Raw_Token source =>
- "%\n" ^ output_text state {markdown = true} source ^ "\n");
+ Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]);
(* command spans *)
@@ -305,7 +306,7 @@
fun edge which f (x: string option, y) =
if x = y then I
- else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
+ else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt)));
val begin_tag = edge #2 Latex.begin_tag;
val end_tag = edge #1 Latex.end_tag;
@@ -315,11 +316,11 @@
in
fun present_span keywords document_tags span state state'
- (tag_stack, active_tag, newline, buffer, present_cont) =
+ (tag_stack, active_tag, newline, latex, present_cont) =
let
val present = fold (fn (tok, (flag, 0)) =>
- Buffer.add (output_token state' tok)
- #> Buffer.add flag
+ fold cons (present_token state' tok)
+ #> cons (Latex.string flag)
| _ => I);
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
@@ -353,8 +354,8 @@
tg :: tgs => (tg, tgs)
| [] => err_bad_nesting (Position.here cmd_pos));
- val buffer' =
- buffer
+ val latex' =
+ latex
|> end_tag edge
|> close_delim (fst present_cont) edge
|> snd present_cont
@@ -364,12 +365,12 @@
val present_cont' =
if newline then (present (#3 srcs), present (#4 srcs))
else (I, present (#3 srcs) #> present (#4 srcs));
- in (tag_stack', active_tag', newline', buffer', present_cont') end;
+ in (tag_stack', active_tag', newline', latex', present_cont') end;
-fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) =
+fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
if not (null tags) then err_bad_nesting " at end of theory"
else
- buffer
+ latex
|> end_tag (active_tag, NONE)
|> close_delim (fst present_cont) (active_tag, NONE)
|> snd present_cont;
@@ -490,15 +491,17 @@
val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>);
fun present_command tr span st st' =
- Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
+ Toplevel.setmp_thread_position tr
+ (present_span keywords document_tags span st st');
fun present _ [] = I
| present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
in
if length command_results = length spans then
- ((NONE, []), NONE, true, Buffer.empty, (I, I))
+ ((NONE, []), NONE, true, [], (I, I))
|> present Toplevel.toplevel (command_results ~~ spans)
|> present_trailer
+ |> rev
else error "Messed-up outer syntax for presentation"
end;
@@ -668,12 +671,13 @@
(** document command **)
-fun document_command markdown (loc, txt) =
+fun document_command {markdown} (loc, txt) =
Toplevel.keep (fn state =>
(case loc of
- NONE => ignore (output_text state markdown txt)
+ NONE => ignore (output_text state {markdown = markdown} txt)
| SOME (_, pos) =>
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
- Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
+ Toplevel.present_local_theory loc (fn state =>
+ ignore (output_text state {markdown = markdown} txt));
end;
--- a/src/Pure/Tools/doc.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Tools/doc.scala Thu Dec 14 11:24:26 2017 +0100
@@ -82,7 +82,7 @@
def view(path: Path)
{
- if (path.is_file) Console.println(Library.trim_line(File.read(path)))
+ if (path.is_file) Output.writeln(Library.trim_line(File.read(path)), stdout = true)
else {
val pdf = path.ext("pdf")
if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
@@ -103,7 +103,7 @@
val docs = getopts(args)
val entries = contents()
- if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
+ if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
else {
docs.foreach(doc =>
entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
--- a/src/Pure/Tools/server.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/Tools/server.scala Thu Dec 14 11:24:26 2017 +0100
@@ -134,11 +134,11 @@
if (operation_list) {
for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
- Console.println(entry.print)
+ Output.writeln(entry.print, stdout = true)
}
else {
val (entry, thread) = start(name, port)
- Console.println(entry.print)
+ Output.writeln(entry.print, stdout = true)
thread.foreach(_.join)
}
})
--- a/src/Pure/build-jars Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/build-jars Thu Dec 14 11:24:26 2017 +0100
@@ -126,6 +126,7 @@
System/progress.scala
System/system_channel.scala
Thy/html.scala
+ Thy/latex.scala
Thy/present.scala
Thy/sessions.scala
Thy/thy_header.scala
--- a/src/Pure/library.ML Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Pure/library.ML Thu Dec 14 11:24:26 2017 +0100
@@ -145,6 +145,7 @@
val unsuffix: string -> string -> string
val trim_line: string -> string
val trim_split_lines: string -> string list
+ val normalize_lines: string -> string
val replicate_string: int -> string -> string
val translate_string: (string -> string) -> string -> string
val encode_lines: string -> string
@@ -723,6 +724,11 @@
val trim_split_lines = trim_line #> split_lines #> map trim_line;
+fun normalize_lines str =
+ if exists_string (fn s => s = "\r") str then
+ split_lines str |> map trim_line |> cat_lines
+ else str;
+
fun replicate_string (0: int) _ = ""
| replicate_string 1 a = a
| replicate_string k a =
--- a/src/Tools/jEdit/src/scala_console.scala Wed Dec 13 19:28:19 2017 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Thu Dec 14 11:24:26 2017 +0100
@@ -110,7 +110,7 @@
private def report_error(str: String)
{
- if (global_console == null || global_err == null) System.err.println(str)
+ if (global_console == null || global_err == null) isabelle.Output.writeln(str)
else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
}