tuned signature;
authorwenzelm
Sun May 06 19:10:21 2018 +0200 (17 months ago ago)
changeset 68091d934bbfeac32
parent 68090 0763d4eb3ebc
child 68092 7c8ed28dd40a
tuned signature;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/PIDE/markup.ML	Sat May 05 22:33:35 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun May 06 19:10:21 2018 +0200
     1.3 @@ -203,7 +203,8 @@
     1.4    val command_timing: Properties.entry
     1.5    val theory_timing: Properties.entry
     1.6    val exportN: string
     1.7 -  val export: {id: string option, theory_name: string, path: string, compress: bool} -> Properties.T
     1.8 +  type export_args = {id: string option, theory_name: string, path: string, compress: bool}
     1.9 +  val export: export_args -> Properties.T
    1.10    val loading_theory: string -> Properties.T
    1.11    val dest_loading_theory: Properties.T -> string option
    1.12    val build_session_finished: Properties.T
    1.13 @@ -641,7 +642,8 @@
    1.14  val theory_timing = (functionN, "theory_timing");
    1.15  
    1.16  val exportN = "export";
    1.17 -fun export {id, theory_name, path, compress} =
    1.18 +type export_args = {id: string option, theory_name: string, path: string, compress: bool}
    1.19 +fun export ({id, theory_name, path, compress}: export_args) =
    1.20    [(functionN, exportN), ("id", the_default "" id),
    1.21      ("theory_name", theory_name), ("path", path), ("compress", Value.print_bool compress)];
    1.22  
     2.1 --- a/src/Pure/PIDE/resources.ML	Sat May 05 22:33:35 2018 +0200
     2.2 +++ b/src/Pure/PIDE/resources.ML	Sun May 06 19:10:21 2018 +0200
     2.3 @@ -36,7 +36,8 @@
     2.4    val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
     2.5    val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T
     2.6    val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T
     2.7 -  val export: {theory_name: string, path: string, compress: bool} -> Output.output list -> unit
     2.8 +  val export_message: Markup.export_args -> Output.output list -> unit
     2.9 +  val export: theory -> string -> Output.output -> unit
    2.10  end;
    2.11  
    2.12  structure Resources: RESOURCES =
    2.13 @@ -299,12 +300,13 @@
    2.14  
    2.15  (* export *)
    2.16  
    2.17 -fun export {theory_name, path, compress} output =
    2.18 -  let
    2.19 -    val props =
    2.20 -      Markup.export
    2.21 -        {id = Position.get_id (Position.thread_data ()),
    2.22 -          theory_name = theory_name, path = path, compress = compress};
    2.23 -  in Output.try_protocol_message props output end;
    2.24 +val export_message = Output.try_protocol_message o Markup.export;
    2.25 +
    2.26 +fun export thy path output =
    2.27 +  export_message
    2.28 +   {id = Position.get_id (Position.thread_data ()),
    2.29 +    theory_name = Context.theory_long_name thy,
    2.30 +    path = path,
    2.31 +    compress = true} [output];
    2.32  
    2.33  end;