src/Pure/Tools/dump.scala
author wenzelm
Mon Jun 11 15:50:28 2018 +0200 (12 months ago)
changeset 68416 33114721ac9a
parent 68365 f9379279f98c
child 68491 f0f83ce0badd
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Tools/dump.scala
     2     Author:     Makarius
     3 
     4 Dump cumulative PIDE session database.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Dump
    11 {
    12   /* aspects */
    13 
    14   sealed case class Aspect_Args(
    15     options: Options,
    16     progress: Progress,
    17     deps: Sessions.Deps,
    18     output_dir: Path,
    19     node_name: Document.Node.Name,
    20     node_status: Protocol.Node_Status,
    21     snapshot: Document.Snapshot)
    22   {
    23     def write(file_name: Path, bytes: Bytes)
    24     {
    25       val path = output_dir + Path.basic(node_name.theory) + file_name
    26       Isabelle_System.mkdirs(path.dir)
    27       Bytes.write(path, bytes)
    28     }
    29 
    30     def write(file_name: Path, text: String): Unit =
    31       write(file_name, Bytes(text))
    32 
    33     def write(file_name: Path, body: XML.Body): Unit =
    34       write(file_name, Symbol.encode(YXML.string_of_body(body)))
    35   }
    36 
    37   sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
    38     options: List[String] = Nil)
    39   {
    40     override def toString: String = name
    41   }
    42 
    43   val known_aspects =
    44     List(
    45       Aspect("markup", "PIDE markup (YXML format)",
    46         { case args =>
    47             args.write(Path.explode("markup.yxml"),
    48               args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
    49         }),
    50       Aspect("messages", "output messages (YXML format)",
    51         { case args =>
    52             args.write(Path.explode("messages.yxml"),
    53               args.snapshot.messages.iterator.map(_._1).toList)
    54         }),
    55       Aspect("latex", "generated LaTeX source",
    56         { case args =>
    57             for (entry <- args.snapshot.exports if entry.name == "document.tex")
    58               args.write(Path.explode(entry.name), entry.uncompressed())
    59         }, options = List("editor_presentation")),
    60       Aspect("theory", "foundational theory content",
    61         { case args =>
    62             for {
    63               entry <- args.snapshot.exports
    64               if entry.name.startsWith(Export_Theory.export_prefix)
    65             } args.write(Path.explode(entry.name), entry.uncompressed())
    66         }, options = List("editor_presentation", "export_theory"))
    67     ).sortBy(_.name)
    68 
    69   def show_aspects: String =
    70     cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
    71 
    72   def the_aspect(name: String): Aspect =
    73     known_aspects.find(aspect => aspect.name == name) getOrElse
    74       error("Unknown aspect " + quote(name))
    75 
    76 
    77   /* dump */
    78 
    79   val default_output_dir = Path.explode("dump")
    80 
    81   def make_options(options: Options, aspects: List[Aspect]): Options =
    82     (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
    83       { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
    84 
    85   def dump(options: Options, logic: String,
    86     aspects: List[Aspect] = Nil,
    87     progress: Progress = No_Progress,
    88     log: Logger = No_Logger,
    89     dirs: List[Path] = Nil,
    90     select_dirs: List[Path] = Nil,
    91     output_dir: Path = default_output_dir,
    92     verbose: Boolean = false,
    93     system_mode: Boolean = false,
    94     selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    95   {
    96     if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
    97       system_mode = system_mode) != 0) error(logic + " FAILED")
    98 
    99     val dump_options = make_options(options, aspects)
   100 
   101 
   102     /* dependencies */
   103 
   104     val deps =
   105       Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
   106         selection_deps(selection)
   107 
   108     val include_sessions =
   109       deps.sessions_structure.imports_topological_order
   110 
   111     val use_theories =
   112       deps.sessions_structure.build_topological_order.
   113         flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
   114 
   115 
   116     /* session */
   117 
   118     val session =
   119       Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
   120         include_sessions = include_sessions, progress = progress, log = log)
   121 
   122     val theories_result = session.use_theories(use_theories, progress = progress)
   123     val session_result = session.stop()
   124 
   125 
   126     /* dump aspects */
   127 
   128     for ((node_name, node_status) <- theories_result.nodes) {
   129       val snapshot = theories_result.snapshot(node_name)
   130       val aspect_args =
   131         Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot)
   132       aspects.foreach(_.operation(aspect_args))
   133     }
   134 
   135     session_result
   136   }
   137 
   138 
   139   /* Isabelle tool wrapper */
   140 
   141   val isabelle_tool =
   142     Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
   143     {
   144       var aspects: List[Aspect] = known_aspects
   145       var base_sessions: List[String] = Nil
   146       var select_dirs: List[Path] = Nil
   147       var output_dir = default_output_dir
   148       var requirements = false
   149       var exclude_session_groups: List[String] = Nil
   150       var all_sessions = false
   151       var dirs: List[Path] = Nil
   152       var session_groups: List[String] = Nil
   153       var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
   154       var options = Options.init()
   155       var system_mode = false
   156       var verbose = false
   157       var exclude_sessions: List[String] = Nil
   158 
   159       val getopts = Getopts("""
   160 Usage: isabelle dump [OPTIONS] [SESSIONS ...]
   161 
   162   Options are:
   163     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
   164     -B NAME      include session NAME and all descendants
   165     -D DIR       include session directory and select its sessions
   166     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
   167     -R           operate on requirements of selected sessions
   168     -X NAME      exclude sessions from group NAME and all descendants
   169     -a           select all sessions
   170     -d DIR       include session directory
   171     -g NAME      select session group NAME
   172     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   173     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   174     -s           system build mode for logic image
   175     -v           verbose
   176     -x NAME      exclude session NAME and all descendants
   177 
   178   Dump cumulative PIDE session database, with the following aspects:
   179 
   180 """ + Library.prefix_lines("    ", show_aspects) + "\n",
   181       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
   182       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   183       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   184       "O:" -> (arg => output_dir = Path.explode(arg)),
   185       "R" -> (_ => requirements = true),
   186       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   187       "a" -> (_ => all_sessions = true),
   188       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   189       "l:" -> (arg => logic = arg),
   190       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   191       "o:" -> (arg => options = options + arg),
   192       "s" -> (_ => system_mode = true),
   193       "v" -> (_ => verbose = true),
   194       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   195 
   196       val sessions = getopts(args)
   197 
   198       val progress = new Console_Progress(verbose = verbose)
   199 
   200       val result =
   201         progress.interrupt_handler {
   202           dump(options, logic,
   203             aspects = aspects,
   204             progress = progress,
   205             dirs = dirs,
   206             select_dirs = select_dirs,
   207             output_dir = output_dir,
   208             verbose = verbose,
   209             selection = Sessions.Selection(
   210               requirements = requirements,
   211               all_sessions = all_sessions,
   212               base_sessions = base_sessions,
   213               exclude_session_groups = exclude_session_groups,
   214               exclude_sessions = exclude_sessions,
   215               session_groups = session_groups,
   216               sessions = sessions))
   217         }
   218 
   219       progress.echo(result.timing.message_resources)
   220 
   221       sys.exit(result.rc)
   222     })
   223 }