# HG changeset patch
# User wenzelm
# Date 1681497737 -7200
# Node ID 5ba68d3bd74113ed5659c98851afe28fadcfad37
# Parent  39007362ab7d4291e114b1f939649f6b7cee9cbe
more operations, following Isabelle/ML conventions;

diff -r 39007362ab7d -r 5ba68d3bd741 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/General/symbol.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -110,13 +110,11 @@
 fun is_space s = s = space;
 
 local
-  val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
+  val spaces0 = Vector.tabulate (65, fn i => replicate_string i space);
 in
   fun spaces n =
-    if n < 64 then Vector.sub (small_spaces, n)
-    else
-      replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^
-        Vector.sub (small_spaces, n mod 64);
+    if n < 64 then Vector.nth spaces0 n
+    else replicate_string (n div 64) (Vector.nth spaces0 64) ^ Vector.nth spaces0 (n mod 64);
 end;
 
 val comment = "\<comment>";
diff -r 39007362ab7d -r 5ba68d3bd741 src/Pure/General/vector.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/vector.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Pure/General/vector.ML
+    Author:     Makarius
+
+Additional operations for structure Vector, following Isabelle/ML conventions.
+*)
+
+signature VECTOR =
+sig
+  include VECTOR
+  val nth: 'a vector -> int -> 'a
+  val forall: ('a -> bool) -> 'a vector -> bool
+  val fold: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
+  val fold_rev: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
+end;
+
+structure Vector: VECTOR =
+struct
+
+open Vector;
+
+fun nth vec i = sub (vec, i);
+
+val forall = all;
+
+fun fold f vec x = foldl (fn (a, b) => f a b) x vec;
+fun fold_rev f vec x = foldr (fn (a, b) => f a b) x vec;
+
+end;
diff -r 39007362ab7d -r 5ba68d3bd741 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/Isar/token.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -731,7 +731,7 @@
     val range = Position.range (pos, pos');
     val tok =
       if 0 <= k andalso k < Vector.length immediate_kinds then
-        Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
+        Token ((s, range), (Vector.nth immediate_kinds k, s), Slot)
       else
         (case explode Keyword.empty_keywords pos s of
           [tok] => tok
diff -r 39007362ab7d -r 5ba68d3bd741 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -19,6 +19,7 @@
 ML_file "ML/ml_system.ML";
 
 ML_file "General/basics.ML";
+ML_file "General/vector.ML";
 ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";
diff -r 39007362ab7d -r 5ba68d3bd741 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -130,7 +130,7 @@
     String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel,
     Comment Comment.Latex, Dummy, EOF];
 
-fun token_kind i = Vector.sub (token_kinds, i);
+val token_kind = Vector.nth token_kinds;
 fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds));
 
 
diff -r 39007362ab7d -r 5ba68d3bd741 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -407,7 +407,7 @@
     fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
 
     fun pretty_prod (name, tag) =
-      (prods_content (#2 (Vector.sub (prods, tag))) @ map prod_of_chain (chains_preds chains tag))
+      (prods_content (#2 (Vector.nth prods tag)) @ map prod_of_chain (chains_preds chains tag))
       |> map (fn (symbs, const, p) =>
           Pretty.block (Pretty.breaks
             (Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const)));
@@ -476,7 +476,7 @@
         val prods' =
           let
             fun get_prod i =
-              if i < nt_count then Vector.sub (prods, i)
+              if i < nt_count then Vector.nth prods i
               else nt_gram_empty;
           in Array.tabulate (nt_count', get_prod) end;
 
@@ -601,7 +601,7 @@
     fun token_prods prods =
       fold cons (prods_lookup prods tk) #>
       fold cons (prods_lookup prods Lexicon.dummy);
-    fun nt_prods nt = #2 (Vector.sub (prods, nt));
+    fun nt_prods nt = #2 (Vector.nth prods nt);
   in fold (token_prods o nt_prods) (chains_all_preds chains [nt]) [] end;
 
 
diff -r 39007362ab7d -r 5ba68d3bd741 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/library.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -658,7 +658,7 @@
 fun string_of_int i =
   if i < 0 then Int.toString i
   else if i < 10 then chr (zero + i)
-  else if i < small_int then Vector.sub (small_int_table, i)
+  else if i < small_int then Vector.nth small_int_table i
   else Int.toString i;
 
 end;
diff -r 39007362ab7d -r 5ba68d3bd741 src/Pure/name.ML
--- a/src/Pure/name.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/name.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -59,8 +59,8 @@
   in ":" ^ leading ^ string_of_int i end);
 
 fun bound n =
-  if n < 1000 then Vector.sub (small_int, n)
-  else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
+  if n < 1000 then Vector.nth small_int n
+  else ":" ^ bound (n div 1000) ^ Vector.nth small_int (n mod 1000);
 
 val is_bound = String.isPrefix ":";