--- 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 ***
--- 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"
--- 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)) ();
--- 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
--- 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);
--- 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)
--- 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 =
--- 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;
--- 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>\<open>document_positions\<close>;
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;