more scalable -- avoid huge lines within stdout;
authorwenzelm
Fri May 11 19:57:49 2018 +0200 (12 months ago)
changeset 68148fb661e4c4717
parent 68147 a8f40dd73c61
child 68149 9a4a6adb95b5
more scalable -- avoid huge lines within stdout;
src/Pure/PIDE/markup.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri May 11 19:27:00 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri May 11 19:57:49 2018 +0200
     1.3 @@ -577,7 +577,7 @@
     1.4      val THEORY_NAME = "theory_name"
     1.5      val COMPRESS = "compress"
     1.6  
     1.7 -    def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
     1.8 +    def dest_inline(props: Properties.T): Option[(Args, Path)] =
     1.9        props match {
    1.10          case
    1.11            List(
    1.12 @@ -585,8 +585,8 @@
    1.13              (THEORY_NAME, theory_name),
    1.14              (NAME, name),
    1.15              (COMPRESS, Value.Boolean(compress)),
    1.16 -            (EXPORT, hex)) =>
    1.17 -          Some((Args(None, serial, theory_name, name, compress), Bytes.hex(hex)))
    1.18 +            (FILE, file)) if isabelle.Path.is_valid(file) =>
    1.19 +          Some((Args(None, serial, theory_name, name, compress), isabelle.Path.explode(file)))
    1.20          case _ => None
    1.21        }
    1.22  
     2.1 --- a/src/Pure/Tools/build.ML	Fri May 11 19:27:00 2018 +0200
     2.2 +++ b/src/Pure/Tools/build.ML	Fri May 11 19:57:49 2018 +0200
     2.3 @@ -97,7 +97,11 @@
     2.4        else if function = (Markup.functionN, Markup.exportN) andalso
     2.5          not (null args) andalso #1 (hd args) = Markup.idN
     2.6        then
     2.7 -        inline_message (#2 function) (tl args @ [(Markup.exportN, hex_string (implode output))])
     2.8 +        let
     2.9 +          val path = Isabelle_System.create_tmp_path "export" "";
    2.10 +          val _ = File.open_output (fn out => List.app (File.output out) output) path;
    2.11 +          val file_name = Path.implode (Path.expand path);
    2.12 +        in inline_message (#2 function) (tl args @ [(Markup.fileN, file_name)]) end
    2.13        else
    2.14          (case Markup.dest_loading_theory props of
    2.15            SOME name => writeln ("\floading_theory = " ^ name)
     3.1 --- a/src/Pure/Tools/build.scala	Fri May 11 19:27:00 2018 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Fri May 11 19:57:49 2018 +0200
     3.3 @@ -286,9 +286,13 @@
     3.4                  case None =>
     3.5                    for {
     3.6                      text <- Library.try_unprefix("\fexport = ", line)
     3.7 -                    (args, body) <-
     3.8 +                    (args, path) <-
     3.9                        Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
    3.10 -                  } { export_consumer(name, args, body) }
    3.11 +                  } {
    3.12 +                    val body = Bytes.read(path)
    3.13 +                    path.file.delete
    3.14 +                    export_consumer(name, args, body)
    3.15 +                  }
    3.16                },
    3.17              progress_limit =
    3.18                options.int("process_output_limit") match {