src/Pure/Thy/thy_info.ML

--- a/src/Pure/Thy/thy_info.ML	Mon May 14 22:01:00 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon May 14 22:22:47 2018 +0200
@@ -8,7 +8,8 @@
 signature THY_INFO =
 sig
   type presentation_context =
-    {options: Options.T, pos: Position.T, segments: Thy_Output.segment list}
+    {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
+      segments: Thy_Output.segment list}
   val apply_presentation: presentation_context -> theory -> unit
   val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
   val get_names: unit -> string list
@@ -34,7 +35,8 @@
 (** presentation of consolidated theory **)
 
 type presentation_context =
-  {options: Options.T, pos: Position.T, segments: Thy_Output.segment list};
+  {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
+    segments: Thy_Output.segment list};
 
 structure Presentation = Theory_Data
 (
@@ -50,7 +52,7 @@
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
 val _ =
-  Theory.setup (add_presentation (fn {options, pos, segments} => fn thy =>
+  Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
@@ -61,7 +63,7 @@
         else
           let
             val latex = Latex.isabelle_body (Context.theory_name thy) body;
-            val output = [Latex.output_text latex, Latex.output_positions pos latex];
+            val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
             val _ = Export.export thy "document.tex" output;
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
@@ -320,7 +322,8 @@
       let
         val segments = (spans ~~ maps Toplevel.join_results results)
           |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
-        val context = {options = options, pos = text_pos, segments = segments};
+        val context: presentation_context =
+          {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
       in apply_presentation context thy end;
   in (thy, present, size text) end;