src/Pure/PIDE/markup.ML
changeset 68090 7c8ed28dd40a
parent 68089 d934bbfeac32
child 68101 0699a0bacc50
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun May 06 19:10:21 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun May 06 22:15:52 2018 +0200
     1.3 @@ -203,7 +203,7 @@
     1.4    val command_timing: Properties.entry
     1.5    val theory_timing: Properties.entry
     1.6    val exportN: string
     1.7 -  type export_args = {id: string option, theory_name: string, path: string, compress: bool}
     1.8 +  type export_args = {id: string option, theory_name: string, name: 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 @@ -642,10 +642,10 @@
    1.13  val theory_timing = (functionN, "theory_timing");
    1.14  
    1.15  val exportN = "export";
    1.16 -type export_args = {id: string option, theory_name: string, path: string, compress: bool}
    1.17 -fun export ({id, theory_name, path, compress}: export_args) =
    1.18 -  [(functionN, exportN), ("id", the_default "" id),
    1.19 -    ("theory_name", theory_name), ("path", path), ("compress", Value.print_bool compress)];
    1.20 +type export_args = {id: string option, theory_name: string, name: string, compress: bool}
    1.21 +fun export ({id, theory_name, name, compress}: export_args) =
    1.22 +  [(functionN, exportN), (idN, the_default "" id),
    1.23 +    ("theory_name", theory_name), (nameN, name), ("compress", Value.print_bool compress)];
    1.24  
    1.25  fun loading_theory name = [("function", "loading_theory"), ("name", name)];
    1.26