clarified modules: enable pretty.ML to use XML/YXML more directly;
authorwenzelm
Mon, 02 Sep 2024 20:54:00 +0200
changeset 80803 7e39c785ca5d
parent 80802 c3c76f4880bc
child 80804 9035d32b4af3
clarified modules: enable pretty.ML to use XML/YXML more directly;
src/Pure/General/bytes.ML
src/Pure/General/path.ML
src/Pure/ML/ml_pp.ML
src/Pure/PIDE/xml.ML
src/Pure/PIDE/xml_type.ML
src/Pure/ROOT.ML
--- 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";