# HG changeset patch # User wenzelm # Date 1513178320 -3600 # Node ID 1c0a6a95711401f35a4e9657196fbecf1d50dc29 # Parent 4ade0d38742989af05c7f6a5a5a1d1f13fc3487b positions as postlude: avoid intrusion of odd %-forms into main tex source; diff -r 4ade0d387429 -r 1c0a6a957114 NEWS --- a/NEWS Tue Dec 12 18:53:40 2017 +0100 +++ b/NEWS Wed Dec 13 16:18:40 2017 +0100 @@ -87,12 +87,8 @@ 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. Minor INCOMPATIBILITY. - -* Original source positions are inlined into generated tex files: this -improves error messages by "isabelle document", but may sometimes -confuse LaTeX. Rare INCOMPATIBILITY, set option -"document_positions=false" to avoid this. +Isabelle/Scala, with simplified arguments and explicit errors from the +latex process. Minor INCOMPATIBILITY. *** HOL *** diff -r 4ade0d387429 -r 1c0a6a957114 etc/options --- a/etc/options Tue Dec 12 18:53:40 2017 +0100 +++ b/etc/options Wed Dec 13 16:18:40 2017 +0100 @@ -13,8 +13,6 @@ -- "alternative document variants (separated by colons)" option document_tags : string = "" -- "default command tags (separated by commas)" -option document_positions : bool = true - -- "inline original source positions into generated tex files" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" diff -r 4ade0d387429 -r 1c0a6a957114 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Tue Dec 12 18:53:40 2017 +0100 +++ b/src/Pure/PIDE/command.ML Wed Dec 13 16:18:40 2017 +0100 @@ -199,7 +199,7 @@ Toplevel.setmp_thread_position tr (fn () => Outer_Syntax.side_comments span |> maps (fn cmt => - (Thy_Output.output_text st' {markdown = false, positions = false} (Token.input_of cmt); []) + (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); []) handle exn => if Exn.is_interrupt exn then Exn.reraise exn else Runtime.exn_messages exn)) (); diff -r 4ade0d387429 -r 1c0a6a957114 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Tue Dec 12 18:53:40 2017 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Wed Dec 13 16:18:40 2017 +0100 @@ -45,7 +45,7 @@ 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, positions = false}); + enclose s1 s2 o Latex.output_text o Thy_Output.output_text state {markdown = false}); in diff -r 4ade0d387429 -r 1c0a6a957114 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Tue Dec 12 18:53:40 2017 +0100 +++ b/src/Pure/Thy/latex.ML Wed Dec 13 16:18:40 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 @@ -15,14 +22,14 @@ Symbol.symbol list -> string val output_symbols: Symbol.symbol list -> string val output_syms: string -> string - val line_output: Position.T -> string -> string val output_token: Token.T -> string val begin_delim: string -> string 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 isabelle_theory: Position.T -> 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,46 @@ 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 output (Text (s, pos)) (positions, line) = + let + val positions' = + (case Position.line_of pos of + NONE => positions + | SOME l => position (apply2 Value.print_int (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 = @@ -170,30 +217,6 @@ end; -(* positions *) - -fun output_prop (a, b) = enclose "%:%" "%:%\n" (a ^ "=" ^ b); - -fun output_file pos = - (case Position.file_of pos of - NONE => "" - | SOME file => output_prop (Markup.fileN, file)); - - -val is_blank_line = forall_string (fn s => s = " " orelse s = "\t"); - -fun line_output pos output = - (case Position.line_of pos of - NONE => output - | SOME n => - (case take_prefix is_blank_line (split_lines output) of - (_, []) => output - | (blank, rest) => - cat_lines blank ^ " %\n" ^ - output_prop (Markup.lineN, Value.print_int n) ^ - cat_lines rest)); - - (* output token *) fun output_token tok = @@ -231,17 +254,22 @@ (* 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 ^ "}"); -fun isabelle_theory pos name txt = - output_file pos ^ - "\\begin{isabellebody}%\n\ - \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ - "%\n\\end{isabellebody}%\n"; +fun environment_block name = environment_delim name |-> enclose_body #> block; +fun environment name = environment_delim name |-> enclose; + +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 Position.none name + isabelle_body_delim name + |-> enclose ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^ output_known_symbols known syms); diff -r 4ade0d387429 -r 1c0a6a957114 src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Tue Dec 12 18:53:40 2017 +0100 +++ b/src/Pure/Thy/latex.scala Wed Dec 13 16:18:40 2017 +0100 @@ -30,40 +30,46 @@ /* generated .tex file */ private val File_Pattern = """^%:%file=(.+)%:%$""".r - private val Line_Pattern = """^*%:%line=(\d+)%:%$""".r + private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r def read_tex_file(tex_file: Path): Tex_File = - new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray) + { + 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 + } - final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String]) + 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 - val source_file: Option[String] = - if (tex_lines.nonEmpty) { - tex_lines(0) match { - case File_Pattern(file) => Some(file) - case _ => None - } + 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)) } - else None - - private def prev_lines_iterator(l: Int): Iterator[String] = - if (0 < l && l <= tex_lines.length) - Range.inclusive(l - 1, 0, -1).iterator.map(tex_lines(_)) - else Iterator.empty - - def source_position(l: Int): Option[Position.T] = - (for { - file <- source_file.iterator - s <- prev_lines_iterator(l) - line <- - (s match { - case Line_Pattern(Value.Int(line)) => Some(line) - case _ => None - }) - } - yield { Position.Line_File(line, file) }).toStream.headOption def position(line: Int): Position.T = source_position(line) getOrElse Position.Line_File(line, tex_file.implode) diff -r 4ade0d387429 -r 1c0a6a957114 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Tue Dec 12 18:53:40 2017 +0100 +++ b/src/Pure/Thy/present.ML Wed Dec 13 16:18:40 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: Position.T -> 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; @@ -278,11 +278,15 @@ (* theory elements *) -fun theory_output pos 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 pos 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 = diff -r 4ade0d387429 -r 1c0a6a957114 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Dec 12 18:53:40 2017 +0100 +++ b/src/Pure/Thy/thy_info.ML Wed Dec 13 16:18:40 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 text_pos 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 4ade0d387429 -r 1c0a6a957114 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Dec 12 18:53:40 2017 +0100 +++ b/src/Pure/Thy/thy_output.ML Wed Dec 13 16:18:40 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, positions: 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 @@ -193,7 +194,7 @@ (* output text *) -fun output_text state {markdown, positions} source = +fun output_text state {markdown} source = let val is_reported = (case try Toplevel.context_of state of @@ -209,20 +210,19 @@ else (); val output_antiquotes = - map (fn ant => - eval_antiquote state ant - |> positions ? Latex.line_output (#1 (Antiquote.range [ant]))) #> implode; + 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 @@ -262,18 +262,17 @@ val blank_token = basic_token Token.is_blank; val newline_token = basic_token Token.is_newline; -fun present_token {positions} state tok = +fun present_token state tok = (case tok of - No_Token => "" - | Basic_Token tok => Latex.output_token tok |> positions ? Latex.line_output (Token.pos_of 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, positions = positions} 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, positions = positions} source) + [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)] | Raw_Token source => - "%\n" ^ output_text state {markdown = true, positions = positions} source ^ "\n"); + Latex.string "%\n" :: output_text state {markdown = true} source @ [Latex.string "\n"]); (* command spans *) @@ -307,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; @@ -316,12 +315,12 @@ in -fun present_span positions keywords document_tags span state state' - (tag_stack, active_tag, newline, buffer, present_cont) = +fun present_span keywords document_tags span state state' + (tag_stack, active_tag, newline, latex, present_cont) = let val present = fold (fn (tok, (flag, 0)) => - Buffer.add (present_token positions 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; @@ -355,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 @@ -366,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; @@ -413,7 +412,6 @@ fun present_thy thy command_results toks = let - val positions = Options.default_bool \<^system_option>\document_positions\; val keywords = Thy_Header.get_keywords thy; @@ -494,15 +492,16 @@ fun present_command tr span st st' = Toplevel.setmp_thread_position tr - (present_span {positions = positions} keywords document_tags span st st'); + (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; @@ -675,10 +674,10 @@ fun document_command {markdown} (loc, txt) = Toplevel.keep (fn state => (case loc of - NONE => ignore (output_text state {markdown = markdown, positions = false} 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 = markdown, positions = false} txt)); + ignore (output_text state {markdown = markdown} txt)); end;