--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Nov 02 14:31:48 2019 +0000
@@ -973,8 +973,8 @@
val prv_path = Path.ext "prv" path;
val _ =
Export.export thy (Path.binding (prv_path, Position.none))
- [implode (map (fn (s, _) => snd (strip_number s) ^
- " -- proved by " ^ Distribution.version ^ "\n") proved'')];
+ (proved'' |> map (fn (s, _) =>
+ XML.Text (snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n")));
in {pfuns = pfuns, type_map = type_map, env = NONE} end))
|> Sign.parent_path;
--- a/src/Pure/General/buffer.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/General/buffer.ML Sat Nov 02 14:31:48 2019 +0000
@@ -9,48 +9,28 @@
type T
val empty: T
val is_empty: T -> bool
- val chunks: T -> string list
val content: T -> string
val add: string -> T -> T
+ val output: T -> (string -> unit) -> unit
val markup: Markup.T -> (T -> T) -> T -> T
- val output: T -> BinIO.outstream -> unit
end;
structure Buffer: BUFFER =
struct
-abstype T = Buffer of {chunk_size: int, chunk: string list, buffer: string list}
+abstype T = Buffer of string list
with
-val empty = Buffer {chunk_size = 0, chunk = [], buffer = []};
-
-fun is_empty (Buffer {chunk, buffer, ...}) = null chunk andalso null buffer;
-
-local
- val chunk_limit = 4096;
+val empty = Buffer [];
- fun add_chunk [] buffer = buffer
- | add_chunk chunk buffer = implode (rev chunk) :: buffer;
-in
-
-fun chunks (Buffer {chunk, buffer, ...}) = rev (add_chunk chunk buffer);
-
-val content = implode o chunks;
+fun is_empty (Buffer xs) = null xs;
-fun add x (buf as Buffer {chunk_size, chunk, buffer}) =
- let val n = size x in
- if n = 0 then buf
- else if n + chunk_size < chunk_limit then
- Buffer {chunk_size = n + chunk_size, chunk = x :: chunk, buffer = buffer}
- else
- Buffer {chunk_size = 0, chunk = [],
- buffer =
- if n < chunk_limit
- then add_chunk (x :: chunk) buffer
- else x :: add_chunk chunk buffer}
- end;
+fun add "" buf = buf
+ | add x (Buffer xs) = Buffer (x :: xs);
-end;
+fun content (Buffer xs) = implode (rev xs);
+
+fun output (Buffer xs) out = List.app out (rev xs);
end;
@@ -58,7 +38,4 @@
let val (bg, en) = Markup.output m
in add bg #> body #> add en end;
-fun output buf stream =
- List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (chunks buf);
-
end;
--- a/src/Pure/General/file.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/General/file.ML Sat Nov 02 14:31:48 2019 +0000
@@ -165,7 +165,7 @@
fun append path txt = append_list path [txt];
fun generate path txt = if try read path = SOME txt then () else write path txt;
-fun write_buffer path buf = open_output (Buffer.output buf) path;
+fun write_buffer path buf = open_output (Buffer.output buf o output) path;
(* eq *)
--- a/src/Pure/General/output.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/General/output.ML Sat Nov 02 14:31:48 2019 +0000
@@ -28,8 +28,9 @@
val physical_stdout: output -> unit
val physical_stderr: output -> unit
val physical_writeln: output -> unit
+ type protocol_message_fn = Output_Primitives.protocol_message_fn
exception Protocol_Message of Properties.T
- val protocol_message_undefined: Properties.T -> string list -> unit
+ val protocol_message_undefined: protocol_message_fn
val writelns: string list -> unit
val state: string -> unit
val information: string -> unit
@@ -39,8 +40,8 @@
val status: string list -> unit
val report: string list -> unit
val result: Properties.T -> string list -> unit
- val protocol_message: Properties.T -> string list -> unit
- val try_protocol_message: Properties.T -> string list -> unit
+ val protocol_message: protocol_message_fn
+ val try_protocol_message: protocol_message_fn
end;
signature PRIVATE_OUTPUT =
@@ -57,7 +58,7 @@
val status_fn: (output list -> unit) Unsynchronized.ref
val report_fn: (output list -> unit) Unsynchronized.ref
val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
- val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
+ val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref
val init_channels: unit -> unit
end;
@@ -105,6 +106,8 @@
val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
+
+type protocol_message_fn = Output_Primitives.protocol_message_fn;
val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
@@ -121,8 +124,8 @@
exception Protocol_Message of Properties.T;
-fun protocol_message_undefined props (_: string list) =
- raise Protocol_Message props;
+val protocol_message_undefined: Output_Primitives.protocol_message_fn =
+ fn props => fn _ => raise Protocol_Message props;
fun init_channels () =
(writeln_fn := (physical_writeln o implode);
@@ -153,8 +156,8 @@
fun status ss = ! status_fn (map output ss);
fun report ss = ! report_fn (map output ss);
fun result props ss = ! result_fn props (map output ss);
-fun protocol_message props ss = ! protocol_message_fn props (map output ss);
-fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
+fun protocol_message props body = ! protocol_message_fn props body;
+fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
(* profiling *)
--- a/src/Pure/General/output_primitives.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/General/output_primitives.ML Sat Nov 02 14:31:48 2019 +0000
@@ -6,6 +6,14 @@
signature OUTPUT_PRIMITIVES =
sig
+ structure XML:
+ sig
+ type attributes = (string * string) list
+ datatype tree =
+ Elem of (string * attributes) * tree list
+ | Text of string
+ type body = tree list
+ end
type output = string
type serial = int
type properties = (string * string) list
@@ -21,13 +29,31 @@
val status_fn: output list -> unit
val report_fn: output list -> unit
val result_fn: properties -> output list -> unit
- val protocol_message_fn: properties -> output list -> unit
+ type protocol_message_fn = properties -> XML.body -> unit
+ val protocol_message_fn: protocol_message_fn
val markup_fn: string * properties -> output * output
end;
structure Output_Primitives: OUTPUT_PRIMITIVES =
struct
+(** XML trees **)
+
+structure XML =
+struct
+
+type attributes = (string * string) list;
+
+datatype tree =
+ Elem of (string * attributes) * tree list
+ | Text of string;
+
+type body = tree list;
+end;
+
+
+(* output *)
+
type output = string;
type serial = int;
type properties = (string * string) list;
@@ -45,7 +71,9 @@
val status_fn = ignore_outputs;
val report_fn = ignore_outputs;
fun result_fn (_: properties) = ignore_outputs;
-fun protocol_message_fn (_: properties) = ignore_outputs;
+
+type protocol_message_fn = properties -> XML.body -> unit;
+val protocol_message_fn: protocol_message_fn = fn _ => fn _ => ();
fun markup_fn (_: string * properties) = ("", "");
--- a/src/Pure/PIDE/byte_message.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/PIDE/byte_message.ML Sat Nov 02 14:31:48 2019 +0000
@@ -23,7 +23,7 @@
(* output operations *)
-fun write stream = List.app (fn s => BinIO.output (stream, Byte.stringToBytes s));
+fun write stream = List.app (File.output stream);
fun flush stream = ignore (try BinIO.flushOut stream);
--- a/src/Pure/PIDE/protocol.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/PIDE/protocol.ML Sat Nov 02 14:31:48 2019 +0000
@@ -62,7 +62,7 @@
tokens = toks ~~ sources}
end;
-fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [commas ids];
+fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [XML.Text (commas ids)];
val _ =
Isabelle_Process.protocol_command "Document.define_command"
@@ -146,8 +146,7 @@
open XML.Encode;
fun encode_upd (a, bs) =
string (space_implode "," (map Value.print_int (a :: bs)));
- in triple int (list string) (list encode_upd) end
- |> YXML.chunks_of_body);
+ in triple int (list string) (list encode_upd) end);
in Document.start_execution state' end)));
val _ =
@@ -158,7 +157,7 @@
YXML.parse_body versions_yxml |>
let open XML.Decode in list int end;
val state1 = Document.remove_versions versions state;
- val _ = Output.protocol_message Markup.removed_versions [versions_yxml];
+ val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)];
in state1 end));
val _ =
--- a/src/Pure/PIDE/xml.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/PIDE/xml.ML Sat Nov 02 14:31:48 2019 +0000
@@ -34,6 +34,9 @@
Elem of (string * attributes) * tree list
| Text of string
type body = tree list
+ val blob: string list -> body
+ val is_empty: tree -> bool
+ val is_empty_body: body -> bool
val xml_elemN: string
val xml_nameN: string
val xml_bodyN: string
@@ -48,7 +51,6 @@
val output_markup: Markup.T -> Markup.output
val string_of: tree -> string
val pretty: int -> tree -> Pretty.T
- val output: tree -> BinIO.outstream -> unit
val parse_comments: string list -> unit * string list
val parse_string : string -> string option
val parse_element: string list -> tree * string list
@@ -73,13 +75,14 @@
(** XML trees **)
-type attributes = (string * string) list;
+open Output_Primitives.XML;
+
+val blob = map Text;
-datatype tree =
- Elem of (string * attributes) * tree list
- | Text of string;
+fun is_empty (Text "") = true
+ | is_empty _ = false;
-type body = tree list;
+val is_empty_body = forall is_empty;
(* wrapped elements *)
@@ -177,7 +180,6 @@
in Buffer.empty |> traverse depth tree end;
val string_of = Buffer.content o buffer_of ~1;
-val output = Buffer.output o buffer_of ~1;
fun pretty depth tree =
Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
--- a/src/Pure/PIDE/yxml.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/PIDE/yxml.ML Sat Nov 02 14:31:48 2019 +0000
@@ -20,12 +20,11 @@
val Y: Symbol.symbol
val embed_controls: string -> string
val detect: string -> bool
- val output_markup: Markup.T -> string * string
- val buffer_body: XML.body -> Buffer.T -> Buffer.T
- val buffer: XML.tree -> Buffer.T -> Buffer.T
- val chunks_of_body: XML.body -> string list
+ val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
val string_of_body: XML.body -> string
val string_of: XML.tree -> string
+ val write_body: Path.T -> XML.body -> unit
+ val output_markup: Markup.T -> string * string
val output_markup_elem: Markup.T -> (string * string) * string
val parse_body: string -> XML.body
val parse: string -> XML.tree
@@ -65,30 +64,33 @@
(* output *)
+fun traverse string =
+ let
+ fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
+ fun tree (XML.Elem ((name, atts), ts)) =
+ string XY #> string name #> fold attrib atts #> string X #>
+ fold tree ts #>
+ string XYX
+ | tree (XML.Text s) = string s;
+ in tree end;
+
+fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
+val string_of = string_of_body o single;
+
+fun write_body path body =
+ path |> File.open_output (fn file =>
+ fold (traverse (fn s => fn () => File.output file s)) body ());
+
+
+(* markup elements *)
+
+val Z = chr 0;
+val Z_text = [XML.Text Z];
+
fun output_markup (markup as (name, atts)) =
if Markup.is_empty markup then Markup.no_output
else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
-fun buffer_attrib (a, x) =
- Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
-
-fun buffer_body ts = fold buffer ts
-and buffer (XML.Elem ((name, atts), ts)) =
- Buffer.add XY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add X #>
- buffer_body ts #>
- Buffer.add XYX
- | buffer (XML.Text s) = Buffer.add s
-
-fun chunks_of_body body = Buffer.empty |> buffer_body body |> Buffer.chunks;
-fun string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content;
-val string_of = string_of_body o single;
-
-
-(* wrapped elements *)
-
-val Z = chr 0;
-val Z_text = [XML.Text Z];
-
fun output_markup_elem markup =
let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
in ((bg1, bg2), en) end;
--- a/src/Pure/System/invoke_scala.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/System/invoke_scala.ML Sat Nov 02 14:31:48 2019 +0000
@@ -33,7 +33,7 @@
fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
val promise = Future.promise_name "invoke_scala" abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
- val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
+ val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
in promise end;
fun method name arg = Future.join (promise_method name arg);
--- a/src/Pure/System/isabelle_process.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/System/isabelle_process.ML Sat Nov 02 14:31:48 2019 +0000
@@ -106,15 +106,15 @@
fun message name props body =
Message_Channel.send msg_channel (Message_Channel.message name props body);
- fun standard_message props name body =
- if forall (fn s => s = "") body then ()
+ fun standard_message props name ss =
+ if forall (fn s => s = "") ss then ()
else
let
val props' =
(case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
(false, SOME id') => props @ [(Markup.idN, id')]
| _ => props);
- in message name props' body end;
+ in message name props' (XML.blob ss) end;
in
Private_Output.status_fn := standard_message [] Markup.statusN;
Private_Output.report_fn := standard_message [] Markup.reportN;
@@ -130,11 +130,13 @@
Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
Private_Output.error_message_fn :=
(fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
- Private_Output.system_message_fn := message Markup.systemN [];
- Private_Output.protocol_message_fn := message Markup.protocolN;
+ Private_Output.system_message_fn :=
+ (fn ss => message Markup.systemN [] (XML.blob ss));
+ Private_Output.protocol_message_fn :=
+ (fn props => fn body => message Markup.protocolN props body);
Session.init_protocol_handlers ();
- message Markup.initN [] [Session.welcome ()];
+ message Markup.initN [] [XML.Text (Session.welcome ())];
msg_channel
end;
--- a/src/Pure/System/message_channel.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/System/message_channel.ML Sat Nov 02 14:31:48 2019 +0000
@@ -7,7 +7,7 @@
signature MESSAGE_CHANNEL =
sig
type message
- val message: string -> Properties.T -> string list -> message
+ val message: string -> Properties.T -> XML.body -> message
type T
val send: T -> message -> unit
val shutdown: T -> unit
@@ -19,19 +19,20 @@
(* message *)
-datatype message = Message of string list;
+datatype message = Message of XML.body;
-fun chunk ss =
- string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss;
+fun body_size body = fold (YXML.traverse (Integer.add o size)) body 0;
+
+fun chunk body = XML.Text (string_of_int (body_size body) ^ "\n") :: body;
fun message name raw_props body =
let
val robust_props = map (apply2 YXML.embed_controls) raw_props;
- val header = YXML.string_of (XML.Elem ((name, robust_props), []));
+ val header = XML.Elem ((name, robust_props), []);
in Message (chunk [header] @ chunk body) end;
-fun output_message stream (Message ss) =
- List.app (File.output stream) ss;
+fun output_message stream (Message body) =
+ fold (YXML.traverse (fn s => fn () => File.output stream s)) body ();
(* channel *)
--- a/src/Pure/Thy/export.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Thy/export.ML Sat Nov 02 14:31:48 2019 +0000
@@ -9,14 +9,14 @@
val report_export: theory -> Path.binding -> unit
type params =
{theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
- val export_params: params -> string list -> unit
- val export: theory -> Path.binding -> string list -> unit
- val export_executable: theory -> Path.binding -> string list -> unit
+ val export_params: params -> XML.body -> unit
+ val export: theory -> Path.binding -> XML.body -> unit
+ val export_executable: theory -> Path.binding -> XML.body -> unit
val export_file: theory -> Path.binding -> Path.T -> unit
val export_executable_file: theory -> Path.binding -> Path.T -> unit
val markup: theory -> Path.T -> Markup.T
val message: theory -> Path.T -> string
- val protocol_message: Properties.T -> string list -> unit
+ val protocol_message: Output.protocol_message_fn
end;
structure Export: EXPORT =
@@ -34,7 +34,7 @@
type params =
{theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
-fun export_params ({theory = thy, binding, executable, compress, strict}: params) blob =
+fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
(report_export thy binding;
(Output.try_protocol_message o Markup.export)
{id = Position.get_id (Position.thread_data ()),
@@ -43,18 +43,21 @@
name = Path.implode_binding (tap Path.proper_binding binding),
executable = executable,
compress = compress,
- strict = strict} blob);
+ strict = strict} body);
-fun export thy binding blob =
+fun export thy binding body =
export_params
- {theory = thy, binding = binding, executable = false, compress = true, strict = true} blob;
+ {theory = thy, binding = binding, executable = false, compress = true, strict = true} body;
-fun export_executable thy binding blob =
+fun export_executable thy binding body =
export_params
- {theory = thy, binding = binding, executable = true, compress = true, strict = true} blob;
+ {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
-fun export_file thy binding file = export thy binding [File.read file];
-fun export_executable_file thy binding file = export_executable thy binding [File.read file];
+fun export_file thy binding file =
+ export thy binding [XML.Text (File.read file)];
+
+fun export_executable_file thy binding file =
+ export_executable thy binding [XML.Text (File.read file)];
(* information message *)
@@ -71,7 +74,7 @@
(* protocol message (bootstrap) *)
-fun protocol_message props output =
+fun protocol_message props body =
(case props of
function :: args =>
if function = (Markup.functionN, Markup.exportN) andalso
@@ -79,7 +82,7 @@
then
let
val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
- val _ = File.write_list path output;
+ val _ = YXML.write_body path body;
in Protocol_Message.inline (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
else raise Output.Protocol_Message props
| [] => raise Output.Protocol_Message props);
--- a/src/Pure/Thy/export_theory.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Thy/export_theory.ML Sat Nov 02 14:31:48 2019 +0000
@@ -125,12 +125,9 @@
Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
if Options.bool (#options context) "export_theory" then f context thy else ()));
-fun export_buffer thy name buffer =
- if Buffer.is_empty buffer then ()
- else Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks buffer);
-
-fun export_body thy name elems =
- export_buffer thy name (YXML.buffer_body elems Buffer.empty);
+fun export_body thy name body =
+ if XML.is_empty_body body then ()
+ else Export.export thy (Path.binding0 (Path.make ["theory", name])) body;
(* presentation *)
@@ -301,17 +298,13 @@
in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end
end;
- fun buffer_export_thm (thm_id, thm_name) =
+ fun export_thm (thm_id, thm_name) =
let
val markup = entity_markup_thm (#serial thm_id, thm_name);
val thm = Global_Theory.get_thm_name thy (thm_name, Position.none);
- val body = encode_thm thm_id thm;
- in YXML.buffer (XML.Elem (markup, body)) end;
+ in XML.Elem (markup, encode_thm thm_id thm) end;
- val _ =
- Buffer.empty
- |> fold buffer_export_thm (Global_Theory.dest_thm_names thy)
- |> export_buffer thy "thms";
+ val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy));
(* type classes *)
@@ -420,7 +413,7 @@
val _ =
Export.export thy \<^path_binding>\<open>theory/parents\<close>
- [YXML.string_of_body (XML.Encode.string (cat_lines (map Context.theory_long_name parents)))];
+ (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
in () end);
--- a/src/Pure/Thy/thy_info.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Thy/thy_info.ML Sat Nov 02 14:31:48 2019 +0000
@@ -65,8 +65,9 @@
val latex = Latex.isabelle_body (Context.theory_name thy) body;
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
val _ =
- if Options.bool options "export_document"
- then Export.export thy (Path.explode_binding0 "document.tex") output else ();
+ if Options.bool options "export_document" then
+ Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output)
+ else ();
val _ = if #enabled option then Present.theory_output thy output else ();
in () end
end));
--- a/src/Pure/Tools/build.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Tools/build.ML Sat Nov 02 14:31:48 2019 +0000
@@ -239,11 +239,12 @@
val _ =
Isabelle_Process.protocol_command "build_session"
(fn [args_yxml] =>
- let
- val args = decode_args args_yxml;
- val result = (build_session args; "") handle exn =>
- (Runtime.exn_message exn handle _ (*sic!*) =>
- "Exception raised, but failed to print details!");
- in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
+ let
+ val args = decode_args args_yxml;
+ val result = (build_session args; "") handle exn =>
+ (Runtime.exn_message exn handle _ (*sic!*) =>
+ "Exception raised, but failed to print details!");
+ in Output.protocol_message Markup.build_session_finished [XML.Text result] end
+ | _ => raise Match);
end;
--- a/src/Pure/Tools/debugger.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Tools/debugger.ML Sat Nov 02 14:31:48 2019 +0000
@@ -23,7 +23,7 @@
else
Output.protocol_message
(Markup.debugger_output (Standard_Thread.the_name ()))
- [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
+ [XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)];
val writeln_message = output_message Markup.writelnN;
val warning_message = output_message Markup.warningN;
@@ -201,13 +201,12 @@
fun debugger_state thread_name =
Output.protocol_message (Markup.debugger_state thread_name)
- [get_debugging ()
+ (get_debugging ()
|> map (fn st =>
(Position.properties_of
(Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)),
PolyML.DebuggerInterface.debugFunction st))
- |> let open XML.Encode in list (pair properties string) end
- |> YXML.string_of_body];
+ |> let open XML.Encode in list (pair properties string) end);
fun debugger_command thread_name =
(case get_input thread_name of
--- a/src/Pure/Tools/generated_files.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Tools/generated_files.ML Sat Nov 02 14:31:48 2019 +0000
@@ -136,7 +136,7 @@
in () end;
fun export_file thy (file: file) =
- Export.export thy (file_binding file) [#content file];
+ Export.export thy (file_binding file) [XML.Text (#content file)];
(* file types *)
@@ -290,7 +290,7 @@
Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
in
(if is_some executable then Export.export_executable else Export.export)
- thy binding' [content]
+ thy binding' [XML.Text content]
end));
val _ =
if null export then ()
--- a/src/Pure/Tools/print_operation.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/Tools/print_operation.ML Sat Nov 02 14:31:48 2019 +0000
@@ -23,13 +23,9 @@
fun report () =
Output.try_protocol_message Markup.print_operations
- let
- val yxml =
- Synchronized.value print_operations
- |> map (fn (x, (y, _)) => (x, y)) |> rev
- |> let open XML.Encode in list (pair string string) end
- |> YXML.string_of_body;
- in [yxml] end;
+ (Synchronized.value print_operations
+ |> map (fn (x, (y, _)) => (x, y)) |> rev
+ |> let open XML.Encode in list (pair string string) end);
val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
--- a/src/Pure/proofterm.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Pure/proofterm.ML Sat Nov 02 14:31:48 2019 +0000
@@ -2150,14 +2150,13 @@
val encode_term = encode_standard_term consts;
val encode_proof = encode_standard_proof consts;
in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
- val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
in
- chunks |> Export.export_params
+ Export.export_params
{theory = thy,
binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
executable = false,
compress = true,
- strict = false}
+ strict = false} xml
end;
fun export thy i prop prf =
--- a/src/Tools/Code/code_target.ML Sat Nov 02 14:31:34 2019 +0000
+++ b/src/Tools/Code/code_target.ML Sat Nov 02 14:31:48 2019 +0000
@@ -282,7 +282,7 @@
fun export binding content thy =
let
val thy' = thy |> Generated_Files.add_files (binding, content);
- val _ = Export.export thy' binding [content];
+ val _ = Export.export thy' binding [XML.Text content];
in thy' end;
local