# HG changeset patch
# User wenzelm
# Date 1401103756 -7200
# Node ID 16536c15d749bc07c3e1295a9b46315dadfd6334
# Parent  db7c735e963df104612981fd30740e022ecabbc8
capitalize even more carefully (see 5ac67041ccf8), e.g. relevant for option "z3_non_commercial" and prospective "MaSh";

diff -r db7c735e963d -r 16536c15d749 src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Sun May 25 17:08:46 2014 +0200
+++ b/src/Pure/General/word.scala	Mon May 26 13:29:16 2014 +0200
@@ -43,10 +43,9 @@
     }
 
   def perhaps_capitalize(str: String): String =
-    str match {
-      case Case(c) if c != Lowercase => str
-      case _ => capitalize(str)
-    }
+    if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
+      capitalize(str)
+    else str
 
   sealed abstract class Case
   case object Lowercase extends Case