# HG changeset patch
# User wenzelm
# Date 1397724850 -7200
# Node ID 5ac67041ccf8ba5da7ac5111d501944ef984af05
# Parent  8e3c848008fa1cb03072898b04e30dcd6fcf815d
capitalize more carefully, e.g. relevant for option "ML_exception_trace";

diff -r 8e3c848008fa -r 5ac67041ccf8 src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Wed Apr 16 21:51:41 2014 +0200
+++ b/src/Pure/General/word.scala	Thu Apr 17 10:54:10 2014 +0200
@@ -40,6 +40,12 @@
       uppercase(str.substring(0, n)) + lowercase(str.substring(n))
     }
 
+  def perhaps_capitalize(str: String): String =
+    str match {
+      case Case(c) if c != Lowercase => str
+      case _ => capitalize(str)
+    }
+
   sealed abstract class Case
   case object Lowercase extends Case
   case object Uppercase extends Case
diff -r 8e3c848008fa -r 5ac67041ccf8 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Apr 16 21:51:41 2014 +0200
+++ b/src/Pure/System/options.scala	Thu Apr 17 10:54:10 2014 +0200
@@ -58,7 +58,7 @@
           case word :: rest if word == strip => rest
           case _ => words
         }
-      Word.implode(words1.map(Word.capitalize(_)))
+      Word.implode(words1.map(Word.perhaps_capitalize(_)))
     }
 
     def unknown: Boolean = typ == Unknown
diff -r 8e3c848008fa -r 5ac67041ccf8 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 16 21:51:41 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Apr 17 10:54:10 2014 +0200
@@ -201,7 +201,7 @@
     for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
       line match {
         case Heading1(s) =>
-          data.root.add(make_node(Word.capitalize(s), offset, offset + line.length))
+          data.root.add(make_node(Word.perhaps_capitalize(s), offset, offset + line.length))
         case Heading2(s) =>
           data.root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
             .add(make_node(s, offset, offset + line.length))
diff -r 8e3c848008fa -r 5ac67041ccf8 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Apr 16 21:51:41 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Thu Apr 17 10:54:10 2014 +0200
@@ -85,7 +85,8 @@
         }
       reactions += { case ValueChanged(`search`) => delay_search.invoke() }
     }, "Search Symbols")
-    pages.map(p => p.title = Word.implode(Word.explode('_', p.title).map(Word.capitalize(_))))
+    pages.map(p =>
+      p.title = Word.implode(Word.explode('_', p.title).map(Word.perhaps_capitalize(_))))
   }
   set_content(group_tabs)
 }