# HG changeset patch
# User wenzelm
# Date 1693325824 -7200
# Node ID 4da5cdaa4dcd15ffc1c1784dc94275fc2fa8d1e3
# Parent  60561d28569bc33daeca23d3fa071842b7f339d9
clarified signature;

diff -r 60561d28569b -r 4da5cdaa4dcd src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Tue Aug 29 18:13:30 2023 +0200
+++ b/src/Pure/General/word.scala	Tue Aug 29 18:17:04 2023 +0200
@@ -25,16 +25,16 @@
   def lowercase(str: String): String = str.toLowerCase(Locale.ROOT)
   def uppercase(str: String): String = str.toUpperCase(Locale.ROOT)
 
-  def capitalize(str: String): String =
+  def capitalized(str: String): String =
     if (str.length == 0) str
     else {
       val n = Character.charCount(str.codePointAt(0))
       uppercase(str.substring(0, n)) + lowercase(str.substring(n))
     }
 
-  def perhaps_capitalize(str: String): String =
+  def perhaps_capitalized(str: String): String =
     if (Codepoint.iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
-      capitalize(str)
+      capitalized(str)
     else str
 
   object Case {
@@ -42,7 +42,7 @@
       c match {
         case Case.lowercase => Word.lowercase(str)
         case Case.uppercase => Word.uppercase(str)
-        case Case.capitalized => Word.capitalize(str)
+        case Case.capitalized => Word.capitalized(str)
       }
     def unapply(str: String): Option[Case] =
       if (str.nonEmpty) {
diff -r 60561d28569b -r 4da5cdaa4dcd src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Aug 29 18:13:30 2023 +0200
+++ b/src/Pure/System/options.scala	Tue Aug 29 18:17:04 2023 +0200
@@ -117,7 +117,7 @@
           case word :: rest if word == strip => rest
           case _ => words
         }
-      Word.implode(words1.map(Word.perhaps_capitalize))
+      Word.implode(words1.map(Word.perhaps_capitalized))
     }
     def title_jedit: String = title("jedit")
 
diff -r 60561d28569b -r 4da5cdaa4dcd src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Tue Aug 29 18:13:30 2023 +0200
+++ b/src/Pure/Thy/bibtex.scala	Tue Aug 29 18:17:04 2023 +0200
@@ -132,11 +132,11 @@
               case (Error(msg, Value.Int(l)), _) =>
                 Some((true, (msg, get_line_pos(l))))
               case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
-                Some((false, (Word.capitalize(msg) + " in entry " + quote(name), chunk_pos(name))))
+                Some((false, (Word.capitalized(msg) + " in entry " + quote(name), chunk_pos(name))))
               case (Warning(msg), Warning_Line(Value.Int(l))) =>
-                Some((false, (Word.capitalize(msg), get_line_pos(l))))
+                Some((false, (Word.capitalized(msg), get_line_pos(l))))
               case (Warning(msg), _) =>
-                Some((false, (Word.capitalize(msg), Position.none)))
+                Some((false, (Word.capitalized(msg), Position.none)))
               case _ => None
             }
           ).partition(_._1)
diff -r 60561d28569b -r 4da5cdaa4dcd src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Aug 29 18:13:30 2023 +0200
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Aug 29 18:17:04 2023 +0200
@@ -278,7 +278,7 @@
 
   private val auto_build_button =
     new JEdit_Options.Bool_GUI(document_auto, "Auto") {
-      tooltip = Word.capitalize(document_auto.description)
+      tooltip = Word.capitalized(document_auto.description)
       override def clicked(state: Boolean): Unit = {
         super.clicked(state)
 
diff -r 60561d28569b -r 4da5cdaa4dcd src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Aug 29 18:13:30 2023 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Aug 29 18:17:04 2023 +0200
@@ -91,7 +91,7 @@
   extends GUI.Selector[String](batches: _*) with JEdit_Options.Entry {
     name = option_name
     tooltip =
-      if (standalone) Word.capitalize(options.value.description(option_name))
+      if (standalone) Word.capitalized(options.value.description(option_name))
       else options.value.check_name(option_name).print_default
 
     override val title: String =
diff -r 60561d28569b -r 4da5cdaa4dcd src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Tue Aug 29 18:13:30 2023 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Tue Aug 29 18:17:04 2023 +0200
@@ -169,7 +169,7 @@
     }
 
     for (page <- pages)
-      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize))
+      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalized))
   }
   set_content(group_tabs)