src/Pure/PIDE/resources.ML
changeset 68090 0763d4eb3ebc
parent 67493 c4e9e0c50487
child 68091 d934bbfeac32
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat May 05 21:44:18 2018 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat May 05 22:33:35 2018 +0200
     1.3 @@ -36,6 +36,7 @@
     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: {theory_name: string, path: string, compress: bool} -> Output.output list -> unit
     1.8  end;
     1.9  
    1.10  structure Resources: RESOURCES =
    1.11 @@ -295,4 +296,15 @@
    1.12  
    1.13  end;
    1.14  
    1.15 +
    1.16 +(* export *)
    1.17 +
    1.18 +fun export {theory_name, path, compress} output =
    1.19 +  let
    1.20 +    val props =
    1.21 +      Markup.export
    1.22 +        {id = Position.get_id (Position.thread_data ()),
    1.23 +          theory_name = theory_name, path = path, compress = compress};
    1.24 +  in Output.try_protocol_message props output end;
    1.25 +
    1.26  end;