# HG changeset patch # User wenzelm # Date 1725303240 -7200 # Node ID 7e39c785ca5d9e7cb33d1fd7ef426eb7faaaae74 # Parent c3c76f4880bc02fb0aa75d773a227285cea75809 clarified modules: enable pretty.ML to use XML/YXML more directly; diff -r c3c76f4880bc -r 7e39c785ca5d src/Pure/General/bytes.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; diff -r c3c76f4880bc -r 7e39c785ca5d src/Pure/General/path.ML --- 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 *) diff -r c3c76f4880bc -r 7e39c785ca5d src/Pure/ML/ml_pp.ML --- 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 ("")); diff -r c3c76f4880bc -r 7e39c785ca5d src/Pure/PIDE/xml.ML --- 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 *) diff -r c3c76f4880bc -r 7e39c785ca5d src/Pure/PIDE/xml_type.ML --- 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; diff -r c3c76f4880bc -r 7e39c785ca5d src/Pure/ROOT.ML --- 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";