clarified default: all aspects;
authorwenzelm
Fri Jun 01 11:10:22 2018 +0200 (14 months ago)
changeset 683455bc1e1ac7955
parent 68344 3bb44c25ce8b
child 68346 b44010800a19
clarified default: all aspects;
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Fri Jun 01 10:56:01 2018 +0200
     1.2 +++ b/src/Pure/Tools/dump.scala	Fri Jun 01 11:10:22 2018 +0200
     1.3 @@ -29,6 +29,9 @@
     1.4    }
     1.5  
     1.6    sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit)
     1.7 +  {
     1.8 +    override def toString: String = name
     1.9 +  }
    1.10  
    1.11    private val known_aspects =
    1.12      List(
    1.13 @@ -45,10 +48,10 @@
    1.14                args.write(node_name, "markup.yxml", args.result.markup_to_XML(node_name))
    1.15              }
    1.16          })
    1.17 -    )
    1.18 +    ).sortBy(_.name)
    1.19  
    1.20    def show_aspects: String =
    1.21 -    cat_lines(known_aspects.sortBy(_.name).map(aspect => aspect.name + " - " + aspect.description))
    1.22 +    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
    1.23  
    1.24    def the_aspect(name: String): Aspect =
    1.25      known_aspects.find(aspect => aspect.name == name) getOrElse
    1.26 @@ -114,7 +117,7 @@
    1.27    val isabelle_tool =
    1.28      Isabelle_Tool("dump", "dump build database produced by PIDE session.", args =>
    1.29      {
    1.30 -      var aspects: List[Aspect] = Nil
    1.31 +      var aspects: List[Aspect] = known_aspects
    1.32        var base_sessions: List[String] = Nil
    1.33        var select_dirs: List[Path] = Nil
    1.34        var output_dir = default_output_dir
    1.35 @@ -133,7 +136,7 @@
    1.36  Usage: isabelle dump [OPTIONS] [SESSIONS ...]
    1.37  
    1.38    Options are:
    1.39 -    -A NAMES     dump named aspects (comma-separated list, see below)
    1.40 +    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
    1.41      -B NAME      include session NAME and all descendants
    1.42      -D DIR       include session directory and select its sessions
    1.43      -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
    1.44 @@ -149,7 +152,7 @@
    1.45      -x NAME      exclude session NAME and all descendants
    1.46  
    1.47    Dump build database produced by PIDE session. The following dump aspects
    1.48 -  are known (option -A):
    1.49 +  are available:
    1.50  
    1.51  """ + Library.prefix_lines("    ", show_aspects) + "\n",
    1.52        "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),