positions as postlude: avoid intrusion of odd %-forms into main tex source;
authorwenzelm
Wed Dec 13 16:18:40 2017 +0100 (17 months ago)
changeset 671941c0a6a957114
parent 67193 4ade0d387429
child 67195 6be90977f882
positions as postlude: avoid intrusion of odd %-forms into main tex source;
NEWS
etc/options
src/Pure/PIDE/command.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/latex.scala
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Tue Dec 12 18:53:40 2017 +0100
     1.2 +++ b/NEWS	Wed Dec 13 16:18:40 2017 +0100
     1.3 @@ -87,12 +87,8 @@
     1.4  more accurately: only terminal proof steps ('by' etc.) are skipped.
     1.5  
     1.6  * Command-line tool "isabelle document" has been re-implemented in
     1.7 -Isabelle/Scala, with simplified arguments. Minor INCOMPATIBILITY.
     1.8 -
     1.9 -* Original source positions are inlined into generated tex files: this
    1.10 -improves error messages by "isabelle document", but may sometimes
    1.11 -confuse LaTeX. Rare INCOMPATIBILITY, set option
    1.12 -"document_positions=false" to avoid this.
    1.13 +Isabelle/Scala, with simplified arguments and explicit errors from the
    1.14 +latex process. Minor INCOMPATIBILITY.
    1.15  
    1.16  
    1.17  *** HOL ***
     2.1 --- a/etc/options	Tue Dec 12 18:53:40 2017 +0100
     2.2 +++ b/etc/options	Wed Dec 13 16:18:40 2017 +0100
     2.3 @@ -13,8 +13,6 @@
     2.4    -- "alternative document variants (separated by colons)"
     2.5  option document_tags : string = ""
     2.6    -- "default command tags (separated by commas)"
     2.7 -option document_positions : bool = true
     2.8 -  -- "inline original source positions into generated tex files"
     2.9  
    2.10  option thy_output_display : bool = false
    2.11    -- "indicate output as multi-line display-style material"
     3.1 --- a/src/Pure/PIDE/command.ML	Tue Dec 12 18:53:40 2017 +0100
     3.2 +++ b/src/Pure/PIDE/command.ML	Wed Dec 13 16:18:40 2017 +0100
     3.3 @@ -199,7 +199,7 @@
     3.4    Toplevel.setmp_thread_position tr
     3.5      (fn () =>
     3.6        Outer_Syntax.side_comments span |> maps (fn cmt =>
     3.7 -        (Thy_Output.output_text st' {markdown = false, positions = false} (Token.input_of cmt); [])
     3.8 +        (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
     3.9            handle exn =>
    3.10              if Exn.is_interrupt exn then Exn.reraise exn
    3.11              else Runtime.exn_messages exn)) ();
     4.1 --- a/src/Pure/Thy/document_antiquotations.ML	Tue Dec 12 18:53:40 2017 +0100
     4.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Wed Dec 13 16:18:40 2017 +0100
     4.3 @@ -45,7 +45,7 @@
     4.4  fun control_antiquotation name s1 s2 =
     4.5    Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
     4.6      (fn {state, ...} =>
     4.7 -      enclose s1 s2 o Thy_Output.output_text state {markdown = false, positions = false});
     4.8 +      enclose s1 s2 o Latex.output_text o Thy_Output.output_text state {markdown = false});
     4.9  
    4.10  in
    4.11  
     5.1 --- a/src/Pure/Thy/latex.ML	Tue Dec 12 18:53:40 2017 +0100
     5.2 +++ b/src/Pure/Thy/latex.ML	Wed Dec 13 16:18:40 2017 +0100
     5.3 @@ -6,6 +6,13 @@
     5.4  
     5.5  signature LATEX =
     5.6  sig
     5.7 +  type text
     5.8 +  val string: string -> text
     5.9 +  val text: string * Position.T -> text
    5.10 +  val block: text list -> text
    5.11 +  val enclose_body: string -> string -> text list -> text list
    5.12 +  val output_text: text list -> string
    5.13 +  val output_positions: Position.T -> text list -> string
    5.14    val output_name: string -> string
    5.15    val output_ascii: string -> string
    5.16    val latex_control: Symbol.symbol
    5.17 @@ -15,14 +22,14 @@
    5.18      Symbol.symbol list -> string
    5.19    val output_symbols: Symbol.symbol list -> string
    5.20    val output_syms: string -> string
    5.21 -  val line_output: Position.T -> string -> string
    5.22    val output_token: Token.T -> string
    5.23    val begin_delim: string -> string
    5.24    val end_delim: string -> string
    5.25    val begin_tag: string -> string
    5.26    val end_tag: string -> string
    5.27 +  val environment_block: string -> text list -> text
    5.28    val environment: string -> string -> string
    5.29 -  val isabelle_theory: Position.T -> string -> string -> string
    5.30 +  val isabelle_body: string -> text list -> text list
    5.31    val symbol_source: (string -> bool) * (string -> bool) ->
    5.32      string -> Symbol.symbol list -> string
    5.33    val theory_entry: string -> string
    5.34 @@ -32,6 +39,46 @@
    5.35  structure Latex: LATEX =
    5.36  struct
    5.37  
    5.38 +(* text with positions *)
    5.39 +
    5.40 +abstype text = Text of string * Position.T | Block of text list
    5.41 +with
    5.42 +
    5.43 +fun string s = Text (s, Position.none);
    5.44 +val text = Text;
    5.45 +val block = Block;
    5.46 +
    5.47 +fun output_text texts =
    5.48 +  let
    5.49 +    fun output (Text (s, _)) = Buffer.add s
    5.50 +      | output (Block body) = fold output body;
    5.51 +  in Buffer.empty |> fold output texts |> Buffer.content end;
    5.52 +
    5.53 +fun output_positions file_pos texts =
    5.54 +  let
    5.55 +    fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b);
    5.56 +    fun output (Text (s, pos)) (positions, line) =
    5.57 +          let
    5.58 +            val positions' =
    5.59 +              (case Position.line_of pos of
    5.60 +                NONE => positions
    5.61 +              | SOME l => position (apply2 Value.print_int (line, l)) :: positions);
    5.62 +            val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line;
    5.63 +          in (positions', line') end
    5.64 +      | output (Block body) res = fold output body res;
    5.65 +  in
    5.66 +    (case Position.file_of file_pos of
    5.67 +      NONE => ""
    5.68 +    | SOME file =>
    5.69 +        ([position (Markup.fileN, file), "\\endinput"], 1)
    5.70 +        |> fold output texts |> #1 |> rev |> cat_lines)
    5.71 +  end;
    5.72 +
    5.73 +end;
    5.74 +
    5.75 +fun enclose_body bg en body = string bg :: body @ [string en];
    5.76 +
    5.77 +
    5.78  (* output name for LaTeX macros *)
    5.79  
    5.80  val output_name =
    5.81 @@ -170,30 +217,6 @@
    5.82  end;
    5.83  
    5.84  
    5.85 -(* positions *)
    5.86 -
    5.87 -fun output_prop (a, b) = enclose "%:%" "%:%\n" (a ^ "=" ^ b);
    5.88 -
    5.89 -fun output_file pos =
    5.90 -  (case Position.file_of pos of
    5.91 -    NONE => ""
    5.92 -  | SOME file => output_prop (Markup.fileN, file));
    5.93 -
    5.94 -
    5.95 -val is_blank_line = forall_string (fn s => s = " " orelse s = "\t");
    5.96 -
    5.97 -fun line_output pos output =
    5.98 -  (case Position.line_of pos of
    5.99 -    NONE => output
   5.100 -  | SOME n =>
   5.101 -      (case take_prefix is_blank_line (split_lines output) of
   5.102 -        (_, []) => output
   5.103 -      | (blank, rest) =>
   5.104 -          cat_lines blank ^ " %\n" ^
   5.105 -          output_prop (Markup.lineN, Value.print_int n) ^
   5.106 -          cat_lines rest));
   5.107 -
   5.108 -
   5.109  (* output token *)
   5.110  
   5.111  fun output_token tok =
   5.112 @@ -231,17 +254,22 @@
   5.113  
   5.114  (* theory presentation *)
   5.115  
   5.116 -fun environment name =
   5.117 -  enclose ("%\n\\begin{" ^ output_name name ^ "}%\n") ("%\n\\end{" ^ output_name name ^ "}");
   5.118 +fun environment_delim name =
   5.119 + ("%\n\\begin{" ^ output_name name ^ "}%\n",
   5.120 +  "%\n\\end{" ^ output_name name ^ "}");
   5.121  
   5.122 -fun isabelle_theory pos name txt =
   5.123 -  output_file pos ^
   5.124 -  "\\begin{isabellebody}%\n\
   5.125 -  \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
   5.126 -  "%\n\\end{isabellebody}%\n";
   5.127 +fun environment_block name = environment_delim name |-> enclose_body #> block;
   5.128 +fun environment name = environment_delim name |-> enclose;
   5.129 +
   5.130 +fun isabelle_body_delim name =
   5.131 + ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n",
   5.132 +  "%\n\\end{isabellebody}%\n");
   5.133 +
   5.134 +fun isabelle_body name = isabelle_body_delim name |-> enclose_body;
   5.135  
   5.136  fun symbol_source known name syms =
   5.137 -  isabelle_theory Position.none name
   5.138 +  isabelle_body_delim name
   5.139 +  |-> enclose
   5.140      ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
   5.141        output_known_symbols known syms);
   5.142  
     6.1 --- a/src/Pure/Thy/latex.scala	Tue Dec 12 18:53:40 2017 +0100
     6.2 +++ b/src/Pure/Thy/latex.scala	Wed Dec 13 16:18:40 2017 +0100
     6.3 @@ -30,40 +30,46 @@
     6.4    /* generated .tex file */
     6.5  
     6.6    private val File_Pattern = """^%:%file=(.+)%:%$""".r
     6.7 -  private val Line_Pattern = """^*%:%line=(\d+)%:%$""".r
     6.8 +  private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
     6.9  
    6.10    def read_tex_file(tex_file: Path): Tex_File =
    6.11 -    new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray)
    6.12 +  {
    6.13 +    val positions =
    6.14 +      Line.logical_lines(File.read(tex_file)).reverse.
    6.15 +        takeWhile(_ != "\\endinput").reverse
    6.16 +
    6.17 +    val source_file =
    6.18 +      positions match {
    6.19 +        case File_Pattern(file) :: _ => Some(file)
    6.20 +        case _ => None
    6.21 +      }
    6.22  
    6.23 -  final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String])
    6.24 +    val source_lines =
    6.25 +      if (source_file.isEmpty) Nil
    6.26 +      else
    6.27 +        positions.flatMap(line =>
    6.28 +          line match {
    6.29 +            case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
    6.30 +            case _ => None
    6.31 +          })
    6.32 +
    6.33 +    new Tex_File(tex_file, source_file, source_lines)
    6.34 +  }
    6.35 +
    6.36 +  final class Tex_File private[Latex](
    6.37 +    tex_file: Path, source_file: Option[String], source_lines: List[(Int, Int)])
    6.38    {
    6.39      override def toString: String = tex_file.toString
    6.40  
    6.41 -    val source_file: Option[String] =
    6.42 -      if (tex_lines.nonEmpty) {
    6.43 -        tex_lines(0) match {
    6.44 -          case File_Pattern(file) => Some(file)
    6.45 -          case _ => None
    6.46 -        }
    6.47 +    def source_position(l: Int): Option[Position.T] =
    6.48 +      source_file match {
    6.49 +        case None => None
    6.50 +        case Some(file) =>
    6.51 +          val source_line =
    6.52 +            (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))(
    6.53 +              { case (_, (_, n)) => n })
    6.54 +          if (source_line == 0) None else Some(Position.Line_File(source_line, file))
    6.55        }
    6.56 -      else None
    6.57 -
    6.58 -    private def prev_lines_iterator(l: Int): Iterator[String] =
    6.59 -      if (0 < l && l <= tex_lines.length)
    6.60 -        Range.inclusive(l - 1, 0, -1).iterator.map(tex_lines(_))
    6.61 -      else Iterator.empty
    6.62 -
    6.63 -    def source_position(l: Int): Option[Position.T] =
    6.64 -      (for {
    6.65 -        file <- source_file.iterator
    6.66 -        s <- prev_lines_iterator(l)
    6.67 -        line <-
    6.68 -          (s match {
    6.69 -            case Line_Pattern(Value.Int(line)) => Some(line)
    6.70 -            case _ => None
    6.71 -          })
    6.72 -      }
    6.73 -      yield { Position.Line_File(line, file) }).toStream.headOption
    6.74  
    6.75      def position(line: Int): Position.T =
    6.76        source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
     7.1 --- a/src/Pure/Thy/present.ML	Tue Dec 12 18:53:40 2017 +0100
     7.2 +++ b/src/Pure/Thy/present.ML	Wed Dec 13 16:18:40 2017 +0100
     7.3 @@ -12,7 +12,7 @@
     7.4    val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     7.5      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
     7.6    val finish: unit -> unit
     7.7 -  val theory_output: Position.T -> theory -> string -> unit
     7.8 +  val theory_output: Position.T -> theory -> Latex.text list -> unit
     7.9    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    7.10    val display_drafts: Path.T list -> int
    7.11  end;
    7.12 @@ -278,11 +278,15 @@
    7.13  
    7.14  (* theory elements *)
    7.15  
    7.16 -fun theory_output pos thy tex =
    7.17 +fun theory_output pos thy body =
    7.18    with_session_info () (fn _ =>
    7.19      if is_session_theory thy then
    7.20 -      let val name = Context.theory_name thy;
    7.21 -      in change_theory_info name (fn (_, html) => (Latex.isabelle_theory pos name tex, html)) end
    7.22 +      let val name = Context.theory_name thy in
    7.23 +        (change_theory_info name o apfst)
    7.24 +          (fn _ =>
    7.25 +            let val latex = Latex.isabelle_body name body
    7.26 +            in Latex.output_text latex ^ Latex.output_positions pos latex end)
    7.27 +      end
    7.28      else ());
    7.29  
    7.30  fun theory_link (curr_chapter, curr_session) thy =
     8.1 --- a/src/Pure/Thy/thy_info.ML	Tue Dec 12 18:53:40 2017 +0100
     8.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Dec 13 16:18:40 2017 +0100
     8.3 @@ -268,8 +268,8 @@
     8.4        in
     8.5          if exists (Toplevel.is_skipped_proof o #2) res then ()
     8.6          else
     8.7 -          let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
     8.8 -          in if document then Present.theory_output text_pos thy tex_source else () end
     8.9 +          let val body = Thy_Output.present_thy thy res toks;
    8.10 +          in if document then Present.theory_output text_pos thy body else () end
    8.11        end;
    8.12  
    8.13    in (thy, present, size text) end;
     9.1 --- a/src/Pure/Thy/thy_output.ML	Tue Dec 12 18:53:40 2017 +0100
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Dec 13 16:18:40 2017 +0100
     9.3 @@ -24,8 +24,9 @@
     9.4    val boolean: string -> bool
     9.5    val integer: string -> int
     9.6    val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
     9.7 -  val output_text: Toplevel.state -> {markdown: bool, positions: bool} -> Input.source -> string
     9.8 -  val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
     9.9 +  val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
    9.10 +  val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
    9.11 +    Token.T list -> Latex.text list
    9.12    val pretty_text: Proof.context -> string -> Pretty.T
    9.13    val pretty_term: Proof.context -> term -> Pretty.T
    9.14    val pretty_thm: Proof.context -> thm -> Pretty.T
    9.15 @@ -193,7 +194,7 @@
    9.16  
    9.17  (* output text *)
    9.18  
    9.19 -fun output_text state {markdown, positions} source =
    9.20 +fun output_text state {markdown} source =
    9.21    let
    9.22      val is_reported =
    9.23        (case try Toplevel.context_of state of
    9.24 @@ -209,20 +210,19 @@
    9.25        else ();
    9.26  
    9.27      val output_antiquotes =
    9.28 -      map (fn ant =>
    9.29 -        eval_antiquote state ant
    9.30 -        |> positions ? Latex.line_output (#1 (Antiquote.range [ant]))) #> implode;
    9.31 +      map (fn ant => Latex.text (eval_antiquote state ant, #1 (Antiquote.range [ant])));
    9.32  
    9.33      fun output_line line =
    9.34 -      (if Markdown.line_is_item line then "\\item " else "") ^
    9.35 +      (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
    9.36          output_antiquotes (Markdown.line_content line);
    9.37  
    9.38 -    fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
    9.39 -    and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
    9.40 +    fun output_block (Markdown.Par lines) =
    9.41 +          Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines))
    9.42        | output_block (Markdown.List {kind, body, ...}) =
    9.43 -          Latex.environment (Markdown.print_kind kind) (output_blocks body);
    9.44 +          Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
    9.45 +    and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
    9.46    in
    9.47 -    if Toplevel.is_skipped_proof state then ""
    9.48 +    if Toplevel.is_skipped_proof state then []
    9.49      else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
    9.50      then
    9.51        let
    9.52 @@ -262,18 +262,17 @@
    9.53  val blank_token = basic_token Token.is_blank;
    9.54  val newline_token = basic_token Token.is_newline;
    9.55  
    9.56 -fun present_token {positions} state tok =
    9.57 +fun present_token state tok =
    9.58    (case tok of
    9.59 -    No_Token => ""
    9.60 -  | Basic_Token tok => Latex.output_token tok |> positions ? Latex.line_output (Token.pos_of tok)
    9.61 +    No_Token => []
    9.62 +  | Basic_Token tok => [Latex.text (Latex.output_token tok, Token.pos_of tok)]
    9.63    | Markup_Token (cmd, source) =>
    9.64 -      "%\n\\isamarkup" ^ cmd ^ "{" ^
    9.65 -        output_text state {markdown = false, positions = positions} source ^ "%\n}\n"
    9.66 +      Latex.string ("%\n\\isamarkup" ^ cmd ^ "{") ::
    9.67 +        output_text state {markdown = false} source @ [Latex.string "%\n}\n"]
    9.68    | Markup_Env_Token (cmd, source) =>
    9.69 -      Latex.environment ("isamarkup" ^ cmd)
    9.70 -        (output_text state {markdown = true, positions = positions} source)
    9.71 +      [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
    9.72    | Raw_Token source =>
    9.73 -      "%\n" ^ output_text state {markdown = true, positions = positions} source ^ "\n");
    9.74 +      Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]);
    9.75  
    9.76  
    9.77  (* command spans *)
    9.78 @@ -307,7 +306,7 @@
    9.79  
    9.80  fun edge which f (x: string option, y) =
    9.81    if x = y then I
    9.82 -  else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
    9.83 +  else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt)));
    9.84  
    9.85  val begin_tag = edge #2 Latex.begin_tag;
    9.86  val end_tag = edge #1 Latex.end_tag;
    9.87 @@ -316,12 +315,12 @@
    9.88  
    9.89  in
    9.90  
    9.91 -fun present_span positions keywords document_tags span state state'
    9.92 -    (tag_stack, active_tag, newline, buffer, present_cont) =
    9.93 +fun present_span keywords document_tags span state state'
    9.94 +    (tag_stack, active_tag, newline, latex, present_cont) =
    9.95    let
    9.96      val present = fold (fn (tok, (flag, 0)) =>
    9.97 -        Buffer.add (present_token positions state' tok)
    9.98 -        #> Buffer.add flag
    9.99 +        fold cons (present_token state' tok)
   9.100 +        #> cons (Latex.string flag)
   9.101        | _ => I);
   9.102  
   9.103      val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
   9.104 @@ -355,8 +354,8 @@
   9.105            tg :: tgs => (tg, tgs)
   9.106          | [] => err_bad_nesting (Position.here cmd_pos));
   9.107  
   9.108 -    val buffer' =
   9.109 -      buffer
   9.110 +    val latex' =
   9.111 +      latex
   9.112        |> end_tag edge
   9.113        |> close_delim (fst present_cont) edge
   9.114        |> snd present_cont
   9.115 @@ -366,12 +365,12 @@
   9.116      val present_cont' =
   9.117        if newline then (present (#3 srcs), present (#4 srcs))
   9.118        else (I, present (#3 srcs) #> present (#4 srcs));
   9.119 -  in (tag_stack', active_tag', newline', buffer', present_cont') end;
   9.120 +  in (tag_stack', active_tag', newline', latex', present_cont') end;
   9.121  
   9.122 -fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) =
   9.123 +fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
   9.124    if not (null tags) then err_bad_nesting " at end of theory"
   9.125    else
   9.126 -    buffer
   9.127 +    latex
   9.128      |> end_tag (active_tag, NONE)
   9.129      |> close_delim (fst present_cont) (active_tag, NONE)
   9.130      |> snd present_cont;
   9.131 @@ -413,7 +412,6 @@
   9.132  
   9.133  fun present_thy thy command_results toks =
   9.134    let
   9.135 -    val positions = Options.default_bool \<^system_option>\<open>document_positions\<close>;
   9.136      val keywords = Thy_Header.get_keywords thy;
   9.137  
   9.138  
   9.139 @@ -494,15 +492,16 @@
   9.140  
   9.141      fun present_command tr span st st' =
   9.142        Toplevel.setmp_thread_position tr
   9.143 -        (present_span {positions = positions} keywords document_tags span st st');
   9.144 +        (present_span keywords document_tags span st st');
   9.145  
   9.146      fun present _ [] = I
   9.147        | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
   9.148    in
   9.149      if length command_results = length spans then
   9.150 -      ((NONE, []), NONE, true, Buffer.empty, (I, I))
   9.151 +      ((NONE, []), NONE, true, [], (I, I))
   9.152        |> present Toplevel.toplevel (command_results ~~ spans)
   9.153        |> present_trailer
   9.154 +      |> rev
   9.155      else error "Messed-up outer syntax for presentation"
   9.156    end;
   9.157  
   9.158 @@ -675,10 +674,10 @@
   9.159  fun document_command {markdown} (loc, txt) =
   9.160    Toplevel.keep (fn state =>
   9.161      (case loc of
   9.162 -      NONE => ignore (output_text state {markdown = markdown, positions = false} txt)
   9.163 +      NONE => ignore (output_text state {markdown = markdown} txt)
   9.164      | SOME (_, pos) =>
   9.165          error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
   9.166    Toplevel.present_local_theory loc (fn state =>
   9.167 -    ignore (output_text state {markdown = markdown, positions = false} txt));
   9.168 +    ignore (output_text state {markdown = markdown} txt));
   9.169  
   9.170  end;