--- a/src/Pure/Tools/dump.scala Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/Tools/dump.scala Fri Apr 01 17:06:10 2022 +0200
@@ -9,8 +9,7 @@
import java.io.{BufferedWriter, FileOutputStream, OutputStreamWriter}
-object Dump
-{
+object Dump {
/* aspects */
sealed case class Aspect_Args(
@@ -19,10 +18,9 @@
progress: Progress,
output_dir: Path,
snapshot: Document.Snapshot,
- status: Document_Status.Node_Status)
- {
- def write_path(file_name: Path): Path =
- {
+ status: Document_Status.Node_Status
+ ) {
+ def write_path(file_name: Path): Path = {
val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
Isabelle_System.make_directory(path.dir)
path
@@ -39,9 +37,12 @@
writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body))
}
- sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
- options: List[String] = Nil)
- {
+ sealed case class Aspect(
+ name: String,
+ description: String,
+ operation: Aspect_Args => Unit,
+ options: List[String] = Nil
+ ) {
override def toString: String = name
}
@@ -79,13 +80,12 @@
sealed case class Args(
session: Headless.Session,
snapshot: Document.Snapshot,
- status: Document_Status.Node_Status)
- {
+ status: Document_Status.Node_Status
+ ) {
def print_node: String = snapshot.node_name.toString
}
- object Context
- {
+ object Context {
def apply(
options: Options,
aspects: List[Aspect] = Nil,
@@ -94,10 +94,9 @@
select_dirs: List[Path] = Nil,
selection: Sessions.Selection = Sessions.Selection.empty,
pure_base: Boolean = false,
- skip_base: Boolean = false): Context =
- {
- val session_options: Options =
- {
+ skip_base: Boolean = false
+ ): Context = {
+ val session_options: Options = {
val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
val options1 =
options0 +
@@ -132,22 +131,21 @@
val pure_base: Boolean,
val skip_base: Boolean,
val session_options: Options,
- val deps: Sessions.Deps)
- {
+ val deps: Sessions.Deps
+ ) {
context =>
def session_dirs: List[Path] = dirs ::: select_dirs
- def build_logic(logic: String): Unit =
- {
+ def build_logic(logic: String): Unit = {
Build.build_logic(options, logic, build_heap = true, progress = progress,
dirs = session_dirs, strict = true)
}
def sessions(
logic: String = default_logic,
- log: Logger = No_Logger): List[Session] =
- {
+ log: Logger = No_Logger
+ ): List[Session] = {
/* partitions */
def session_info(session_name: String): Sessions.Info =
@@ -176,8 +174,8 @@
selected_sessions: List[String],
session_logic: String = logic,
strict: Boolean = false,
- record_proofs: Boolean = false): List[Session] =
- {
+ record_proofs: Boolean = false
+ ): List[Session] = {
if (selected_sessions.isEmpty && !strict) Nil
else List(new Session(context, session_logic, log, selected_sessions, record_proofs))
}
@@ -200,8 +198,7 @@
val afp =
if (afp_sessions.isEmpty) Nil
else {
- val (part1, part2) =
- {
+ val (part1, part2) = {
val graph = session_graph.restrict(afp_sessions -- afp_bulky_sessions)
val force_partition1 = AFP.force_partition1.filter(graph.defined)
val force_part1 = graph.all_preds(graph.all_succs(force_partition1)).toSet
@@ -226,13 +223,11 @@
private val errors = Synchronized(List.empty[String])
- def add_errors(more_errs: List[String]): Unit =
- {
+ def add_errors(more_errs: List[String]): Unit = {
errors.change(errs => errs ::: more_errs)
}
- def check_errors: Unit =
- {
+ def check_errors: Unit = {
val errs = errors.value
if (errs.nonEmpty) error(errs.mkString("\n\n"))
}
@@ -243,8 +238,8 @@
val logic: String,
log: Logger,
selected_sessions: List[String],
- record_proofs: Boolean)
- {
+ record_proofs: Boolean
+ ) {
/* resources */
val options: Options =
@@ -259,8 +254,7 @@
session_dirs = context.session_dirs,
include_sessions = deps.sessions_structure.imports_topological_order)
- val used_theories: List[Document.Node.Name] =
- {
+ val used_theories: List[Document.Node.Name] = {
for {
session_name <-
deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order
@@ -289,15 +283,13 @@
/* process */
- def process(process_theory: Args => Unit, unicode_symbols: Boolean = false): Unit =
- {
+ def process(process_theory: Args => Unit, unicode_symbols: Boolean = false): Unit = {
val session = resources.start_session(progress = progress)
// asynchronous consumer
- object Consumer
- {
+ object Consumer {
sealed case class Bad_Theory(
name: Document.Node.Name,
status: Document_Status.Node_Status,
@@ -307,8 +299,7 @@
private val consumer =
Consumer_Thread.fork(name = "dump")(
- consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
- {
+ consume = (args: (Document.Snapshot, Document_Status.Node_Status)) => {
val (snapshot, status) = args
val name = snapshot.node_name
if (status.ok) {
@@ -342,8 +333,7 @@
def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
consumer.send((snapshot, status))
- def shutdown(): List[Bad_Theory] =
- {
+ def shutdown(): List[Bad_Theory] = {
consumer.shutdown()
consumer_bad_theories.value.reverse
}
@@ -394,8 +384,8 @@
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
output_dir: Path = default_output_dir,
- selection: Sessions.Selection = Sessions.Selection.empty): Unit =
- {
+ selection: Sessions.Selection = Sessions.Selection.empty
+ ): Unit = {
val context =
Context(options, aspects = aspects, progress = progress, dirs = dirs,
select_dirs = select_dirs, selection = selection)
@@ -403,8 +393,7 @@
context.build_logic(logic)
for (session <- context.sessions(logic = logic, log = log)) {
- session.process((args: Args) =>
- {
+ session.process((args: Args) => {
progress.echo("Processing theory " + args.print_node + " ...")
val aspect_args =
Aspect_Args(session.options, context.deps, progress, output_dir,
@@ -420,8 +409,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("dump", "dump cumulative PIDE session database", Scala_Project.here, args =>
- {
+ Isabelle_Tool("dump", "dump cumulative PIDE session database", Scala_Project.here,
+ args => {
var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil