/* Title: Pure/Tools/process_theories.scala
Author: Makarius
Process theories within an adhoc session context.
*/
package isabelle
import java.io.{File => JFile}
import scala.collection.mutable
import scala.util.matching.Regex
object Process_Theories {
/** process theories **/
def read_files(path: Path): List[Path] =
Library.trim_split_lines(File.read(path)).map(Path.explode)
def process_theories(
options: Options,
logic: String,
directory: Option[Path] = None,
theories: List[String] = Nil,
files: List[Path] = Nil,
dirs: List[Path] = Nil,
output_messages: Boolean = false,
message_head: List[Regex] = Nil,
message_body: List[Regex] = Nil,
margin: Double = Pretty.default_margin,
breakgain: Double = Pretty.default_breakgain,
metric: Pretty.Metric = Symbol.Metric,
unicode_symbols: Boolean = false,
export_files: List[(String, Int, List[String])] = Nil,
progress: Progress = new Progress
): Build.Results = {
Isabelle_System.with_tmp_dir("private") { private_dir =>
/* options */
val build_engine = Build.Engine(Build.engine_name(options))
val build_options = build_engine.build_options(options)
/* session directory and files */
val private_prefix = private_dir.implode + "/"
val session_name = Sessions.DRAFT
val session_dir =
directory match {
case Some(dir) => dir.absolute
case None =>
val dir = Isabelle_System.make_directory(private_dir + Path.basic(session_name))
var seen = Set.empty[JFile]
for (path0 <- files) {
val path = path0.canonical
val file = path.file
if (!seen(file)) {
seen += file
val target = dir + path.base
if (target.is_file) {
error("Duplicate session source file " + path.base + " --- from " + path)
}
Isabelle_System.copy_file(path, target)
}
}
dir
}
/* session theories */
val more_theories =
for (path <- files; name <- Thy_Header.get_thy_name(path.implode))
yield name
val session_theories = theories ::: more_theories
/* session imports */
val sessions_structure = Sessions.load_structure(build_options, dirs = dirs)
val session_imports =
Set.from(
for {
name <- session_theories.iterator
session = sessions_structure.theory_qualifier(name)
if session.nonEmpty
} yield session).toList
/* build session */
Build.build_logic(options, logic, dirs = dirs, progress = progress,
build_heap = true, strict = true)
val session_entry =
Sessions.Session_Entry(
parent = Some(logic),
theories = session_theories.map(a => (Nil, List(((a, Position.none), false)))),
imports = session_imports,
export_files = export_files
.map({ case (a, b, c) => (Path.explode(a).absolute.implode, b, c) }))
val session_info =
Sessions.Info.make(session_entry, draft_session = true,
dir = session_dir, options = options)
def session_setup(setup_session_name: String, session: Session): Unit = {
if (output_messages && setup_session_name == session_name) {
def recode(s: String): String = Symbol.output(unicode_symbols, s)
session.all_messages += Session.Consumer[Prover.Message]("process_theories") {
case output: Prover.Output
if Protocol.is_exported(output.message) || Protocol.is_state(output.message) =>
output.properties match {
case Position.Line_File(line, file0) =>
val file = Library.perhaps_unprefix(private_prefix, file0)
val pos = Position.Line_File(line, file)
if (Build.print_log_check(pos, output.message, message_head, message_body)) {
progress.echo(Protocol.message_text(output.message, heading = true, pos = pos,
recode = recode, margin = margin, breakgain = breakgain, metric = metric))
}
case _ =>
}
case _ =>
}
}
}
Build.build(options, private_dir = Some(private_dir), dirs = dirs, progress = progress,
infos = List(session_info), selection = Sessions.Selection.session(session_name),
session_setup = session_setup,
export_files = export_files.nonEmpty)
}
}
/** Isabelle tool wrapper **/
val isabelle_tool = Isabelle_Tool("process_theories",
"process theories within an adhoc session context",
Scala_Project.here,
{ args =>
var directory: Option[Path] = None
val export_files = new mutable.ListBuffer[(String, Int, List[String])]
val message_head = new mutable.ListBuffer[Regex]
val message_body = new mutable.ListBuffer[Regex]
var output_messages = false
var unicode_symbols = false
val dirs = new mutable.ListBuffer[Path]
val files = new mutable.ListBuffer[Path]
var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var margin = Pretty.default_margin
var options = Options.init()
var verbose = false
val getopts = Getopts("""
Usage: isabelle process_theories [OPTIONS] [THEORIES...]
Options are:
-D DIR explicit session directory (default: private)
-E EXPORTS write session export artifacts to file-system
-F FILE include additional session files, listed in FILE
-H REGEX filter messages by matching against head
-M REGEX filter messages by matching against body
-O output messages
-U output Unicode symbols
-d DIR include session directory
-f FILE include additional session file
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-m MARGIN margin for pretty printing (default: """ + margin + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
Process theories within an adhoc session context.
""",
"D:" -> (arg => directory = Some(Path.explode(arg))),
"E:" -> (arg => export_files += Sessions.parse_exports(arg)),
"F:" -> (arg => files ++= read_files(Path.explode(arg))),
"H:" -> (arg => message_head += arg.r),
"M:" -> (arg => message_body += arg.r),
"O" -> (_ => output_messages = true),
"U" -> (_ => unicode_symbols = true),
"d:" -> (arg => dirs += Path.explode(arg)),
"f:" -> (arg => files += Path.explode(arg)),
"l:" -> (arg => logic = arg),
"m:" -> (arg => margin = Value.Double.parse(arg)),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true))
val theories = getopts(args)
val progress = new Console_Progress(verbose = verbose)
val results =
progress.interrupt_handler {
process_theories(options, logic, directory = directory, theories = theories,
files = files.toList, dirs = dirs.toList, output_messages = output_messages,
message_head = message_head.toList, message_body = message_body.toList,
margin = margin, unicode_symbols = unicode_symbols, export_files = export_files.toList,
progress = progress)
}
sys.exit(results.rc)
})
}