# HG changeset patch
# User wenzelm
# Date 1513097182 -3600
# Node ID 9ab34bb83a840ce3d58bd2790a37684ac149bdd2
# Parent  58ab7ddbdb04b7d72a055266613ef9358dfaeec1
option document_positions;

diff -r 58ab7ddbdb04 -r 9ab34bb83a84 NEWS
--- a/NEWS	Tue Dec 12 17:47:23 2017 +0100
+++ b/NEWS	Tue Dec 12 17:46:22 2017 +0100
@@ -87,8 +87,12 @@
 more accurately: only terminal proof steps ('by' etc.) are skipped.
 
 * Command-line tool "isabelle document" has been re-implemented in
-Isabelle/Scala, with simplified arguments and explicit errors from the
-latex process. Minor INCOMPATIBILITY.
+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.
 
 
 *** HOL ***
diff -r 58ab7ddbdb04 -r 9ab34bb83a84 etc/options
--- a/etc/options	Tue Dec 12 17:47:23 2017 +0100
+++ b/etc/options	Tue Dec 12 17:46:22 2017 +0100
@@ -13,6 +13,8 @@
   -- "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 58ab7ddbdb04 -r 9ab34bb83a84 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Dec 12 17:47:23 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Dec 12 17:46:22 2017 +0100
@@ -262,18 +262,18 @@
 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
 
-fun present_token state tok =
+fun present_token {positions} state tok =
   (case tok of
     No_Token => ""
-  | Basic_Token tok => Latex.output_token tok |> Latex.line_output (Token.pos_of tok)
+  | Basic_Token tok => Latex.output_token tok |> positions ? Latex.line_output (Token.pos_of tok)
   | Markup_Token (cmd, source) =>
       "%\n\\isamarkup" ^ cmd ^ "{" ^
-        output_text state {markdown = false, positions = true} source ^ "%\n}\n"
+        output_text state {markdown = false, positions = positions} source ^ "%\n}\n"
   | Markup_Env_Token (cmd, source) =>
       Latex.environment ("isamarkup" ^ cmd)
-        (output_text state {markdown = true, positions = true} source)
+        (output_text state {markdown = true, positions = positions} source)
   | Raw_Token source =>
-      "%\n" ^ output_text state {markdown = true, positions = true} source ^ "\n");
+      "%\n" ^ output_text state {markdown = true, positions = positions} source ^ "\n");
 
 
 (* command spans *)
@@ -316,11 +316,11 @@
 
 in
 
-fun present_span keywords document_tags span state state'
+fun present_span positions keywords document_tags span state state'
     (tag_stack, active_tag, newline, buffer, present_cont) =
   let
     val present = fold (fn (tok, (flag, 0)) =>
-        Buffer.add (present_token state' tok)
+        Buffer.add (present_token positions state' tok)
         #> Buffer.add flag
       | _ => I);
 
@@ -413,6 +413,7 @@
 
 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;
 
 
@@ -492,7 +493,8 @@
     val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>);
 
     fun present_command tr span st st' =
-      Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
+      Toplevel.setmp_thread_position tr
+        (present_span {positions = positions} keywords document_tags span st st');
 
     fun present _ [] = I
       | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;