protocol message for export of theory resources;
authorwenzelm
Sat May 05 22:33:35 2018 +0200 (12 months ago)
changeset 680880763d4eb3ebc
parent 68087 dac267cd51fe
child 68089 d934bbfeac32
protocol message for export of theory resources;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/resources.ML
src/Pure/PIDE/session.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Sat May 05 21:44:18 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sat May 05 22:33:35 2018 +0200
     1.3 @@ -202,6 +202,8 @@
     1.4    val task_statistics: Properties.entry
     1.5    val command_timing: Properties.entry
     1.6    val theory_timing: Properties.entry
     1.7 +  val exportN: string
     1.8 +  val export: {id: string option, theory_name: string, path: string, compress: bool} -> Properties.T
     1.9    val loading_theory: string -> Properties.T
    1.10    val dest_loading_theory: Properties.T -> string option
    1.11    val build_session_finished: Properties.T
    1.12 @@ -638,6 +640,11 @@
    1.13  
    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 +  [(functionN, exportN), ("id", the_default "" id),
    1.19 +    ("theory_name", theory_name), ("path", path), ("compress", Value.print_bool compress)];
    1.20 +
    1.21  fun loading_theory name = [("function", "loading_theory"), ("name", name)];
    1.22  
    1.23  fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
     2.1 --- a/src/Pure/PIDE/markup.scala	Sat May 05 21:44:18 2018 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sat May 05 22:33:35 2018 +0200
     2.3 @@ -568,6 +568,32 @@
     2.4        }
     2.5    }
     2.6  
     2.7 +  val EXPORT = "export"
     2.8 +  object Export
     2.9 +  {
    2.10 +    sealed case class Args(id: Option[String], theory_name: String, path: String, compress: Boolean)
    2.11 +
    2.12 +    val THEORY_NAME = "theory_name"
    2.13 +    val PATH = "path"
    2.14 +    val COMPRESS = "compress"
    2.15 +
    2.16 +    def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
    2.17 +      props match {
    2.18 +        case
    2.19 +          List((THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress)),
    2.20 +            (EXPORT, hex)) => Some((Args(None, theory_name, path, 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 +        case _ => None
    2.30 +      }
    2.31 +  }
    2.32 +
    2.33    val BUILD_SESSION_FINISHED = "build_session_finished"
    2.34    val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
    2.35  
     3.1 --- a/src/Pure/PIDE/resources.ML	Sat May 05 21:44:18 2018 +0200
     3.2 +++ b/src/Pure/PIDE/resources.ML	Sat May 05 22:33:35 2018 +0200
     3.3 @@ -36,6 +36,7 @@
     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: {theory_name: string, path: string, compress: bool} -> Output.output list -> unit
     3.8  end;
     3.9  
    3.10  structure Resources: RESOURCES =
    3.11 @@ -295,4 +296,15 @@
    3.12  
    3.13  end;
    3.14  
    3.15 +
    3.16 +(* export *)
    3.17 +
    3.18 +fun export {theory_name, path, compress} output =
    3.19 +  let
    3.20 +    val props =
    3.21 +      Markup.export
    3.22 +        {id = Position.get_id (Position.thread_data ()),
    3.23 +          theory_name = theory_name, path = path, compress = compress};
    3.24 +  in Output.try_protocol_message props output end;
    3.25 +
    3.26  end;
     4.1 --- a/src/Pure/PIDE/session.scala	Sat May 05 21:44:18 2018 +0200
     4.2 +++ b/src/Pure/PIDE/session.scala	Sat May 05 22:33:35 2018 +0200
     4.3 @@ -435,6 +435,9 @@
     4.4                case Protocol.Theory_Timing(_, _) =>
     4.5                  // FIXME
     4.6  
     4.7 +              case Markup.Export(_) =>
     4.8 +                // FIXME
     4.9 +
    4.10                case Markup.Assign_Update =>
    4.11                  msg.text match {
    4.12                    case Protocol.Assign_Update(id, update) =>
     5.1 --- a/src/Pure/Tools/build.ML	Sat May 05 21:44:18 2018 +0200
     5.2 +++ b/src/Pure/Tools/build.ML	Sat May 05 22:33:35 2018 +0200
     5.3 @@ -94,6 +94,10 @@
     5.4          end
     5.5        else if function = Markup.theory_timing then
     5.6          inline_message (#2 function) args
     5.7 +      else if function = (Markup.functionN, Markup.exportN) andalso
     5.8 +        not (null args) andalso #1 (hd args) = Markup.idN
     5.9 +      then
    5.10 +        inline_message (#2 function) (tl args @ [(Markup.exportN, hex_string (implode output))])
    5.11        else
    5.12          (case Markup.dest_loading_theory props of
    5.13            SOME name => writeln ("\floading_theory = " ^ name)
     6.1 --- a/src/Pure/Tools/build.scala	Sat May 05 21:44:18 2018 +0200
     6.2 +++ b/src/Pure/Tools/build.scala	Sat May 05 22:33:35 2018 +0200
     6.3 @@ -282,6 +282,11 @@
     6.4                Library.try_unprefix("\floading_theory = ", line) match {
     6.5                  case Some(theory) => progress.theory(name, theory)
     6.6                  case None =>
     6.7 +                  for {
     6.8 +                    text <- Library.try_unprefix("\fexport = ", line)
     6.9 +                    (args, body) <-
    6.10 +                      Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
    6.11 +                  } { } // FIXME
    6.12                },
    6.13              progress_limit =
    6.14                options.int("process_output_limit") match {