# HG changeset patch # User wenzelm # Date 1456677601 -3600 # Node ID 38c89353b3491a0ded70a534fee424c239c7ccd1 # Parent b93cc7d734313727aa55c8eed15cab23981382a2 tuned signature; diff -r b93cc7d73431 -r 38c89353b349 src/Pure/System/getopts.scala --- a/src/Pure/System/getopts.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/System/getopts.scala Sun Feb 28 17:40:01 2016 +0100 @@ -9,7 +9,7 @@ object Getopts { - def apply(usage_text: () => String, option_specs: (String, String => Unit)*): Getopts = + def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts = { val options = (Map.empty[Char, (Boolean, String => Unit)] /: option_specs) { @@ -25,11 +25,11 @@ } } -class Getopts private(usage_text: () => String, options: Map[Char, (Boolean, String => Unit)]) +class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)]) { def usage(): Nothing = { - Console.println(usage_text()) + Console.println(usage_text) sys.exit(1) } diff -r b93cc7d73431 -r 38c89353b349 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/System/options.scala Sun Feb 28 17:40:01 2016 +0100 @@ -150,7 +150,7 @@ var list_options = false var export_file = "" - val getopts = Getopts(() => """ + val getopts = Getopts(""" Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] Options are: diff -r b93cc7d73431 -r 38c89353b349 src/Pure/Tools/build_doc.scala --- a/src/Pure/Tools/build_doc.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/Tools/build_doc.scala Sun Feb 28 17:40:01 2016 +0100 @@ -77,7 +77,7 @@ var system_mode = false val getopts = - Getopts(() => """ + Getopts(""" Usage: isabelle build_doc [OPTIONS] [DOCS ...]" Options are: diff -r b93cc7d73431 -r 38c89353b349 src/Pure/Tools/check_sources.scala --- a/src/Pure/Tools/check_sources.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/Tools/check_sources.scala Sun Feb 28 17:40:01 2016 +0100 @@ -54,7 +54,7 @@ def main(args: Array[String]) { Command_Line.tool0 { - val getopts = Getopts(() => """ + val getopts = Getopts(""" Usage: isabelle check_sources [ROOT_DIRS...] Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS. diff -r b93cc7d73431 -r 38c89353b349 src/Pure/Tools/doc.scala --- a/src/Pure/Tools/doc.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/Tools/doc.scala Sun Feb 28 17:40:01 2016 +0100 @@ -96,7 +96,7 @@ def main(args: Array[String]) { Command_Line.tool0 { - val getopts = Getopts(() => """ + val getopts = Getopts(""" Usage: isabelle doc [DOC ...] View Isabelle documentation. diff -r b93cc7d73431 -r 38c89353b349 src/Pure/Tools/update_cartouches.scala --- a/src/Pure/Tools/update_cartouches.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/Tools/update_cartouches.scala Sun Feb 28 17:40:01 2016 +0100 @@ -90,7 +90,7 @@ var replace_comment = false var replace_text = false - val getopts = Getopts(() => """ + val getopts = Getopts(""" Usage: isabelle update_cartouches [FILES|DIRS...] Options are: diff -r b93cc7d73431 -r 38c89353b349 src/Pure/Tools/update_header.scala --- a/src/Pure/Tools/update_header.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/Tools/update_header.scala Sun Feb 28 17:40:01 2016 +0100 @@ -33,7 +33,7 @@ Command_Line.tool0 { var section = "section" - val getopts = Getopts(() => """ + val getopts = Getopts(""" Usage: isabelle update_header [FILES|DIRS...] Options are: diff -r b93cc7d73431 -r 38c89353b349 src/Pure/Tools/update_then.scala --- a/src/Pure/Tools/update_then.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/Tools/update_then.scala Sun Feb 28 17:40:01 2016 +0100 @@ -33,7 +33,7 @@ def main(args: Array[String]) { Command_Line.tool0 { - val getopts = Getopts(() => """ + val getopts = Getopts(""" Usage: isabelle update_then [FILES|DIRS...] Recursively find .thy files and expand old Isar command conflations: diff -r b93cc7d73431 -r 38c89353b349 src/Pure/Tools/update_theorems.scala --- a/src/Pure/Tools/update_theorems.scala Sun Feb 28 17:37:20 2016 +0100 +++ b/src/Pure/Tools/update_theorems.scala Sun Feb 28 17:40:01 2016 +0100 @@ -34,7 +34,7 @@ def main(args: Array[String]) { Command_Line.tool0 { - val getopts = Getopts(() => """ + val getopts = Getopts(""" Usage: isabelle update_theorems [FILES|DIRS...] Recursively find .thy files and update toplevel theorem keywords: