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