# HG changeset patch
# User wenzelm
# Date 1526061469 -7200
# Node ID fb661e4c471793cb7933e48a4f4f9fb4bd09adfc
# Parent  a8f40dd73c6114230453ddcb5f0a3e3131cdd2af
more scalable -- avoid huge lines within stdout;

diff -r a8f40dd73c61 -r fb661e4c4717 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri May 11 19:27:00 2018 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri May 11 19:57:49 2018 +0200
@@ -577,7 +577,7 @@
     val THEORY_NAME = "theory_name"
     val COMPRESS = "compress"
 
-    def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
+    def dest_inline(props: Properties.T): Option[(Args, Path)] =
       props match {
         case
           List(
@@ -585,8 +585,8 @@
             (THEORY_NAME, theory_name),
             (NAME, name),
             (COMPRESS, Value.Boolean(compress)),
-            (EXPORT, hex)) =>
-          Some((Args(None, serial, theory_name, name, compress), Bytes.hex(hex)))
+            (FILE, file)) if isabelle.Path.is_valid(file) =>
+          Some((Args(None, serial, theory_name, name, compress), isabelle.Path.explode(file)))
         case _ => None
       }
 
diff -r a8f40dd73c61 -r fb661e4c4717 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri May 11 19:27:00 2018 +0200
+++ b/src/Pure/Tools/build.ML	Fri May 11 19:57:49 2018 +0200
@@ -97,7 +97,11 @@
       else if function = (Markup.functionN, Markup.exportN) andalso
         not (null args) andalso #1 (hd args) = Markup.idN
       then
-        inline_message (#2 function) (tl args @ [(Markup.exportN, hex_string (implode output))])
+        let
+          val path = Isabelle_System.create_tmp_path "export" "";
+          val _ = File.open_output (fn out => List.app (File.output out) output) path;
+          val file_name = Path.implode (Path.expand path);
+        in inline_message (#2 function) (tl args @ [(Markup.fileN, file_name)]) end
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)
diff -r a8f40dd73c61 -r fb661e4c4717 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri May 11 19:27:00 2018 +0200
+++ b/src/Pure/Tools/build.scala	Fri May 11 19:57:49 2018 +0200
@@ -286,9 +286,13 @@
                 case None =>
                   for {
                     text <- Library.try_unprefix("\fexport = ", line)
-                    (args, body) <-
+                    (args, path) <-
                       Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
-                  } { export_consumer(name, args, body) }
+                  } {
+                    val body = Bytes.read(path)
+                    path.file.delete
+                    export_consumer(name, args, body)
+                  }
               },
             progress_limit =
               options.int("process_output_limit") match {