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