merged
authorwenzelm
Thu Dec 14 11:24:26 2017 +0100 (17 months ago)
changeset 67198694f29a5433b
parent 67171 2f213405cc0e
parent 67197 b335e255ebcc
child 67199 93600ca0c8d9
merged
lib/Tools/document
     1.1 --- a/NEWS	Wed Dec 13 19:28:19 2017 +0100
     1.2 +++ b/NEWS	Thu Dec 14 11:24:26 2017 +0100
     1.3 @@ -86,6 +86,10 @@
     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 +* Command-line tool "isabelle document" has been re-implemented in
     1.8 +Isabelle/Scala, with simplified arguments and explicit errors from the
     1.9 +latex process. Minor INCOMPATIBILITY.
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  
     3.1 --- a/etc/settings	Wed Dec 13 19:28:19 2017 +0100
     3.2 +++ b/etc/settings	Thu Dec 14 11:24:26 2017 +0100
     3.3 @@ -46,12 +46,17 @@
     3.4  ### Document preparation (cf. isabelle latex/document)
     3.5  ###
     3.6  
     3.7 -ISABELLE_LATEX="latex"
     3.8 -ISABELLE_PDFLATEX="pdflatex"
     3.9 +ISABELLE_LATEX="latex -file-line-error"
    3.10 +ISABELLE_PDFLATEX="pdflatex -file-line-error"
    3.11  ISABELLE_BIBTEX="bibtex"
    3.12  ISABELLE_MAKEINDEX="makeindex"
    3.13  ISABELLE_EPSTOPDF="epstopdf"
    3.14  
    3.15 +if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
    3.16 +  ISABELLE_LATEX="latex -c-style-errors"
    3.17 +  ISABELLE_PDFLATEX="pdflatex -c-style-errors"
    3.18 +fi
    3.19 +
    3.20  
    3.21  ###
    3.22  ### Misc path settings
     4.1 --- a/lib/Tools/document	Wed Dec 13 19:28:19 2017 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,156 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -#
     4.6 -# Author: Markus Wenzel, TU Muenchen
     4.7 -#
     4.8 -# DESCRIPTION: prepare theory session document
     4.9 -
    4.10 -
    4.11 -PRG="$(basename "$0")"
    4.12 -
    4.13 -function usage()
    4.14 -{
    4.15 -  echo
    4.16 -  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
    4.17 -  echo
    4.18 -  echo "  Options are:"
    4.19 -  echo "    -c           cleanup -- be aggressive in removing old stuff"
    4.20 -  echo "    -n NAME      specify document name (default 'document')"
    4.21 -  echo "    -o FORMAT    specify output format: pdf (default), dvi"
    4.22 -  echo "    -t TAGS      specify tagged region markup"
    4.23 -  echo
    4.24 -  echo "  Prepare the theory session document in DIR (default 'document')"
    4.25 -  echo "  producing the specified output format."
    4.26 -  echo
    4.27 -  exit 1
    4.28 -}
    4.29 -
    4.30 -function fail()
    4.31 -{
    4.32 -  echo "$1" >&2
    4.33 -  exit 2
    4.34 -}
    4.35 -
    4.36 -
    4.37 -## process command line
    4.38 -
    4.39 -# options
    4.40 -
    4.41 -CLEAN=""
    4.42 -NAME="document"
    4.43 -OUTFORMAT=pdf
    4.44 -declare -a TAGS=()
    4.45 -
    4.46 -while getopts "cn:o:t:" OPT
    4.47 -do
    4.48 -  case "$OPT" in
    4.49 -    c)
    4.50 -      CLEAN=true
    4.51 -      ;;
    4.52 -    n)
    4.53 -      NAME="$OPTARG"
    4.54 -      ;;
    4.55 -    o)
    4.56 -      OUTFORMAT="$OPTARG"
    4.57 -      ;;
    4.58 -    t)
    4.59 -      splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}")
    4.60 -      ;;
    4.61 -    \?)
    4.62 -      usage
    4.63 -      ;;
    4.64 -  esac
    4.65 -done
    4.66 -
    4.67 -shift $(($OPTIND - 1))
    4.68 -
    4.69 -
    4.70 -# args
    4.71 -
    4.72 -DIR="document"
    4.73 -[ "$#" -ge 1 ] && { DIR="$1"; shift; }
    4.74 -
    4.75 -[ "$#" -ne 0 ] && usage
    4.76 -
    4.77 -
    4.78 -## main
    4.79 -
    4.80 -# check format
    4.81 -
    4.82 -case "$OUTFORMAT" in
    4.83 -  pdf | dvi)
    4.84 -    ;;
    4.85 -  *)
    4.86 -    fail "Bad output format '$OUTFORMAT'"
    4.87 -    ;;
    4.88 -esac
    4.89 -
    4.90 -
    4.91 -# document variants
    4.92 -
    4.93 -ROOT_NAME="root_$NAME"
    4.94 -[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
    4.95 -
    4.96 -function prep_tags ()
    4.97 -{
    4.98 -  (
    4.99 -    for TAG in "${TAGS[@]}"
   4.100 -    do
   4.101 -      case "$TAG" in
   4.102 -        /*)
   4.103 -          echo "\\isafoldtag{${TAG:1}}"
   4.104 -          ;;
   4.105 -        -*)
   4.106 -          echo "\\isadroptag{${TAG:1}}"
   4.107 -          ;;
   4.108 -        +*)
   4.109 -          echo "\\isakeeptag{${TAG:1}}"
   4.110 -          ;;
   4.111 -        *)
   4.112 -          echo "\\isakeeptag{${TAG}}"
   4.113 -          ;;
   4.114 -      esac
   4.115 -    done
   4.116 -    echo
   4.117 -  ) > isabelletags.sty
   4.118 -}
   4.119 -
   4.120 -
   4.121 -# prepare document
   4.122 -
   4.123 -(
   4.124 -  cd "$DIR" || fail "Bad directory '$DIR'"
   4.125 -
   4.126 -  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
   4.127 -
   4.128 -  prep_tags
   4.129 -
   4.130 -  if [ -f build ]; then
   4.131 -    ./build "$OUTFORMAT" "$NAME"
   4.132 -    RC="$?"
   4.133 -  else
   4.134 -    isabelle latex -o sty "$ROOT_NAME.tex" && \
   4.135 -    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
   4.136 -    { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
   4.137 -    { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
   4.138 -    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
   4.139 -    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
   4.140 -    RC="$?"
   4.141 -  fi
   4.142 -
   4.143 -  if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then
   4.144 -    cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
   4.145 -  fi
   4.146 -
   4.147 -  exit "$RC"
   4.148 -)
   4.149 -RC="$?"
   4.150 -
   4.151 -
   4.152 -# install
   4.153 -
   4.154 -[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
   4.155 -
   4.156 -#beware!
   4.157 -[ -n "$CLEAN" ] && rm -rf "$DIR"
   4.158 -
   4.159 -exit "$RC"
     5.1 --- a/src/Doc/System/Presentation.thy	Wed Dec 13 19:28:19 2017 +0100
     5.2 +++ b/src/Doc/System/Presentation.thy	Thu Dec 14 11:24:26 2017 +0100
     5.3 @@ -148,16 +148,17 @@
     5.4    The @{tool_def document} tool prepares logic session documents, processing
     5.5    the sources as provided by the user and generated by Isabelle. Its usage is:
     5.6    @{verbatim [display]
     5.7 -\<open>Usage: isabelle document [OPTIONS] [DIR]
     5.8 +\<open>Usage: isabelle document [OPTIONS]
     5.9  
    5.10    Options are:
    5.11 -    -c           cleanup -- be aggressive in removing old stuff
    5.12 -    -n NAME      specify document name (default 'document')
    5.13 -    -o FORMAT    specify output format: pdf (default), dvi
    5.14 -    -t TAGS      specify tagged region markup
    5.15 +    -d DIR       document output directory (default "output/document")
    5.16 +    -n NAME      document name (default "document")
    5.17 +    -o FORMAT    document format: pdf (default), dvi
    5.18 +    -t TAGS      markup for tagged regions
    5.19  
    5.20 -  Prepare the theory session document in DIR (default 'document')
    5.21 -  producing the specified output format.\<close>}
    5.22 +  Prepare the theory session document in document directory, producing the
    5.23 +  specified output format.
    5.24 +\<close>}
    5.25  
    5.26    This tool is usually run automatically as part of the Isabelle build
    5.27    process, provided document preparation has been enabled via suitable
    5.28 @@ -166,15 +167,13 @@
    5.29    run.
    5.30  
    5.31    \<^medskip>
    5.32 -  The \<^verbatim>\<open>-c\<close> option tells @{tool document} to dispose the document sources
    5.33 -  after successful operation! This is the right thing to do for sources
    5.34 -  generated by an Isabelle process, but take care of your files in manual
    5.35 -  document preparation!
    5.36 +  Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
    5.37 +  is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
    5.38 +  will appear in the parent of this directory.
    5.39  
    5.40    \<^medskip>
    5.41    The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
    5.42 -  the default is ``\<^verbatim>\<open>document.dvi\<close>''. Note that the result will appear in the
    5.43 -  parent of the target \<^verbatim>\<open>DIR\<close>.
    5.44 +  the default is ``\<^verbatim>\<open>document.pdf\<close>''.
    5.45  
    5.46    \<^medskip>
    5.47    The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
    5.48 @@ -234,10 +233,10 @@
    5.49    we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
    5.50  
    5.51    \<^medskip>
    5.52 -  As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
    5.53 -  run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual
    5.54 -  output document is built and installed in its proper place. The generated
    5.55 -  sources are deleted after successful run of {\LaTeX} and friends.
    5.56 +  As a final step of Isabelle document preparation, @{tool document} is run on
    5.57 +  the generated \<^verbatim>\<open>output/document\<close> directory. Thus the actual output document
    5.58 +  is built and installed in its proper place. The generated sources are
    5.59 +  deleted after successful run of {\LaTeX} and friends.
    5.60  
    5.61    Some care is needed if the document output location is configured
    5.62    differently, say within a directory whose content is still required
     6.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Dec 13 19:28:19 2017 +0100
     6.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Dec 14 11:24:26 2017 +0100
     6.3 @@ -346,7 +346,7 @@
     6.4          res match {
     6.5            case Exn.Res(_) => None
     6.6            case Exn.Exn(exn) =>
     6.7 -            System.err.println("Exception trace for " + quote(task.name) + ":")
     6.8 +            Output.writeln("Exception trace for " + quote(task.name) + ":")
     6.9              exn.printStackTrace()
    6.10              val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
    6.11              Some(first_line)
     7.1 --- a/src/Pure/General/antiquote.ML	Wed Dec 13 19:28:19 2017 +0100
     7.2 +++ b/src/Pure/General/antiquote.ML	Thu Dec 14 11:24:26 2017 +0100
     7.3 @@ -76,11 +76,15 @@
     7.4  
     7.5  val err_prefix = "Antiquotation lexical error: ";
     7.6  
     7.7 +val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
     7.8 +
     7.9  val scan_txt =
    7.10 +  scan_nl ||
    7.11    Scan.repeats1
    7.12     (Scan.many1 (fn (s, _) =>
    7.13 -      not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso Symbol.not_eof s) ||
    7.14 -    $$$ "@" --| Scan.ahead (~$$ "{"));
    7.15 +      not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso
    7.16 +        s <> "\n" andalso Symbol.not_eof s) ||
    7.17 +    $$$ "@" --| Scan.ahead (~$$ "{")) @@@ Scan.optional scan_nl [];
    7.18  
    7.19  val scan_antiq_body =
    7.20    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
     8.1 --- a/src/Pure/General/output.scala	Wed Dec 13 19:28:19 2017 +0100
     8.2 +++ b/src/Pure/General/output.scala	Thu Dec 14 11:24:26 2017 +0100
     8.3 @@ -24,24 +24,24 @@
     8.4    def writeln(msg: String, stdout: Boolean = false)
     8.5    {
     8.6      if (msg != "") {
     8.7 -      if (stdout) Console.println(writeln_text(msg))
     8.8 -      else Console.err.println(writeln_text(msg))
     8.9 +      if (stdout) Console.print(writeln_text(msg) + "\n")
    8.10 +      else Console.err.print(writeln_text(msg) + "\n")
    8.11      }
    8.12    }
    8.13  
    8.14    def warning(msg: String, stdout: Boolean = false)
    8.15    {
    8.16      if (msg != "") {
    8.17 -      if (stdout) Console.println(warning_text(msg))
    8.18 -      else Console.err.println(warning_text(msg))
    8.19 +      if (stdout) Console.print(warning_text(msg) + "\n")
    8.20 +      else Console.err.print(warning_text(msg) + "\n")
    8.21      }
    8.22    }
    8.23  
    8.24    def error_message(msg: String, stdout: Boolean = false)
    8.25    {
    8.26      if (msg != "") {
    8.27 -      if (stdout) Console.println(error_message_text(msg))
    8.28 -      else Console.err.println(error_message_text(msg))
    8.29 +      if (stdout) Console.print(error_message_text(msg) + "\n")
    8.30 +      else Console.err.print(error_message_text(msg) + "\n")
    8.31      }
    8.32    }
    8.33  }
     9.1 --- a/src/Pure/General/path.scala	Wed Dec 13 19:28:19 2017 +0100
     9.2 +++ b/src/Pure/General/path.scala	Thu Dec 14 11:24:26 2017 +0100
     9.3 @@ -215,4 +215,7 @@
     9.4  
     9.5    def absolute_file: JFile = File.absolute(file)
     9.6    def canonical_file: JFile = File.canonical(file)
     9.7 +
     9.8 +  def absolute: Path = File.path(absolute_file)
     9.9 +  def canonical: Path = File.path(canonical_file)
    9.10  }
    12.1 --- a/src/Pure/System/getopts.scala	Wed Dec 13 19:28:19 2017 +0100
    12.2 +++ b/src/Pure/System/getopts.scala	Thu Dec 14 11:24:26 2017 +0100
    12.3 @@ -29,7 +29,7 @@
    12.4  {
    12.5    def usage(): Nothing =
    12.6    {
    12.7 -    Console.println(usage_text)
    12.8 +    Output.writeln(usage_text, stdout = true)
    12.9      sys.exit(1)
   12.10    }
   12.11  
    13.1 --- a/src/Pure/System/isabelle_process.scala	Wed Dec 13 19:28:19 2017 +0100
    13.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Dec 14 11:24:26 2017 +0100
    13.3 @@ -41,7 +41,7 @@
    13.4      modes: List[String] = Nil,
    13.5      cwd: JFile = null,
    13.6      env: Map[String, String] = Isabelle_System.settings(),
    13.7 -    receiver: Prover.Receiver = Console.println(_),
    13.8 +    receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
    13.9      xml_cache: XML.Cache = new XML.Cache(),
   13.10      sessions: Option[Sessions.Structure] = None,
   13.11      store: Sessions.Store = Sessions.store()): Prover =
    14.1 --- a/src/Pure/System/isabelle_tool.scala	Wed Dec 13 19:28:19 2017 +0100
    14.2 +++ b/src/Pure/System/isabelle_tool.scala	Thu Dec 14 11:24:26 2017 +0100
    14.3 @@ -114,6 +114,7 @@
    14.4        ML_Process.isabelle_tool,
    14.5        NEWS.isabelle_tool,
    14.6        Options.isabelle_tool,
    14.7 +      Present.isabelle_tool,
    14.8        Profiling_Report.isabelle_tool,
    14.9        Remote_DMG.isabelle_tool,
   14.10        Server.isabelle_tool,
    15.1 --- a/src/Pure/System/options.scala	Wed Dec 13 19:28:19 2017 +0100
    15.2 +++ b/src/Pure/System/options.scala	Thu Dec 14 11:24:26 2017 +0100
    15.3 @@ -185,13 +185,13 @@
    15.4      }
    15.5  
    15.6      if (get_option != "")
    15.7 -      Console.println(options.check_name(get_option).value)
    15.8 +      Output.writeln(options.check_name(get_option).value, stdout = true)
    15.9  
   15.10      if (export_file != "")
   15.11        File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
   15.12  
   15.13      if (get_option == "" && export_file == "")
   15.14 -      Console.println(options.print)
   15.15 +      Output.writeln(options.print, stdout = true)
   15.16    })
   15.17  }
   15.18  
    16.1 --- a/src/Pure/System/progress.scala	Wed Dec 13 19:28:19 2017 +0100
    16.2 +++ b/src/Pure/System/progress.scala	Thu Dec 14 11:24:26 2017 +0100
    16.3 @@ -45,7 +45,7 @@
    16.4  {
    16.5    override def echo(msg: String)
    16.6    {
    16.7 -    if (stderr) Console.err.println(msg) else Console.println(msg)
    16.8 +    Output.writeln(msg, stdout = !stderr)
    16.9    }
   16.10  
   16.11    override def theory(session: String, theory: String): Unit =
    17.1 --- a/src/Pure/Thy/document_antiquotations.ML	Wed Dec 13 19:28:19 2017 +0100
    17.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Thu Dec 14 11:24:26 2017 +0100
    17.3 @@ -44,7 +44,8 @@
    17.4  
    17.5  fun control_antiquotation name s1 s2 =
    17.6    Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
    17.7 -    (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
    17.8 +    (fn {state, ...} =>
    17.9 +      enclose s1 s2 o Latex.output_text o Thy_Output.output_text state {markdown = false});
   17.10  
   17.11  in
   17.12  
    18.1 --- a/src/Pure/Thy/latex.ML	Wed Dec 13 19:28:19 2017 +0100
    18.2 +++ b/src/Pure/Thy/latex.ML	Thu Dec 14 11:24:26 2017 +0100
    18.3 @@ -6,6 +6,13 @@
    18.4  
    18.5  signature LATEX =
    18.6  sig
    18.7 +  type text
    18.8 +  val string: string -> text
    18.9 +  val text: string * Position.T -> text
   18.10 +  val block: text list -> text
   18.11 +  val enclose_body: string -> string -> text list -> text list
   18.12 +  val output_text: text list -> string
   18.13 +  val output_positions: Position.T -> text list -> string
   18.14    val output_name: string -> string
   18.15    val output_ascii: string -> string
   18.16    val latex_control: Symbol.symbol
   18.17 @@ -20,9 +27,9 @@
   18.18    val end_delim: string -> string
   18.19    val begin_tag: string -> string
   18.20    val end_tag: string -> string
   18.21 +  val environment_block: string -> text list -> text
   18.22    val environment: string -> string -> string
   18.23 -  val tex_trailer: string
   18.24 -  val isabelle_theory: string -> string -> string
   18.25 +  val isabelle_body: string -> text list -> text list
   18.26    val symbol_source: (string -> bool) * (string -> bool) ->
   18.27      string -> Symbol.symbol list -> string
   18.28    val theory_entry: string -> string
   18.29 @@ -32,6 +39,50 @@
   18.30  structure Latex: LATEX =
   18.31  struct
   18.32  
   18.33 +(* text with positions *)
   18.34 +
   18.35 +abstype text = Text of string * Position.T | Block of text list
   18.36 +with
   18.37 +
   18.38 +fun string s = Text (s, Position.none);
   18.39 +val text = Text;
   18.40 +val block = Block;
   18.41 +
   18.42 +fun output_text texts =
   18.43 +  let
   18.44 +    fun output (Text (s, _)) = Buffer.add s
   18.45 +      | output (Block body) = fold output body;
   18.46 +  in Buffer.empty |> fold output texts |> Buffer.content end;
   18.47 +
   18.48 +fun output_positions file_pos texts =
   18.49 +  let
   18.50 +    fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b);
   18.51 +    fun add_position p positions =
   18.52 +      let val s = position (apply2 Value.print_int p)
   18.53 +      in positions |> s <> hd positions ? cons s end;
   18.54 +
   18.55 +    fun output (Text (s, pos)) (positions, line) =
   18.56 +          let
   18.57 +            val positions' =
   18.58 +              (case Position.line_of pos of
   18.59 +                NONE => positions
   18.60 +              | SOME l => add_position (line, l) positions);
   18.61 +            val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line;
   18.62 +          in (positions', line') end
   18.63 +      | output (Block body) res = fold output body res;
   18.64 +  in
   18.65 +    (case Position.file_of file_pos of
   18.66 +      NONE => ""
   18.67 +    | SOME file =>
   18.68 +        ([position (Markup.fileN, file), "\\endinput"], 1)
   18.69 +        |> fold output texts |> #1 |> rev |> cat_lines)
   18.70 +  end;
   18.71 +
   18.72 +end;
   18.73 +
   18.74 +fun enclose_body bg en body = string bg :: body @ [string en];
   18.75 +
   18.76 +
   18.77  (* output name for LaTeX macros *)
   18.78  
   18.79  val output_name =
   18.80 @@ -173,25 +224,28 @@
   18.81  (* output token *)
   18.82  
   18.83  fun output_token tok =
   18.84 -  let val s = Token.content_of tok in
   18.85 -    if Token.is_kind Token.Comment tok then ""
   18.86 -    else if Token.is_command tok then
   18.87 -      "\\isacommand{" ^ output_syms s ^ "}"
   18.88 -    else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
   18.89 -      "\\isakeyword{" ^ output_syms s ^ "}"
   18.90 -    else if Token.is_kind Token.String tok then
   18.91 -      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
   18.92 -    else if Token.is_kind Token.Alt_String tok then
   18.93 -      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   18.94 -    else if Token.is_kind Token.Verbatim tok then
   18.95 -      let
   18.96 -        val ants = Antiquote.read (Token.input_of tok);
   18.97 -        val out = implode (map output_syms_antiq ants);
   18.98 -      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   18.99 -    else if Token.is_kind Token.Cartouche tok then
  18.100 -      enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
  18.101 -    else output_syms s
  18.102 -  end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
  18.103 +  let
  18.104 +    val s = Token.content_of tok;
  18.105 +    val output =
  18.106 +      if Token.is_kind Token.Comment tok then ""
  18.107 +      else if Token.is_command tok then
  18.108 +        "\\isacommand{" ^ output_syms s ^ "}"
  18.109 +      else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
  18.110 +        "\\isakeyword{" ^ output_syms s ^ "}"
  18.111 +      else if Token.is_kind Token.String tok then
  18.112 +        enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
  18.113 +      else if Token.is_kind Token.Alt_String tok then
  18.114 +        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
  18.115 +      else if Token.is_kind Token.Verbatim tok then
  18.116 +        let
  18.117 +          val ants = Antiquote.read (Token.input_of tok);
  18.118 +          val out = implode (map output_syms_antiq ants);
  18.119 +        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
  18.120 +      else if Token.is_kind Token.Cartouche tok then
  18.121 +        enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
  18.122 +      else output_syms s;
  18.123 +  in output end
  18.124 +  handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
  18.125  
  18.126  
  18.127  (* tags *)
  18.128 @@ -204,22 +258,21 @@
  18.129  
  18.130  (* theory presentation *)
  18.131  
  18.132 -fun environment name =
  18.133 -  enclose ("%\n\\begin{" ^ output_name name ^ "}%\n") ("%\n\\end{" ^ output_name name ^ "}");
  18.134 +fun environment_delim name =
  18.135 + ("%\n\\begin{" ^ output_name name ^ "}%\n",
  18.136 +  "%\n\\end{" ^ output_name name ^ "}");
  18.137  
  18.138 -val tex_trailer =
  18.139 -  "%%% Local Variables:\n\
  18.140 -  \%%% mode: latex\n\
  18.141 -  \%%% TeX-master: \"root\"\n\
  18.142 -  \%%% End:\n";
  18.143 +fun environment_block name = environment_delim name |-> enclose_body #> block;
  18.144 +fun environment name = environment_delim name |-> enclose;
  18.145  
  18.146 -fun isabelle_theory name txt =
  18.147 -  "%\n\\begin{isabellebody}%\n\
  18.148 -  \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
  18.149 -  "%\n\\end{isabellebody}%\n" ^ tex_trailer;
  18.150 +fun isabelle_body_delim name =
  18.151 + ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n",
  18.152 +  "%\n\\end{isabellebody}%\n");
  18.153 +
  18.154 +fun isabelle_body name = isabelle_body_delim name |-> enclose_body;
  18.155  
  18.156  fun symbol_source known name syms =
  18.157 -  isabelle_theory name
  18.158 +  uncurry enclose (isabelle_body_delim name)
  18.159      ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
  18.160        output_known_symbols known syms);
  18.161  
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Pure/Thy/latex.scala	Thu Dec 14 11:24:26 2017 +0100
    19.3 @@ -0,0 +1,158 @@
    19.4 +/*  Title:      Pure/Thy/latex.scala
    19.5 +    Author:     Makarius
    19.6 +
    19.7 +Support for LaTeX.
    19.8 +*/
    19.9 +
   19.10 +package isabelle
   19.11 +
   19.12 +
   19.13 +import java.io.{File => JFile}
   19.14 +
   19.15 +import scala.annotation.tailrec
   19.16 +
   19.17 +
   19.18 +object Latex
   19.19 +{
   19.20 +  /** latex errors **/
   19.21 +
   19.22 +  def latex_errors(dir: Path, root_name: String): List[String] =
   19.23 +  {
   19.24 +    val root_log_path = dir + Path.explode(root_name).ext("log")
   19.25 +    if (root_log_path.is_file) {
   19.26 +      for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
   19.27 +      yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map("  " + _))
   19.28 +    }
   19.29 +    else Nil
   19.30 +  }
   19.31 +
   19.32 +
   19.33 +  /* generated .tex file */
   19.34 +
   19.35 +  private val File_Pattern = """^%:%file=(.+)%:%$""".r
   19.36 +  private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
   19.37 +
   19.38 +  def read_tex_file(tex_file: Path): Tex_File =
   19.39 +  {
   19.40 +    val positions =
   19.41 +      Line.logical_lines(File.read(tex_file)).reverse.
   19.42 +        takeWhile(_ != "\\endinput").reverse
   19.43 +
   19.44 +    val source_file =
   19.45 +      positions match {
   19.46 +        case File_Pattern(file) :: _ => Some(file)
   19.47 +        case _ => None
   19.48 +      }
   19.49 +
   19.50 +    val source_lines =
   19.51 +      if (source_file.isEmpty) Nil
   19.52 +      else
   19.53 +        positions.flatMap(line =>
   19.54 +          line match {
   19.55 +            case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
   19.56 +            case _ => None
   19.57 +          })
   19.58 +
   19.59 +    new Tex_File(tex_file, source_file, source_lines)
   19.60 +  }
   19.61 +
   19.62 +  final class Tex_File private[Latex](
   19.63 +    tex_file: Path, source_file: Option[String], source_lines: List[(Int, Int)])
   19.64 +  {
   19.65 +    override def toString: String = tex_file.toString
   19.66 +
   19.67 +    def source_position(l: Int): Option[Position.T] =
   19.68 +      source_file match {
   19.69 +        case None => None
   19.70 +        case Some(file) =>
   19.71 +          val source_line =
   19.72 +            (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))(
   19.73 +              { case (_, (_, n)) => n })
   19.74 +          if (source_line == 0) None else Some(Position.Line_File(source_line, file))
   19.75 +      }
   19.76 +
   19.77 +    def position(line: Int): Position.T =
   19.78 +      source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
   19.79 +  }
   19.80 +
   19.81 +
   19.82 +  /* latex log */
   19.83 +
   19.84 +  def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
   19.85 +  {
   19.86 +    val seen_files = Synchronized(Map.empty[JFile, Tex_File])
   19.87 +
   19.88 +    def check_tex_file(path: Path): Option[Tex_File] =
   19.89 +      seen_files.change_result(seen =>
   19.90 +        seen.get(path.file) match {
   19.91 +          case None =>
   19.92 +            if (path.is_file) {
   19.93 +              val tex_file = read_tex_file(path)
   19.94 +              (Some(tex_file), seen + (path.file -> tex_file))
   19.95 +            }
   19.96 +            else (None, seen)
   19.97 +          case some => (some, seen)
   19.98 +        })
   19.99 +
  19.100 +    def tex_file_position(path: Path, line: Int): Position.T =
  19.101 +      check_tex_file(path) match {
  19.102 +        case Some(tex_file) => tex_file.position(line)
  19.103 +        case None => Position.Line_File(line, path.implode)
  19.104 +      }
  19.105 +
  19.106 +    object File_Line_Error
  19.107 +    {
  19.108 +      val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
  19.109 +      def unapply(line: String): Option[(Path, Int, String)] =
  19.110 +        line match {
  19.111 +          case Pattern(file, Value.Int(line), message) =>
  19.112 +            val path = File.standard_path(file)
  19.113 +            if (Path.is_wellformed(path)) {
  19.114 +              val file = (dir + Path.explode(path)).canonical
  19.115 +              if (file.is_file) Some((file, line, message)) else None
  19.116 +            }
  19.117 +            else None
  19.118 +          case _ => None
  19.119 +        }
  19.120 +    }
  19.121 +
  19.122 +    val More_Error =
  19.123 +      List(
  19.124 +        """l\.\d+""",
  19.125 +        "<argument>",
  19.126 +        "<template>",
  19.127 +        "<recently read>",
  19.128 +        "<to be read again>",
  19.129 +        "<inserted text>",
  19.130 +        "<output>",
  19.131 +        "<everypar>",
  19.132 +        "<everymath>",
  19.133 +        "<everydisplay>",
  19.134 +        "<everyhbox>",
  19.135 +        "<everyvbox>",
  19.136 +        "<everyjob>",
  19.137 +        "<everycr>",
  19.138 +        "<mark>",
  19.139 +        "<everyeof>",
  19.140 +        "<write>").mkString("^(?:", "|", ") (.*)$").r
  19.141 +
  19.142 +    @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
  19.143 +      : List[(String, Position.T)] =
  19.144 +    {
  19.145 +      lines match {
  19.146 +        case File_Line_Error((file, line, msg1)) :: rest1 =>
  19.147 +          val pos = tex_file_position(file, line)
  19.148 +          rest1 match {
  19.149 +            case More_Error(msg2) :: rest2 =>
  19.150 +              filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
  19.151 +            case _ =>
  19.152 +              filter(rest1, (msg1, pos) :: result)
  19.153 +          }
  19.154 +        case _ :: rest => filter(rest, result)
  19.155 +        case Nil => result.reverse
  19.156 +      }
  19.157 +    }
  19.158 +
  19.159 +    filter(Line.logical_lines(root_log), Nil)
  19.160 +  }
  19.161 +}
    20.1 --- a/src/Pure/Thy/present.ML	Wed Dec 13 19:28:19 2017 +0100
    20.2 +++ b/src/Pure/Thy/present.ML	Thu Dec 14 11:24:26 2017 +0100
    20.3 @@ -12,7 +12,7 @@
    20.4    val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
    20.5      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
    20.6    val finish: unit -> unit
    20.7 -  val theory_output: theory -> string -> unit
    20.8 +  val theory_output: Position.T -> theory -> Latex.text list -> unit
    20.9    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
   20.10    val display_drafts: Path.T list -> int
   20.11  end;
   20.12 @@ -188,19 +188,16 @@
   20.13  
   20.14  (* isabelle tool wrappers *)
   20.15  
   20.16 -fun isabelle_document {verbose, purge} format name tags dir =
   20.17 +fun isabelle_document {verbose} format name tags dir =
   20.18    let
   20.19 -    val s = "isabelle document -o '" ^ format ^ "' \
   20.20 -      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
   20.21 +    val script =
   20.22 +      "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
   20.23 +        " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
   20.24      val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
   20.25 -    val _ = if verbose then writeln s else ();
   20.26 -    val (out, rc) = Isabelle_System.bash_output s;
   20.27 -    val _ =
   20.28 -      if not (File.exists doc_path) orelse rc <> 0 then
   20.29 -        cat_error out ("Failed to build document " ^ quote (show_path doc_path))
   20.30 -      else if verbose then writeln out
   20.31 -      else ();
   20.32 -    val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
   20.33 +    val _ = if verbose then writeln script else ();
   20.34 +    val {out, err, rc, ...} = Bash.process script;
   20.35 +    val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
   20.36 +    val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
   20.37    in doc_path end;
   20.38  
   20.39  
   20.40 @@ -213,7 +210,7 @@
   20.41    File.write_buffer (Path.append path (tex_path name)) src;
   20.42  
   20.43  fun write_tex_index tex_index path =
   20.44 -  write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
   20.45 +  write_tex (index_buffer tex_index) doc_indexN path;
   20.46  
   20.47  fun finish () =
   20.48    with_session_info () (fn {name, chapter, info, info_path, doc_format,
   20.49 @@ -243,6 +240,8 @@
   20.50      fun document_job doc_prefix backdrop (doc_name, tags) =
   20.51        let
   20.52          val doc_dir = Path.append doc_prefix (Path.basic doc_name);
   20.53 +        fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else ();
   20.54 +        val _ = purge ();
   20.55          val _ = Isabelle_System.mkdirs doc_dir;
   20.56          val _ =
   20.57            Isabelle_System.bash ("isabelle latex -o sty " ^
   20.58 @@ -255,7 +254,7 @@
   20.59              write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
   20.60        in
   20.61          fn () =>
   20.62 -          (isabelle_document {verbose = true, purge = backdrop} doc_format doc_name tags doc_dir,
   20.63 +          (isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (),
   20.64              fn doc =>
   20.65                if verbose orelse not backdrop then
   20.66                  Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
   20.67 @@ -279,11 +278,15 @@
   20.68  
   20.69  (* theory elements *)
   20.70  
   20.71 -fun theory_output thy tex =
   20.72 +fun theory_output pos thy body =
   20.73    with_session_info () (fn _ =>
   20.74      if is_session_theory thy then
   20.75 -      let val name = Context.theory_name thy;
   20.76 -      in change_theory_info name (fn (_, html) => (Latex.isabelle_theory name tex, html)) end
   20.77 +      let val name = Context.theory_name thy in
   20.78 +        (change_theory_info name o apfst)
   20.79 +          (fn _ =>
   20.80 +            let val latex = Latex.isabelle_body name body
   20.81 +            in Latex.output_text latex ^ Latex.output_positions pos latex end)
   20.82 +      end
   20.83      else ());
   20.84  
   20.85  fun theory_link (curr_chapter, curr_session) thy =
   20.86 @@ -356,8 +359,7 @@
   20.87        |> File.write (Path.append doc_path (tex_path name)));
   20.88      val _ = write_tex_index tex_index doc_path;
   20.89  
   20.90 -    val result =
   20.91 -      isabelle_document {verbose = false, purge = true} "pdf" documentN "" doc_path;
   20.92 +    val result = isabelle_document {verbose = false} "pdf" documentN "" doc_path;
   20.93  
   20.94      val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
   20.95      val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
    21.1 --- a/src/Pure/Thy/present.scala	Wed Dec 13 19:28:19 2017 +0100
    21.2 +++ b/src/Pure/Thy/present.scala	Thu Dec 14 11:24:26 2017 +0100
    21.3 @@ -131,4 +131,129 @@
    21.4    {
    21.5      make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
    21.6    }
    21.7 +
    21.8 +
    21.9 +
   21.10 +  /** build document **/
   21.11 +
   21.12 +  val default_document_name = "document"
   21.13 +  val default_document_format = "pdf"
   21.14 +  val document_formats = List("pdf", "dvi")
   21.15 +  def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name)
   21.16 +
   21.17 +  def document_tags(tags: List[String]): String =
   21.18 +  {
   21.19 +    cat_lines(
   21.20 +      tags.map(tag =>
   21.21 +        tag.toList match {
   21.22 +          case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
   21.23 +          case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
   21.24 +          case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
   21.25 +          case cs => "\\isafoldtag{" + cs.mkString + "}"
   21.26 +        })) + "\n"
   21.27 +  }
   21.28 +
   21.29 +  def build_document(
   21.30 +    document_name: String = default_document_name,
   21.31 +    document_format: String = default_document_format,
   21.32 +    document_dir: Option[Path] = None,
   21.33 +    tags: List[String] = Nil)
   21.34 +  {
   21.35 +    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
   21.36 +
   21.37 +    if (!document_formats.contains(document_format))
   21.38 +      error("Bad document output format: " + quote(document_format))
   21.39 +
   21.40 +    val dir = document_dir getOrElse default_document_dir(document_name)
   21.41 +    if (!dir.is_dir) error("Bad document output directory " + dir)
   21.42 +
   21.43 +    val root_name =
   21.44 +    {
   21.45 +      val root1 = "root_" + document_name
   21.46 +      if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root"
   21.47 +    }
   21.48 +
   21.49 +
   21.50 +    /* bash scripts */
   21.51 +
   21.52 +    def root_bash(ext: String): String = Bash.string(root_name + "." + ext)
   21.53 +
   21.54 +    def latex_bash(fmt: String, ext: String = "tex"): String =
   21.55 +      "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext)
   21.56 +
   21.57 +    def bash(script: String): Process_Result =
   21.58 +      Isabelle_System.bash(script, cwd = dir.file)
   21.59 +
   21.60 +
   21.61 +    /* prepare document */
   21.62 +
   21.63 +    File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags))
   21.64 +
   21.65 +    val result =
   21.66 +      if ((dir + Path.explode("build")).is_file) {
   21.67 +        bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name))
   21.68 +      }
   21.69 +      else {
   21.70 +        bash(
   21.71 +          List(
   21.72 +            latex_bash("sty"),
   21.73 +            latex_bash(document_format),
   21.74 +            "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
   21.75 +            "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
   21.76 +            latex_bash(document_format),
   21.77 +            latex_bash(document_format)).mkString(" && "))
   21.78 +      }
   21.79 +
   21.80 +
   21.81 +    /* result */
   21.82 +
   21.83 +    if (!result.ok) {
   21.84 +      cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
   21.85 +        "Failed to build document in " + File.path(dir.absolute_file))
   21.86 +    }
   21.87 +
   21.88 +    bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
   21.89 +      root_bash(document_format) + " " + File.bash_path(document_target)).check
   21.90 +  }
   21.91 +
   21.92 +
   21.93 +  /* Isabelle tool wrapper */
   21.94 +
   21.95 +  val isabelle_tool =
   21.96 +    Isabelle_Tool("document", "prepare theory session document", args =>
   21.97 +  {
   21.98 +    var document_dir: Option[Path] = None
   21.99 +    var document_name = default_document_name
  21.100 +    var document_format = default_document_format
  21.101 +    var tags: List[String] = Nil
  21.102 +
  21.103 +    val getopts = Getopts("""
  21.104 +Usage: isabelle document [OPTIONS]
  21.105 +
  21.106 +  Options are:
  21.107 +    -d DIR       document output directory (default """ +
  21.108 +      default_document_dir(default_document_name) + """)
  21.109 +    -n NAME      document name (default """ + quote(default_document_name) + """)
  21.110 +    -o FORMAT    document format: """ +
  21.111 +      commas(document_formats.map(fmt =>
  21.112 +        fmt + (if (fmt == default_document_format) " (default)" else ""))) + """
  21.113 +    -t TAGS      markup for tagged regions
  21.114 +
  21.115 +  Prepare the theory session document in document directory, producing the
  21.116 +  specified output format.
  21.117 +""",
  21.118 +      "d:" -> (arg => document_dir = Some(Path.explode(arg))),
  21.119 +      "n:" -> (arg => document_name = arg),
  21.120 +      "o:" -> (arg => document_format = arg),
  21.121 +      "t:" -> (arg => tags = space_explode(',', arg)))
  21.122 +
  21.123 +    val more_args = getopts(args)
  21.124 +    if (more_args.nonEmpty) getopts.usage()
  21.125 +
  21.126 +    try {
  21.127 +      build_document(document_dir = document_dir, document_name = document_name,
  21.128 +        document_format = document_format, tags = tags)
  21.129 +    }
  21.130 +    catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) }
  21.131 +  })
  21.132  }
    22.1 --- a/src/Pure/Thy/thy_info.ML	Wed Dec 13 19:28:19 2017 +0100
    22.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Dec 14 11:24:26 2017 +0100
    22.3 @@ -268,8 +268,8 @@
    22.4        in
    22.5          if exists (Toplevel.is_skipped_proof o #2) res then ()
    22.6          else
    22.7 -          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
    22.8 -          in if document then Present.theory_output thy tex_source else () end
    22.9 +          let val body = Thy_Output.present_thy thy res toks;
   22.10 +          in if document then Present.theory_output text_pos thy body else () end
   22.11        end;
   22.12  
   22.13    in (thy, present, size text) end;
    23.1 --- a/src/Pure/Thy/thy_output.ML	Wed Dec 13 19:28:19 2017 +0100
    23.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Dec 14 11:24:26 2017 +0100
    23.3 @@ -24,8 +24,9 @@
    23.4    val boolean: string -> bool
    23.5    val integer: string -> int
    23.6    val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
    23.7 -  val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string
    23.8 -  val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    23.9 +  val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
   23.10 +  val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
   23.11 +    Token.T list -> Latex.text list
   23.12    val pretty_text: Proof.context -> string -> Pretty.T
   23.13    val pretty_term: Proof.context -> term -> Pretty.T
   23.14    val pretty_thm: Proof.context -> thm -> Pretty.T
   23.15 @@ -35,8 +36,8 @@
   23.16    val string_of_margin: Proof.context -> Pretty.T -> string
   23.17    val output: Proof.context -> Pretty.T list -> string
   23.18    val verbatim_text: Proof.context -> string -> string
   23.19 -  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
   23.20 -    Toplevel.transition -> Toplevel.transition
   23.21 +  val document_command: {markdown: bool} ->
   23.22 +    (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
   23.23  end;
   23.24  
   23.25  structure Thy_Output: THY_OUTPUT =
   23.26 @@ -208,18 +209,20 @@
   23.27          Position.report pos (Markup.language_document (Input.is_delimited source))
   23.28        else ();
   23.29  
   23.30 -    val output_antiquotes = map (eval_antiquote state) #> implode;
   23.31 +    val output_antiquotes =
   23.32 +      map (fn ant => Latex.text (eval_antiquote state ant, #1 (Antiquote.range [ant])));
   23.33  
   23.34      fun output_line line =
   23.35 -      (if Markdown.line_is_item line then "\\item " else "") ^
   23.36 +      (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
   23.37          output_antiquotes (Markdown.line_content line);
   23.38  
   23.39 -    fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
   23.40 -    and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
   23.41 +    fun output_block (Markdown.Par lines) =
   23.42 +          Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines))
   23.43        | output_block (Markdown.List {kind, body, ...}) =
   23.44 -          Latex.environment (Markdown.print_kind kind) (output_blocks body);
   23.45 +          Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
   23.46 +    and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
   23.47    in
   23.48 -    if Toplevel.is_skipped_proof state then ""
   23.49 +    if Toplevel.is_skipped_proof state then []
   23.50      else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
   23.51      then
   23.52        let
   23.53 @@ -259,19 +262,17 @@
   23.54  val blank_token = basic_token Token.is_blank;
   23.55  val newline_token = basic_token Token.is_newline;
   23.56  
   23.57 -
   23.58 -(* output token *)
   23.59 -
   23.60 -fun output_token state tok =
   23.61 +fun present_token state tok =
   23.62    (case tok of
   23.63 -    No_Token => ""
   23.64 -  | Basic_Token tok => Latex.output_token tok
   23.65 +    No_Token => []
   23.66 +  | Basic_Token tok => [Latex.text (Latex.output_token tok, Token.pos_of tok)]
   23.67    | Markup_Token (cmd, source) =>
   23.68 -      "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
   23.69 +      Latex.string ("%\n\\isamarkup" ^ cmd ^ "{") ::
   23.70 +        output_text state {markdown = false} source @ [Latex.string "%\n}\n"]
   23.71    | Markup_Env_Token (cmd, source) =>
   23.72 -      Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source)
   23.73 +      [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
   23.74    | Raw_Token source =>
   23.75 -      "%\n" ^ output_text state {markdown = true} source ^ "\n");
   23.76 +      Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]);
   23.77  
   23.78  
   23.79  (* command spans *)
   23.80 @@ -305,7 +306,7 @@
   23.81  
   23.82  fun edge which f (x: string option, y) =
   23.83    if x = y then I
   23.84 -  else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
   23.85 +  else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt)));
   23.86  
   23.87  val begin_tag = edge #2 Latex.begin_tag;
   23.88  val end_tag = edge #1 Latex.end_tag;
   23.89 @@ -315,11 +316,11 @@
   23.90  in
   23.91  
   23.92  fun present_span keywords document_tags span state state'
   23.93 -    (tag_stack, active_tag, newline, buffer, present_cont) =
   23.94 +    (tag_stack, active_tag, newline, latex, present_cont) =
   23.95    let
   23.96      val present = fold (fn (tok, (flag, 0)) =>
   23.97 -        Buffer.add (output_token state' tok)
   23.98 -        #> Buffer.add flag
   23.99 +        fold cons (present_token state' tok)
  23.100 +        #> cons (Latex.string flag)
  23.101        | _ => I);
  23.102  
  23.103      val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
  23.104 @@ -353,8 +354,8 @@
  23.105            tg :: tgs => (tg, tgs)
  23.106          | [] => err_bad_nesting (Position.here cmd_pos));
  23.107  
  23.108 -    val buffer' =
  23.109 -      buffer
  23.110 +    val latex' =
  23.111 +      latex
  23.112        |> end_tag edge
  23.113        |> close_delim (fst present_cont) edge
  23.114        |> snd present_cont
  23.115 @@ -364,12 +365,12 @@
  23.116      val present_cont' =
  23.117        if newline then (present (#3 srcs), present (#4 srcs))
  23.118        else (I, present (#3 srcs) #> present (#4 srcs));
  23.119 -  in (tag_stack', active_tag', newline', buffer', present_cont') end;
  23.120 +  in (tag_stack', active_tag', newline', latex', present_cont') end;
  23.121  
  23.122 -fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) =
  23.123 +fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
  23.124    if not (null tags) then err_bad_nesting " at end of theory"
  23.125    else
  23.126 -    buffer
  23.127 +    latex
  23.128      |> end_tag (active_tag, NONE)
  23.129      |> close_delim (fst present_cont) (active_tag, NONE)
  23.130      |> snd present_cont;
  23.131 @@ -490,15 +491,17 @@
  23.132      val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>);
  23.133  
  23.134      fun present_command tr span st st' =
  23.135 -      Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
  23.136 +      Toplevel.setmp_thread_position tr
  23.137 +        (present_span keywords document_tags span st st');
  23.138  
  23.139      fun present _ [] = I
  23.140        | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
  23.141    in
  23.142      if length command_results = length spans then
  23.143 -      ((NONE, []), NONE, true, Buffer.empty, (I, I))
  23.144 +      ((NONE, []), NONE, true, [], (I, I))
  23.145        |> present Toplevel.toplevel (command_results ~~ spans)
  23.146        |> present_trailer
  23.147 +      |> rev
  23.148      else error "Messed-up outer syntax for presentation"
  23.149    end;
  23.150  
  23.151 @@ -668,12 +671,13 @@
  23.152  
  23.153  (** document command **)
  23.154  
  23.155 -fun document_command markdown (loc, txt) =
  23.156 +fun document_command {markdown} (loc, txt) =
  23.157    Toplevel.keep (fn state =>
  23.158      (case loc of
  23.159 -      NONE => ignore (output_text state markdown txt)
  23.160 +      NONE => ignore (output_text state {markdown = markdown} txt)
  23.161      | SOME (_, pos) =>
  23.162          error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
  23.163 -  Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
  23.164 +  Toplevel.present_local_theory loc (fn state =>
  23.165 +    ignore (output_text state {markdown = markdown} txt));
  23.166  
  23.167  end;
    24.1 --- a/src/Pure/Tools/doc.scala	Wed Dec 13 19:28:19 2017 +0100
    24.2 +++ b/src/Pure/Tools/doc.scala	Thu Dec 14 11:24:26 2017 +0100
    24.3 @@ -82,7 +82,7 @@
    24.4  
    24.5    def view(path: Path)
    24.6    {
    24.7 -    if (path.is_file) Console.println(Library.trim_line(File.read(path)))
    24.8 +    if (path.is_file) Output.writeln(Library.trim_line(File.read(path)), stdout = true)
    24.9      else {
   24.10        val pdf = path.ext("pdf")
   24.11        if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
   24.12 @@ -103,7 +103,7 @@
   24.13      val docs = getopts(args)
   24.14  
   24.15      val entries = contents()
   24.16 -    if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
   24.17 +    if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
   24.18      else {
   24.19        docs.foreach(doc =>
   24.20          entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
    25.1 --- a/src/Pure/Tools/server.scala	Wed Dec 13 19:28:19 2017 +0100
    25.2 +++ b/src/Pure/Tools/server.scala	Thu Dec 14 11:24:26 2017 +0100
    25.3 @@ -134,11 +134,11 @@
    25.4  
    25.5        if (operation_list) {
    25.6          for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
    25.7 -          Console.println(entry.print)
    25.8 +          Output.writeln(entry.print, stdout = true)
    25.9        }
   25.10        else {
   25.11          val (entry, thread) = start(name, port)
   25.12 -        Console.println(entry.print)
   25.13 +        Output.writeln(entry.print, stdout = true)
   25.14          thread.foreach(_.join)
   25.15        }
   25.16      })
    26.1 --- a/src/Pure/build-jars	Wed Dec 13 19:28:19 2017 +0100
    26.2 +++ b/src/Pure/build-jars	Thu Dec 14 11:24:26 2017 +0100
    26.3 @@ -126,6 +126,7 @@
    26.4    System/progress.scala
    26.5    System/system_channel.scala
    26.6    Thy/html.scala
    26.7 +  Thy/latex.scala
    26.8    Thy/present.scala
    26.9    Thy/sessions.scala
   26.10    Thy/thy_header.scala
    27.1 --- a/src/Pure/library.ML	Wed Dec 13 19:28:19 2017 +0100
    27.2 +++ b/src/Pure/library.ML	Thu Dec 14 11:24:26 2017 +0100
    27.3 @@ -145,6 +145,7 @@
    27.4    val unsuffix: string -> string -> string
    27.5    val trim_line: string -> string
    27.6    val trim_split_lines: string -> string list
    27.7 +  val normalize_lines: string -> string
    27.8    val replicate_string: int -> string -> string
    27.9    val translate_string: (string -> string) -> string -> string
   27.10    val encode_lines: string -> string
   27.11 @@ -723,6 +724,11 @@
   27.12  
   27.13  val trim_split_lines = trim_line #> split_lines #> map trim_line;
   27.14  
   27.15 +fun normalize_lines str =
   27.16 +  if exists_string (fn s => s = "\r") str then
   27.17 +    split_lines str |> map trim_line |> cat_lines
   27.18 +  else str;
   27.19 +
   27.20  fun replicate_string (0: int) _ = ""
   27.21    | replicate_string 1 a = a
   27.22    | replicate_string k a =
    28.1 --- a/src/Tools/jEdit/src/scala_console.scala	Wed Dec 13 19:28:19 2017 +0100
    28.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Thu Dec 14 11:24:26 2017 +0100
    28.3 @@ -110,7 +110,7 @@
    28.4  
    28.5    private def report_error(str: String)
    28.6    {
    28.7 -    if (global_console == null || global_err == null) System.err.println(str)
    28.8 +    if (global_console == null || global_err == null) isabelle.Output.writeln(str)
    28.9      else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
   28.10    }
   28.11