capitalize more carefully, e.g. relevant for option "ML_exception_trace";

--- 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

--- 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

--- 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))

--- 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)
 }