src/Pure/Tools/dump.scala

   object Session
   {
     def apply(
       options: Options,
       logic: String,
-      dump_checkpoints: Boolean = false,
       aspects: List[Aspect] = Nil,
       progress: Progress = No_Progress,
       log: Logger = No_Logger,
       dirs: List[Path] = Nil,
       select_dirs: List[Path] = Nil,
       selection: Sessions.Selection = Sessions.Selection.empty): Session =
     {
-      new Session(
-        options, logic, dump_checkpoints, aspects, progress, log, dirs, select_dirs, selection)
+      new Session(options, logic, aspects, progress, log, dirs, select_dirs, selection)
     }
   }
 
   class Session private(
     options: Options,
     logic: String,
-    dump_checkpoints: Boolean,
     aspects: List[Aspect],
     progress: Progress,
     log: Logger,
     dirs: List[Path],
     select_dirs: List[Path],

       try {
         val use_theories_result =
           session.use_theories(used_theories.map(_.theory),
             unicode_symbols = unicode_symbols,
             progress = progress,
-            checkpoints = if (dump_checkpoints) deps.dump_checkpoints else Set.empty,
             commit = Some(Consumer.apply _))
 
         val bad_theories = Consumer.shutdown()
         val bad_msgs =
           bad_theories.map(bad =>

   val default_output_dir: Path = Path.explode("dump")
 
   def dump(
     options: Options,
     logic: String,
-    dump_checkpoints: Boolean = false,
     aspects: List[Aspect] = Nil,
     progress: Progress = No_Progress,
     log: Logger = No_Logger,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
     selection: Sessions.Selection = Sessions.Selection.empty)
   {
     val session =
-      Session(options, logic, dump_checkpoints = dump_checkpoints, aspects = aspects,
-        progress = progress, log = log, dirs = dirs, select_dirs = select_dirs,
-        selection = selection)
+      Session(options, logic, aspects = aspects, progress = progress, log = log, dirs = dirs,
+        select_dirs = select_dirs, selection = selection)
 
     session.run((args: Args) =>
       {
         progress.echo("Processing theory " + args.print_node + " ...")
         val aspect_args =

     Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
     {
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
-      var dump_checkpoints = false
       var output_dir = default_output_dir
       var requirements = false
       var exclude_session_groups: List[String] = Nil
       var all_sessions = false
       var dirs: List[Path] = Nil

 Usage: isabelle dump [OPTIONS] [SESSIONS ...]
 
   Options are:
     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
-    -C           observe option dump_checkpoint for theories
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
     -R           operate on requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions

   Dump cumulative PIDE session database, with the following aspects:
 
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
-      "C" -> (_ => dump_checkpoints = true),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "O:" -> (arg => output_dir = Path.explode(arg)),
       "R" -> (_ => requirements = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),

 
       val progress = new Console_Progress(verbose = verbose)
 
       progress.interrupt_handler {
         dump(options, logic,
-          dump_checkpoints = dump_checkpoints,
           aspects = aspects,
           progress = progress,
           dirs = dirs,
           select_dirs = select_dirs,
           output_dir = output_dir,