src/Pure/Thy/thy_load.ML
changeset 54458 96ccc8972fc7
parent 54456 f4b1440d9880
child 54519 5fed81762406
     1.1 --- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 21:29:18 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 22:17:45 2013 +0100
     1.3 @@ -20,8 +20,8 @@
     1.4    val loaded_files: theory -> Path.T list
     1.5    val loaded_files_current: theory -> bool
     1.6    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     1.7 -  val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
     1.8 -    Position.T -> string -> theory list -> theory * (unit -> unit) * int
     1.9 +  val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
    1.10 +    Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
    1.11  end;
    1.12  
    1.13  structure Thy_Load: THY_LOAD =
    1.14 @@ -162,7 +162,7 @@
    1.15      val thy = Toplevel.end_theory end_pos end_state;
    1.16    in (results, thy) end;
    1.17  
    1.18 -fun load_thy last_timing update_time master_dir header text_pos text parents =
    1.19 +fun load_thy document last_timing update_time master_dir header text_pos text parents =
    1.20    let
    1.21      val time = ! Toplevel.timing;
    1.22  
    1.23 @@ -191,10 +191,11 @@
    1.24          if exists (Toplevel.is_skipped_proof o #2) res then
    1.25            warning ("Cannot present theory with skipped proofs: " ^ quote name)
    1.26          else
    1.27 -          Thy_Output.present_thy minor Keyword.command_tags
    1.28 -            (Outer_Syntax.is_markup outer_syntax) res toks
    1.29 -          |> Buffer.content
    1.30 -          |> Present.theory_output name
    1.31 +          let val tex_source =
    1.32 +            Thy_Output.present_thy minor Keyword.command_tags
    1.33 +              (Outer_Syntax.is_markup outer_syntax) res toks
    1.34 +            |> Buffer.content;
    1.35 +          in if document then Present.theory_output name tex_source else () end
    1.36        end;
    1.37  
    1.38    in (thy, present, size text) end;