1/*  Title:      Pure/Tools/dump.scala
2    Author:     Makarius
3
4Dump cumulative PIDE session database.
5*/
6
7package isabelle
8
9
10object 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", "export_document")),
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, build_heap = true, progress = progress,
97      dirs = dirs ::: select_dirs, 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 ::: select_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    if (theories_result.ok) session_result
136    else {
137      for {
138        (name, status) <- theories_result.nodes if !status.ok
139        (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
140      } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
141
142      session_result.copy(rc = session_result.rc max 1)
143    }
144  }
145
146
147  /* Isabelle tool wrapper */
148
149  val isabelle_tool =
150    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
151    {
152      var aspects: List[Aspect] = known_aspects
153      var base_sessions: List[String] = Nil
154      var select_dirs: List[Path] = Nil
155      var output_dir = default_output_dir
156      var requirements = false
157      var exclude_session_groups: List[String] = Nil
158      var all_sessions = false
159      var dirs: List[Path] = Nil
160      var session_groups: List[String] = Nil
161      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
162      var options = Options.init()
163      var system_mode = false
164      var verbose = false
165      var exclude_sessions: List[String] = Nil
166
167      val getopts = Getopts("""
168Usage: isabelle dump [OPTIONS] [SESSIONS ...]
169
170  Options are:
171    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
172    -B NAME      include session NAME and all descendants
173    -D DIR       include session directory and select its sessions
174    -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
175    -R           operate on requirements of selected sessions
176    -X NAME      exclude sessions from group NAME and all descendants
177    -a           select all sessions
178    -d DIR       include session directory
179    -g NAME      select session group NAME
180    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
181    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
182    -s           system build mode for logic image
183    -v           verbose
184    -x NAME      exclude session NAME and all descendants
185
186  Dump cumulative PIDE session database, with the following aspects:
187
188""" + Library.prefix_lines("    ", show_aspects) + "\n",
189      "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
190      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
191      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
192      "O:" -> (arg => output_dir = Path.explode(arg)),
193      "R" -> (_ => requirements = true),
194      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
195      "a" -> (_ => all_sessions = true),
196      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
197      "l:" -> (arg => logic = arg),
198      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
199      "o:" -> (arg => options = options + arg),
200      "s" -> (_ => system_mode = true),
201      "v" -> (_ => verbose = true),
202      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
203
204      val sessions = getopts(args)
205
206      val progress = new Console_Progress(verbose = verbose)
207
208      val result =
209        progress.interrupt_handler {
210          dump(options, logic,
211            aspects = aspects,
212            progress = progress,
213            dirs = dirs,
214            select_dirs = select_dirs,
215            output_dir = output_dir,
216            verbose = verbose,
217            selection = Sessions.Selection(
218              requirements = requirements,
219              all_sessions = all_sessions,
220              base_sessions = base_sessions,
221              exclude_session_groups = exclude_session_groups,
222              exclude_sessions = exclude_sessions,
223              session_groups = session_groups,
224              sessions = sessions))
225        }
226
227      progress.echo(result.timing.message_resources)
228
229      sys.exit(result.rc)
230    })
231}
232