# HG changeset patch
# User wenzelm
# Date 1383061945 -3600
# Node ID d5589530f3ba0373d5e0e8f4be7dba8b85707d1c
# Parent  a3c59f04346f066f5ccac6c1c46560a610b61fa8
clarified isabelle options -l;

diff -r a3c59f04346f -r d5589530f3ba src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Oct 29 15:34:29 2013 +0100
+++ b/src/Doc/System/Sessions.thy	Tue Oct 29 16:52:25 2013 +0100
@@ -249,6 +249,8 @@
   \secref{sec:tool-build}.
 
   Option @{verbatim "-g"} prints the value of the given option.
+  Option @{verbatim "-l"} lists all options with their declaration and
+  current value.
 
   Option @{verbatim "-x"} specifies a file to export the result in
   YXML format, instead of printing it in human-readable form.
diff -r a3c59f04346f -r d5589530f3ba src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Oct 29 15:34:29 2013 +0100
+++ b/src/Pure/System/options.scala	Tue Oct 29 16:52:25 2013 +0100
@@ -162,7 +162,10 @@
 {
   override def toString: String = options.iterator.mkString("Options (", ",", ")")
 
-  def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
+  private def print_opt(opt: Options.Opt): String =
+    if (opt.public) "public " + opt.print else opt.print
+
+  def print: String = cat_lines(options.toList.sortBy(_._1).map(p => print_opt(p._2)))
 
   def description(name: String): String = check_name(name).description