tuned signature;
authorwenzelm
Sun May 06 22:15:52 2018 +0200 (14 months ago)
changeset 680907c8ed28dd40a
parent 68089 d934bbfeac32
child 68091 0c7820590236
tuned signature;
clarified modules;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/resources.ML
src/Pure/ROOT.ML
src/Pure/Thy/export.ML
     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  
     2.1 --- a/src/Pure/PIDE/markup.scala	Sun May 06 19:10:21 2018 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sun May 06 22:15:52 2018 +0200
     2.3 @@ -571,25 +571,24 @@
     2.4    val EXPORT = "export"
     2.5    object Export
     2.6    {
     2.7 -    sealed case class Args(id: Option[String], theory_name: String, path: String, compress: Boolean)
     2.8 +    sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean)
     2.9  
    2.10      val THEORY_NAME = "theory_name"
    2.11 -    val PATH = "path"
    2.12      val COMPRESS = "compress"
    2.13  
    2.14      def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
    2.15        props match {
    2.16          case
    2.17 -          List((THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress)),
    2.18 -            (EXPORT, hex)) => Some((Args(None, theory_name, path, compress), Bytes.hex(hex)))
    2.19 +          List((THEORY_NAME, theory_name), (NAME, name), (COMPRESS, Value.Boolean(compress)),
    2.20 +            (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex)))
    2.21          case _ => None
    2.22        }
    2.23  
    2.24      def unapply(props: Properties.T): Option[Args] =
    2.25        props match {
    2.26          case List((FUNCTION, EXPORT), (ID, id),
    2.27 -          (THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress))) =>
    2.28 -            Some(Args(proper_string(id), theory_name, path, compress))
    2.29 +          (THEORY_NAME, theory_name), (PATH, name), (COMPRESS, Value.Boolean(compress))) =>
    2.30 +            Some(Args(proper_string(id), theory_name, name, compress))
    2.31          case _ => None
    2.32        }
    2.33    }
     3.1 --- a/src/Pure/PIDE/resources.ML	Sun May 06 19:10:21 2018 +0200
     3.2 +++ b/src/Pure/PIDE/resources.ML	Sun May 06 22:15:52 2018 +0200
     3.3 @@ -36,8 +36,6 @@
     3.4    val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
     3.5    val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T
     3.6    val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T
     3.7 -  val export_message: Markup.export_args -> Output.output list -> unit
     3.8 -  val export: theory -> string -> Output.output -> unit
     3.9  end;
    3.10  
    3.11  structure Resources: RESOURCES =
    3.12 @@ -297,16 +295,4 @@
    3.13  
    3.14  end;
    3.15  
    3.16 -
    3.17 -(* export *)
    3.18 -
    3.19 -val export_message = Output.try_protocol_message o Markup.export;
    3.20 -
    3.21 -fun export thy path output =
    3.22 -  export_message
    3.23 -   {id = Position.get_id (Position.thread_data ()),
    3.24 -    theory_name = Context.theory_long_name thy,
    3.25 -    path = path,
    3.26 -    compress = true} [output];
    3.27 -
    3.28  end;
     4.1 --- a/src/Pure/ROOT.ML	Sun May 06 19:10:21 2018 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Sun May 06 22:15:52 2018 +0200
     4.3 @@ -300,6 +300,7 @@
     4.4  ML_file "PIDE/command.ML";
     4.5  ML_file "PIDE/query_operation.ML";
     4.6  ML_file "PIDE/resources.ML";
     4.7 +ML_file "Thy/export.ML";
     4.8  ML_file "Thy/present.ML";
     4.9  ML_file "Thy/thy_info.ML";
    4.10  ML_file "Thy/sessions.ML";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/Thy/export.ML	Sun May 06 22:15:52 2018 +0200
     5.3 @@ -0,0 +1,26 @@
     5.4 +(*  Title:      Pure/Thy/export.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Manage theory exports.
     5.8 +*)
     5.9 +
    5.10 +signature EXPORT =
    5.11 +sig
    5.12 +  val export: theory -> string -> Output.output -> unit
    5.13 +  val export_uncompressed: theory -> string -> Output.output -> unit
    5.14 +end;
    5.15 +
    5.16 +structure Export: EXPORT =
    5.17 +struct
    5.18 +
    5.19 +fun gen_export compress thy name output =
    5.20 +  (Output.try_protocol_message o Markup.export)
    5.21 +   {id = Position.get_id (Position.thread_data ()),
    5.22 +    theory_name = Context.theory_long_name thy,
    5.23 +    name = name,
    5.24 +    compress = compress} [output];
    5.25 +
    5.26 +val export = gen_export true;
    5.27 +val export_uncompressed = gen_export false;
    5.28 +
    5.29 +end;