# HG changeset patch
# User wenzelm
# Date 1513247066 -3600
# Node ID 694f29a5433b19128594f9469435dcbe9983792a
# Parent  2f213405cc0eefee5e2b29f7cb223aa39a3690ce# Parent  b335e255ebcc94fd5058f44eb1ed4d0a53059116
merged

diff -r 2f213405cc0e -r 694f29a5433b NEWS
--- 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 ***
 
diff -r 2f213405cc0e -r 694f29a5433b etc/options
diff -r 2f213405cc0e -r 694f29a5433b etc/settings
--- 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
diff -r 2f213405cc0e -r 694f29a5433b lib/Tools/document
--- 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"
diff -r 2f213405cc0e -r 694f29a5433b src/Doc/System/Presentation.thy
--- 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
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Admin/isabelle_cronjob.scala
--- 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)
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/General/antiquote.ML
--- 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 ||
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/General/output.scala
--- 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")
     }
   }
 }
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/General/path.scala
--- 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)
 }
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/PIDE/command.ML
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/PIDE/markup.ML
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/System/getopts.scala
--- 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)
   }
 
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/System/isabelle_process.scala
--- 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 =
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/System/isabelle_tool.scala
--- 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,
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/System/options.scala
--- 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)
   })
 }
 
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/System/progress.scala
--- 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 =
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Thy/document_antiquotations.ML
--- 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
 
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Thy/latex.ML
--- 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);
 
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Thy/latex.scala
--- /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)
+  }
+}
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Thy/present.ML
--- 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"
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Thy/present.scala
--- 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) }
+  })
 }
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Thy/thy_info.ML
--- 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;
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Thy/thy_output.ML
--- 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;
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Tools/doc.scala
--- 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 {
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/Tools/server.scala
--- 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)
       }
     })
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/build-jars
--- 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
diff -r 2f213405cc0e -r 694f29a5433b src/Pure/library.ML
--- 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 =
diff -r 2f213405cc0e -r 694f29a5433b src/Tools/jEdit/src/scala_console.scala
--- 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) }
   }