src/Pure/Tools/dump.scala
changeset 68944 ce68b1488612
parent 68942 4709898282a6
child 68945 fa5d936daf1c
equal deleted inserted replaced
68943:e564605d4cac 68944:ce68b1488612
   219   Dump cumulative PIDE session database, with the following aspects:
   219   Dump cumulative PIDE session database, with the following aspects:
   220 
   220 
   221 """ + Library.prefix_lines("    ", show_aspects) + "\n",
   221 """ + Library.prefix_lines("    ", show_aspects) + "\n",
   222       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
   222       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
   223       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   223       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   224       "C:" -> (arg => commit_clean_delay = Time.seconds(Value.Double.parse(arg))),
   224       "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
   225       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   225       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   226       "O:" -> (arg => output_dir = Path.explode(arg)),
   226       "O:" -> (arg => output_dir = Path.explode(arg)),
   227       "R" -> (_ => requirements = true),
   227       "R" -> (_ => requirements = true),
   228       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   228       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   229       "a" -> (_ => all_sessions = true),
   229       "a" -> (_ => all_sessions = true),