# HG changeset patch
# User wenzelm
# Date 1681500891 -7200
# Node ID 3bb6468d202e8079e0ef088895ee0da5cc85c84f
# Parent  5ba68d3bd74113ed5659c98851afe28fadcfad37
more operations, following Isabelle/ML conventions;

diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/General/bytes.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -158,7 +158,7 @@
   else if size sep <> 1 then [content bytes]
   else
     let
-      val sep_char = String.sub (sep, 0);
+      val sep_char = String.nth sep 0;
 
       fun add_part s part =
         Buffer.add (Substring.string s) (the_default Buffer.empty part);
diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/General/long_name.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -40,9 +40,9 @@
 (* long names separated by "." *)
 
 val separator = ".";
-val separator_char = String.sub (separator, 0);
+val separator_char = String.nth separator 0;
 
-val is_qualified = exists_string (fn s => s = separator);
+fun is_qualified name = String.member name separator_char;
 
 val hidden_prefix = "??."
 val hidden = prefix hidden_prefix;
@@ -85,7 +85,7 @@
 fun string_ops string =
   let
     val n = size string;
-    fun char i = String.sub (string, i);
+    val char = String.nth string;
     fun string_end i = i >= n;
     fun chunk_end i = string_end i orelse char i = separator_char;
   in {string_end = string_end, chunk_end = chunk_end} end;
diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/General/string.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/string.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -0,0 +1,50 @@
+(*  Title:      Pure/General/string.ML
+    Author:     Makarius
+
+Additional operations for structure String, following Isabelle/ML conventions.
+
+NB: Isabelle normally works with Symbol.symbol, which is represented as a
+small string fragment. Raw type char is rarely useful.
+*)
+
+signature STRING =
+sig
+  include STRING
+  val nth: string -> int -> char
+  val exists: (char -> bool) -> string -> bool
+  val forall: (char -> bool) -> string -> bool
+  val member: string -> char -> bool
+  val fold: (char -> 'a -> 'a) -> string -> 'a -> 'a
+  val fold_rev: (char -> 'a -> 'a) -> string -> 'a -> 'a
+end;
+
+structure String: STRING =
+struct
+
+open String;
+
+fun nth str i = sub (str, i);
+
+fun exists pred str =
+  let
+    val n = size str;
+    fun ex i = Int.< (i, n) andalso (pred (nth str i) orelse ex (i + 1));
+  in ex 0 end;
+
+fun forall pred = not o exists (not o pred);
+
+fun member str c = exists (fn c' => c = c') str;
+
+fun fold f str x0 =
+  let
+    val n = size str;
+    fun iter (x, i) = if Int.< (i, n) then iter (f (nth str i) x, i + 1) else x;
+  in iter (x0, 0) end;
+
+fun fold_rev f str x0 =
+  let
+    val n = size str;
+    fun iter (x, i) = if Int.>= (i, 0) then iter (f (nth str i) x, i - 1) else x;
+  in iter (x0, n - 1) end;
+
+end;
diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/General/symbol.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -124,7 +124,7 @@
 
 fun is_char s = size s = 1;
 
-fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
+fun is_utf8 s = size s > 0 andalso String.forall (fn c => Char.ord c >= 128) s;
 
 fun raw_symbolic s =
   String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s);
diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/General/symbol_explode.ML
--- a/src/Pure/General/symbol_explode.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/General/symbol_explode.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -17,7 +17,7 @@
 
 fun explode string =
   let
-    fun char i = String.sub (string, i);
+    val char = String.nth string;
     fun substring i j = String.substring (string, i, j - i);
 
     val n = size string;
diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/General/value.ML
--- a/src/Pure/General/value.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/General/value.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -42,7 +42,7 @@
 fun parse_int str =
   let
     fun err () = raise Fail ("Bad integer " ^ quote str);
-    fun char i = Char.ord (String.sub (str, i));
+    val char = Char.ord o String.nth str;
     val n = size str;
 
     fun digits i a =
diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -19,6 +19,7 @@
 ML_file "ML/ml_system.ML";
 
 ML_file "General/basics.ML";
+ML_file "General/string.ML";
 ML_file "General/vector.ML";
 ML_file "General/symbol_explode.ML";
 
diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/library.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -716,7 +716,7 @@
 fun member_string str s = exists_string (fn s' => s = s') str;
 
 fun last_string "" = NONE
-  | last_string s = SOME (str (String.sub (s, size s - 1)));
+  | last_string s = SOME (str (String.nth s (size s - 1)));
 
 fun first_field sep str =
   let