--- a/src/Pure/Thy/export.ML Sun Mar 29 19:47:42 2020 +0200
+++ b/src/Pure/Thy/export.ML Sun Mar 29 21:32:20 2020 +0200
@@ -83,10 +83,7 @@
let
val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
val _ = YXML.write_body path body;
- in
- Protocol_Message.inline_properties (#2 function)
- (tl args @ [(Markup.fileN, Path.implode path)])
- end
+ in Protocol_Message.marker (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
else raise Output.Protocol_Message props
| [] => raise Output.Protocol_Message props);