src/Pure/PIDE/resources.ML
changeset 68092 7c8ed28dd40a
parent 68091 d934bbfeac32
child 69243 d98cfb369cbd
     1.1 --- a/src/Pure/PIDE/resources.ML	Sun May 06 19:10:21 2018 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sun May 06 22:15:52 2018 +0200
     1.3 @@ -36,8 +36,6 @@
     1.4    val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
     1.5    val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T
     1.6    val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T
     1.7 -  val export_message: Markup.export_args -> Output.output list -> unit
     1.8 -  val export: theory -> string -> Output.output -> unit
     1.9  end;
    1.10  
    1.11  structure Resources: RESOURCES =
    1.12 @@ -297,16 +295,4 @@
    1.13  
    1.14  end;
    1.15  
    1.16 -
    1.17 -(* export *)
    1.18 -
    1.19 -val export_message = Output.try_protocol_message o Markup.export;
    1.20 -
    1.21 -fun export thy path output =
    1.22 -  export_message
    1.23 -   {id = Position.get_id (Position.thread_data ()),
    1.24 -    theory_name = Context.theory_long_name thy,
    1.25 -    path = path,
    1.26 -    compress = true} [output];
    1.27 -
    1.28  end;