--- a/src/Pure/General/bytes.ML Mon Sep 02 20:12:52 2024 +0200
+++ b/src/Pure/General/bytes.ML Mon Sep 02 20:54:00 2024 +0200
@@ -211,13 +211,4 @@
fun write path bytes = File_Stream.open_output (fn stream => write_stream stream bytes) path;
-
-(* ML pretty printing *)
-
-val _ =
- ML_system_pp (fn _ => fn _ => fn bytes =>
- PolyML.PrettyString
- (if is_empty bytes then "Bytes.empty"
- else "Bytes {size = " ^ string_of_int (size bytes) ^ "}"))
-
end;
--- a/src/Pure/General/path.ML Mon Sep 02 20:12:52 2024 +0200
+++ b/src/Pure/General/path.ML Mon Sep 02 20:54:00 2024 +0200
@@ -26,7 +26,7 @@
val explode: string -> T
val explode_pos: string * Position.T -> T * Position.T
val split: string -> T list
- val pretty: T -> Pretty.T
+ val print_markup: T -> Markup.T * string
val print: T -> string
val dir: T -> T
val base: T -> T
@@ -188,13 +188,11 @@
(* print *)
-fun pretty path =
+fun print_markup path =
let val s = implode_path path
- in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
+ in (Markup.path s, quote s) end;
-val print = Pretty.unformatted_string_of o pretty;
-
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
+val print = print_markup #-> Markup.markup;
(* base element *)
--- a/src/Pure/ML/ml_pp.ML Mon Sep 02 20:12:52 2024 +0200
+++ b/src/Pure/ML/ml_pp.ML Mon Sep 02 20:54:00 2024 +0200
@@ -8,6 +8,15 @@
struct
val _ =
+ ML_system_pp (fn _ => fn _ => fn bytes =>
+ PolyML.PrettyString
+ (if Bytes.is_empty bytes then "Bytes.empty"
+ else "Bytes {size = " ^ string_of_int (Bytes.size bytes) ^ "}"));
+
+val _ =
+ ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.mark_str o Path.print_markup);
+
+val _ =
ML_system_pp (fn _ => fn _ => fn t =>
PolyML.PrettyString ("<thread " ^ quote (Isabelle_Thread.print t) ^
(if Isabelle_Thread.is_active t then "" else " (inactive)") ^ ">"));
--- a/src/Pure/PIDE/xml.ML Mon Sep 02 20:12:52 2024 +0200
+++ b/src/Pure/PIDE/xml.ML Mon Sep 02 20:54:00 2024 +0200
@@ -37,13 +37,7 @@
val is_empty_body: body -> bool
val string: string -> body
val enclose: string -> string -> body -> body
- val xml_elemN: string
- val xml_nameN: string
- val xml_bodyN: string
- val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
- val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
val add_content: tree -> Buffer.T -> Buffer.T
- val content_of: body -> string
val trim_blanks: body -> body
val header: string
val text: string -> string
@@ -98,21 +92,6 @@
fun enclose bg en body = string bg @ body @ string en;
-(* wrapped elements *)
-
-val xml_elemN = "xml_elem";
-val xml_nameN = "xml_name";
-val xml_bodyN = "xml_body";
-
-fun wrap_elem (((a, atts), body1), body2) =
- Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
-
-fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
- if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
- then SOME (((a, atts), body1), body2) else NONE
- | unwrap_elem _ = NONE;
-
-
(* text content *)
fun add_content tree =
@@ -123,8 +102,6 @@
Elem (_, ts) => fold add_content ts
| Text s => Buffer.add s));
-val content_of = Buffer.build_content o fold add_content;
-
(* trim blanks *)
--- a/src/Pure/PIDE/xml_type.ML Mon Sep 02 20:12:52 2024 +0200
+++ b/src/Pure/PIDE/xml_type.ML Mon Sep 02 20:54:00 2024 +0200
@@ -11,6 +11,12 @@
Elem of (string * attributes) * tree list
| Text of string
type body = tree list
+ val xml_elemN: string
+ val xml_nameN: string
+ val xml_bodyN: string
+ val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
+ val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
+ val content_of: body -> string
end
structure XML: XML =
@@ -24,4 +30,35 @@
type body = tree list;
+
+(* wrapped elements *)
+
+val xml_elemN = "xml_elem";
+val xml_nameN = "xml_name";
+val xml_bodyN = "xml_body";
+
+fun wrap_elem (((a, atts), body1), body2) =
+ Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
+
+fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
+ if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
+ then SOME (((a, atts), body1), body2) else NONE
+ | unwrap_elem _ = NONE;
+
+
+(* text content *)
+
+fun add_contents [] res = res
+ | add_contents (t :: ts) res = add_contents ts (add_content t res)
+and add_content tree res =
+ (case unwrap_elem tree of
+ SOME (_, ts) => add_contents ts res
+ | NONE =>
+ (case tree of
+ Elem (_, ts) => add_contents ts res
+ | Text s => s :: res));
+
+fun content_of body =
+ String.concat (rev (add_contents body []));
+
end;
--- a/src/Pure/ROOT.ML Mon Sep 02 20:12:52 2024 +0200
+++ b/src/Pure/ROOT.ML Mon Sep 02 20:54:00 2024 +0200
@@ -80,14 +80,15 @@
ML_file "General/linear_set.ML";
ML_file "General/change_table.ML";
ML_file "General/buffer.ML";
+ML_file "General/path.ML";
+ML_file "General/file_stream.ML";
+ML_file "General/bytes.ML";
+ML_file "PIDE/yxml.ML";
ML_file "General/pretty.ML";
ML_file "General/rat.ML";
ML_file "PIDE/xml.ML";
-ML_file "General/path.ML";
ML_file "General/url.ML";
ML_file "System/bash.ML";
-ML_file "General/file_stream.ML";
-ML_file "General/bytes.ML";
ML_file "General/file.ML";
ML_file "General/long_name.ML";
ML_file "General/binding.ML";
@@ -96,7 +97,6 @@
ML_file "General/timing.ML";
ML_file "General/sha1.ML";
-ML_file "PIDE/yxml.ML";
ML_file "ML/ml_profiling.ML";
ML_file "PIDE/byte_message.ML";
ML_file "PIDE/protocol_message.ML";