src/Pure/Thy/thy_info.ML
changeset 68184 6c693b2700b3
parent 68182 fa3cf61121ee
child 68491 f0f83ce0badd
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 14 22:01:00 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 14 22:22:47 2018 +0200
     1.3 @@ -8,7 +8,8 @@
     1.4  signature THY_INFO =
     1.5  sig
     1.6    type presentation_context =
     1.7 -    {options: Options.T, pos: Position.T, segments: Thy_Output.segment list}
     1.8 +    {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
     1.9 +      segments: Thy_Output.segment list}
    1.10    val apply_presentation: presentation_context -> theory -> unit
    1.11    val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
    1.12    val get_names: unit -> string list
    1.13 @@ -34,7 +35,8 @@
    1.14  (** presentation of consolidated theory **)
    1.15  
    1.16  type presentation_context =
    1.17 -  {options: Options.T, pos: Position.T, segments: Thy_Output.segment list};
    1.18 +  {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
    1.19 +    segments: Thy_Output.segment list};
    1.20  
    1.21  structure Presentation = Theory_Data
    1.22  (
    1.23 @@ -50,7 +52,7 @@
    1.24  fun add_presentation f = Presentation.map (cons (f, stamp ()));
    1.25  
    1.26  val _ =
    1.27 -  Theory.setup (add_presentation (fn {options, pos, segments} => fn thy =>
    1.28 +  Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
    1.29      if exists (Toplevel.is_skipped_proof o #state) segments then ()
    1.30      else
    1.31        let
    1.32 @@ -61,7 +63,7 @@
    1.33          else
    1.34            let
    1.35              val latex = Latex.isabelle_body (Context.theory_name thy) body;
    1.36 -            val output = [Latex.output_text latex, Latex.output_positions pos latex];
    1.37 +            val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
    1.38              val _ = Export.export thy "document.tex" output;
    1.39              val _ = if #enabled option then Present.theory_output thy output else ();
    1.40            in () end
    1.41 @@ -320,7 +322,8 @@
    1.42        let
    1.43          val segments = (spans ~~ maps Toplevel.join_results results)
    1.44            |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
    1.45 -        val context = {options = options, pos = text_pos, segments = segments};
    1.46 +        val context: presentation_context =
    1.47 +          {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
    1.48        in apply_presentation context thy end;
    1.49    in (thy, present, size text) end;
    1.50