diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala --- a/src/Pure/General/file.scala +++ b/src/Pure/General/file.scala @@ -1,355 +1,358 @@ /* Title: Pure/General/file.scala Author: Makarius File-system operations. */ package isabelle import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, File => JFile, IOException} import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath, Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException} import java.nio.file.attribute.BasicFileAttributes import java.net.{URL, MalformedURLException} import java.util.zip.{GZIPInputStream, GZIPOutputStream} import java.util.regex.Pattern import java.util.EnumSet import org.tukaani.xz.{XZInputStream, XZOutputStream} import scala.collection.mutable import scala.util.matching.Regex object File { /* standard path (Cygwin or Posix) */ def standard_path(path: Path): String = path.expand.implode def standard_path(platform_path: String): String = if (Platform.is_windows) { val Platform_Root = new Regex("(?i)" + Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""") val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") platform_path.replace('/', '\\') match { case Platform_Root(rest) => "/" + rest.replace('\\', '/') case Drive(letter, rest) => "/cygdrive/" + Word.lowercase(letter) + (if (rest == "") "" else "/" + rest.replace('\\', '/')) case path => path.replace('\\', '/') } } else platform_path def standard_path(file: JFile): String = standard_path(file.getPath) def standard_url(name: String): String = try { val url = new URL(name) if (url.getProtocol == "file" && Url.is_wellformed_file(name)) standard_path(Url.parse_file(name)) else name } catch { case _: MalformedURLException => standard_path(name) } /* platform path (Windows or Posix) */ private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") private val Named_Root = new Regex("//+([^/]*)(.*)") def platform_path(standard_path: String): String = if (Platform.is_windows) { val result_path = new StringBuilder val rest = standard_path match { case Cygdrive(drive, rest) => result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) rest case Named_Root(root, rest) => result_path ++= JFile.separator result_path ++= JFile.separator result_path ++= root rest case path if path.startsWith("/") => result_path ++= Isabelle_System.cygwin_root() path case path => path } for (p <- space_explode('/', rest) if p != "") { val len = result_path.length if (len > 0 && result_path(len - 1) != JFile.separatorChar) result_path += JFile.separatorChar result_path ++= p } result_path.toString } else standard_path def platform_path(path: Path): String = platform_path(standard_path(path)) def platform_file(path: Path): JFile = new JFile(platform_path(path)) /* platform files */ def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile def absolute_name(file: JFile): String = absolute(file).getPath def canonical(file: JFile): JFile = file.getCanonicalFile def canonical_name(file: JFile): String = canonical(file).getPath def path(file: JFile): Path = Path.explode(standard_path(file)) def pwd(): Path = path(Path.current.absolute_file) /* relative paths */ def relative_path(base: Path, other: Path): Option[Path] = { val base_path = base.file.toPath val other_path = other.file.toPath if (other_path.startsWith(base_path)) Some(path(base_path.relativize(other_path).toFile)) else None } /* bash path */ def bash_path(path: Path): String = Bash.string(standard_path(path)) def bash_path(file: JFile): String = Bash.string(standard_path(file)) /* directory entries */ def check_dir(path: Path): Path = if (path.is_dir) path else error("No such directory: " + path) def check_file(path: Path): Path = if (path.is_file) path else error("No such file: " + path) /* directory content */ def read_dir(dir: Path): List[String] = { if (!dir.is_dir) error("No such directory: " + dir.toString) val files = dir.file.listFiles if (files == null) Nil else files.toList.map(_.getName).sorted } def find_files( start: JFile, pred: JFile => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false): List[JFile] = { val result = new mutable.ListBuffer[JFile] def check(file: JFile) { if (pred(file)) result += file } if (start.isFile) check(start) else if (start.isDirectory) { val options = if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS) else EnumSet.noneOf(classOf[FileVisitOption]) Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE, new SimpleFileVisitor[JPath] { override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult = { if (include_dirs) check(path.toFile) FileVisitResult.CONTINUE } override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult = { val file = path.toFile if (include_dirs || !file.isDirectory) check(file) FileVisitResult.CONTINUE } } ) } result.toList } /* read */ def read(file: JFile): String = Bytes.read(file).text def read(path: Path): String = read(path.file) def read_stream(reader: BufferedReader): String = { val output = new StringBuilder(100) var c = -1 while ({ c = reader.read; c != -1 }) output += c.toChar reader.close output.toString } def read_stream(stream: InputStream): String = read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) def read_gzip(file: JFile): String = read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_gzip(path: Path): String = read_gzip(path.file) def read_xz(file: JFile): String = read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_xz(path: Path): String = read_xz(path.file) /* read lines */ def read_line(reader: BufferedReader): Option[String] = { val line = try { reader.readLine} catch { case _: IOException => null } if (line == null) None else Some(line) } def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] var line: Option[String] = None while ({ line = read_line(reader); line.isDefined }) { progress(line.get) result += line.get } reader.close result.toList } /* write */ + def writer(file: JFile): BufferedWriter = + new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset)) + def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream) { val stream = make_stream(new FileOutputStream(file)) using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text)) } def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s) def write(path: Path, text: CharSequence): Unit = write(path.file, text) def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit = File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options)) def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options()) def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit = write_xz(path.file, text, options) def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options()) def write_backup(path: Path, text: CharSequence) { if (path.is_file) move(path, path.backup) write(path, text) } def write_backup2(path: Path, text: CharSequence) { if (path.is_file) move(path, path.backup2) write(path, text) } /* append */ def append(file: JFile, text: CharSequence): Unit = Files.write(file.toPath, UTF8.bytes(text.toString), StandardOpenOption.APPEND, StandardOpenOption.CREATE) def append(path: Path, text: CharSequence): Unit = append(path.file, text) /* eq */ def eq(file1: JFile, file2: JFile): Boolean = try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) } catch { case ERROR(_) => false } def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) /* eq_content */ def eq_content(file1: JFile, file2: JFile): Boolean = if (eq(file1, file2)) true else if (file1.length != file2.length) false else Bytes.read(file1) == Bytes.read(file2) def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) /* copy */ def copy(src: JFile, dst: JFile) { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!eq(src, target)) Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) /* move */ def move(src: JFile, dst: JFile) { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file) /* symbolic link */ def link(src: Path, dst: Path, force: Boolean = false) { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => Cygwin.link(standard_path(src), target) case _: FileSystemException if Platform.is_windows => Cygwin.link(standard_path(src), target) } } /* permissions */ def is_executable(path: Path): Boolean = { if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok else path.file.canExecute } def set_executable(path: Path, flag: Boolean) { if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path) else if (Platform.is_windows) Isabelle_System.chmod("a-x", path) else path.file.setExecutable(flag, false) } } diff --git a/src/Pure/PIDE/yxml.scala b/src/Pure/PIDE/yxml.scala --- a/src/Pure/PIDE/yxml.scala +++ b/src/Pure/PIDE/yxml.scala @@ -1,147 +1,155 @@ /* Title: Pure/PIDE/yxml.scala Author: Makarius Efficient text representation of XML trees. Suitable for direct inlining into plain text. */ package isabelle import scala.collection.mutable object YXML { /* chunk markers */ val X = '\u0005' val Y = '\u0006' val is_X = (c: Char) => c == X val is_Y = (c: Char) => c == Y val X_string = X.toString val Y_string = Y.toString val XY_string = X_string + Y_string + val XYX_string = XY_string + X_string def detect(s: String): Boolean = s.exists(c => c == X || c == Y) def detect_elem(s: String): Boolean = s.startsWith(XY_string) /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?) + def traversal(string: String => Unit, body: XML.Body): Unit = + { + def tree(t: XML.Tree): Unit = + t match { + case XML.Elem(Markup(name, atts), ts) => + string(XY_string) + string(name) + for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) } + string(X_string) + ts.foreach(tree) + string(XYX_string) + case XML.Text(text) => string(text) + } + body.foreach(tree) + } + def string_of_body(body: XML.Body): String = { val s = new StringBuilder - def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 } - def tree(t: XML.Tree): Unit = - t match { - case XML.Elem(Markup(name, atts), ts) => - s += X; s += Y; s ++= name; atts.foreach(attrib); s += X - ts.foreach(tree) - s += X; s += Y; s += X - case XML.Text(text) => s ++= text - } - body.foreach(tree) + traversal(str => s ++= str, body) s.toString } def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) /* parsing */ private def err(msg: String) = error("Malformed YXML: " + msg) private def err_attribute() = err("bad attribute") private def err_element() = err("bad element") private def err_unbalanced(name: String) = if (name == "") err("unbalanced element") else err("unbalanced element " + quote(name)) private def parse_attrib(source: CharSequence) = { val s = source.toString val i = s.indexOf('=') if (i <= 0) err_attribute() (s.substring(0, i), s.substring(i + 1)) } def parse_body(source: CharSequence): XML.Body = { /* stack operations */ def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree] var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer())) def add(x: XML.Tree) { (stack: @unchecked) match { case ((_, body) :: _) => body += x } } def push(name: String, atts: XML.Attributes) { if (name == "") err_element() else stack = (Markup(name, atts), buffer()) :: stack } def pop() { (stack: @unchecked) match { case ((Markup.Empty, _) :: _) => err_unbalanced("") case ((markup, body) :: pending) => stack = pending add(XML.Elem(markup, body.toList)) } } /* parse chunks */ for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) { if (chunk.length == 1 && chunk.charAt(0) == Y) pop() else { Library.separated_chunks(is_Y, chunk).toList match { case ch :: name :: atts if ch.length == 0 => push(name.toString, atts.map(parse_attrib)) case txts => for (txt <- txts) add(XML.Text(txt.toString)) } } } (stack: @unchecked) match { case List((Markup.Empty, body)) => body.toList case (Markup(name, _), _) :: _ => err_unbalanced(name) } } def parse(source: CharSequence): XML.Tree = parse_body(source) match { case List(result) => result case Nil => XML.Text("") case _ => err("multiple XML trees") } def parse_elem(source: CharSequence): XML.Tree = parse_body(source) match { case List(elem: XML.Elem) => elem case _ => err("single XML element expected") } /* failsafe parsing */ private def markup_broken(source: CharSequence) = XML.Elem(Markup.Broken, List(XML.Text(source.toString))) def parse_body_failsafe(source: CharSequence): XML.Body = { try { parse_body(source) } catch { case ERROR(_) => List(markup_broken(source)) } } def parse_failsafe(source: CharSequence): XML.Tree = { try { parse(source) } catch { case ERROR(_) => markup_broken(source) } } } diff --git a/src/Pure/Tools/dump.scala b/src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala +++ b/src/Pure/Tools/dump.scala @@ -1,493 +1,499 @@ /* Title: Pure/Tools/dump.scala Author: Makarius Dump cumulative PIDE session database. */ package isabelle +import java.io.{BufferedWriter, FileOutputStream, OutputStreamWriter} + object Dump { /* aspects */ sealed case class Aspect_Args( options: Options, deps: Sessions.Deps, progress: Progress, output_dir: Path, snapshot: Document.Snapshot, status: Document_Status.Node_Status) { - def write(file_name: Path, bytes: Bytes) + def write_path(file_name: Path): Path = { val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name Isabelle_System.mkdirs(path.dir) - Bytes.write(path, bytes) + path } + def write(file_name: Path, bytes: Bytes): Unit = + Bytes.write(write_path(file_name), bytes) + def write(file_name: Path, text: String): Unit = write(file_name, Bytes(text)) def write(file_name: Path, body: XML.Body): Unit = - write(file_name, Symbol.encode(YXML.string_of_body(body))) + using(File.writer(write_path(file_name).file))( + 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) { override def toString: String = name } val known_aspects: List[Aspect] = List( Aspect("markup", "PIDE markup (YXML format)", { case args => args.write(Path.explode("markup.yxml"), args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full)) }), Aspect("messages", "output messages (YXML format)", { case args => args.write(Path.explode("messages.yxml"), args.snapshot.messages.iterator.map(_._1).toList) }), Aspect("latex", "generated LaTeX source", { case args => for (entry <- args.snapshot.exports if entry.name == "document.tex") args.write(Path.explode(entry.name), entry.uncompressed()) }, options = List("export_document")), Aspect("theory", "foundational theory content", { case args => for { entry <- args.snapshot.exports if entry.name.startsWith(Export_Theory.export_prefix) } args.write(Path.explode(entry.name), entry.uncompressed()) }, options = List("export_theory")) ).sortBy(_.name) def show_aspects: String = cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description)) def the_aspect(name: String): Aspect = known_aspects.find(aspect => aspect.name == name) getOrElse error("Unknown aspect " + quote(name)) /* context and session */ sealed case class Args( session: Headless.Session, snapshot: Document.Snapshot, status: Document_Status.Node_Status) { def print_node: String = snapshot.node_name.toString } object Context { def apply( options: Options, aspects: List[Aspect] = Nil, progress: Progress = No_Progress, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, selection: Sessions.Selection = Sessions.Selection.empty, pure_base: Boolean = false): Context = { val session_options: Options = { val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options val options1 = options0 + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0" + "editor_tracing_messages=0" + "editor_presentation" (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) } val sessions_structure: Sessions.Structure = Sessions.load_structure(session_options, dirs = dirs, select_dirs = select_dirs). selection(selection) { val selection_size = sessions_structure.build_graph.size if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...") } val deps: Sessions.Deps = Sessions.deps(sessions_structure, progress = progress).check_errors new Context(options, progress, dirs, select_dirs, pure_base, session_options, deps) } } class Context private( val options: Options, val progress: Progress, val dirs: List[Path], val select_dirs: List[Path], val pure_base: Boolean, val session_options: Options, val deps: Sessions.Deps) { context => def session_dirs: List[Path] = dirs ::: select_dirs def build_logic(logic: String) { 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] = { /* partitions */ def session_info(session_name: String): Sessions.Info = deps.sessions_structure(session_name) val session_graph = deps.sessions_structure.build_graph val all_sessions = session_graph.topological_order val afp_sessions = (for (name <- all_sessions if session_info(name).is_afp) yield name).toSet val afp_bulky_sessions = (for (name <- all_sessions if session_info(name).is_afp_bulky) yield name).toList val base_sessions = session_graph.all_preds(List(logic).filter(session_graph.defined)).reverse val proof_sessions = session_graph.all_succs( for (name <- all_sessions if session_info(name).record_proofs) yield name) /* resulting sessions */ def make_session( selected_sessions: List[String], session_logic: String = logic, strict: Boolean = false, record_proofs: Boolean = false): List[Session] = { if (selected_sessions.isEmpty && !strict) Nil else List(new Session(context, session_logic, log, selected_sessions, record_proofs)) } val PURE = isabelle.Thy_Header.PURE val base = if (logic == PURE && !pure_base) Nil else make_session(base_sessions, session_logic = PURE, strict = logic == PURE) val main = make_session( session_graph.topological_order.filterNot(name => afp_sessions.contains(name) || base_sessions.contains(name) || proof_sessions.contains(name))) val proofs = make_session(proof_sessions, session_logic = PURE, record_proofs = true) val afp = if (afp_sessions.isEmpty) Nil else { 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 graph.keys.partition(a => force_part1(a) || graph.is_isolated(a)) } List(part1, part2, afp_bulky_sessions).flatMap(make_session(_)) } proofs ::: base ::: main ::: afp } /* processed theories */ private val processed_theories = Synchronized(Set.empty[String]) def process_theory(theory: String): Boolean = processed_theories.change_result(processed => (!processed(theory), processed + theory)) /* errors */ private val errors = Synchronized(List.empty[String]) def add_errors(more_errs: List[String]) { errors.change(errs => errs ::: more_errs) } def check_errors { val errs = errors.value if (errs.nonEmpty) error(errs.mkString("\n\n")) } } class Session private[Dump]( val context: Context, val logic: String, log: Logger, selected_sessions: List[String], record_proofs: Boolean) { /* resources */ val options: Options = if (record_proofs) context.session_options + "record_proofs=2" else context.session_options private def deps = context.deps private def progress = context.progress val resources: Headless.Resources = Headless.Resources.make(options, logic, progress = progress, log = log, session_dirs = context.session_dirs, include_sessions = deps.sessions_structure.imports_topological_order) val used_theories: List[Document.Node.Name] = { for { session_name <- deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order (name, theory_options) <- deps(session_name).used_theories if !resources.session_base.loaded_theory(name.theory) if { def warn(msg: String): Unit = progress.echo_warning("Skipping theory " + name + " (" + msg + ")") val conditions = space_explode(',', theory_options.string("condition")). filter(cond => Isabelle_System.getenv(cond) == "") if (conditions.nonEmpty) { warn("undefined " + conditions.mkString(", ")) false } else if (options.bool("skip_proofs") && !theory_options.bool("skip_proofs")) { warn("option skip_proofs") false } else true } } yield name } /* process */ def process(process_theory: Args => Unit, unicode_symbols: Boolean = false) { val session = resources.start_session(progress = progress) // asynchronous consumer object Consumer { sealed case class Bad_Theory( name: Document.Node.Name, status: Document_Status.Node_Status, errors: List[String]) private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory]) private val consumer = Consumer_Thread.fork(name = "dump")( consume = (args: (Document.Snapshot, Document_Status.Node_Status)) => { val (snapshot, status) = args val name = snapshot.node_name if (status.ok) { try { if (context.process_theory(name.theory)) { process_theory(Args(session, snapshot, status)) } } catch { case exn: Throwable if !Exn.is_interrupt(exn) => val msg = Exn.message(exn) progress.echo("FAILED to process theory " + name) progress.echo_error_message(msg) consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _) } } else { val msgs = for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) yield { "Error" + Position.here(pos) + ":\n" + XML.content(Pretty.formatted(List(tree))) } progress.echo("FAILED to process theory " + name) msgs.foreach(progress.echo_error_message) consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _) } true }) def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit = consumer.send((snapshot, status)) def shutdown(): List[Bad_Theory] = { consumer.shutdown() consumer_bad_theories.value.reverse } } // synchronous body try { val use_theories_result = session.use_theories(used_theories.map(_.theory), unicode_symbols = unicode_symbols, progress = progress, commit = Some(Consumer.apply _)) val bad_theories = Consumer.shutdown() val bad_msgs = bad_theories.map(bad => Output.clean_yxml( "FAILED theory " + bad.name + (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") + (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", "")))) val pending_msgs = use_theories_result.nodes_pending match { case Nil => Nil case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString))) } context.add_errors(bad_msgs ::: pending_msgs) } finally { session.stop() } } } /* dump */ val default_output_dir: Path = Path.explode("dump") val default_logic: String = Thy_Header.PURE def dump( options: Options, logic: String, 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 context = Context(options, aspects = aspects, progress = progress, dirs = dirs, select_dirs = select_dirs, selection = selection) context.build_logic(logic) for (session <- context.sessions(logic = logic, log = log)) { session.process((args: Args) => { progress.echo("Processing theory " + args.print_node + " ...") val aspect_args = Aspect_Args(session.options, context.deps, progress, output_dir, args.snapshot, args.status) aspects.foreach(_.operation(aspect_args)) }) } context.check_errors } /* Isabelle tool wrapper */ val isabelle_tool = 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 output_dir = default_output_dir var requirements = false var exclude_session_groups: List[String] = Nil var all_sessions = false var logic = default_logic var dirs: List[Path] = Nil var session_groups: List[String] = Nil var options = Options.init() var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle dump [OPTIONS] [SESSIONS ...] Options are: -A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """) -B NAME include session NAME and all descendants -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 -b NAME base logic image (default """ + isabelle.quote(default_logic) + """) -d DIR include session directory -g NAME select session group NAME -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants 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)), "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), "b:" -> (arg => logic = arg), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val progress = new Console_Progress(verbose = verbose) progress.interrupt_handler { dump(options, logic, aspects = aspects, progress = progress, dirs = dirs, select_dirs = select_dirs, output_dir = output_dir, selection = Sessions.Selection( requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions)) } }) }