src/Pure/Tools/process_theories.scala

Process theories within an adhoc session context.

/*  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


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,
    theories: List[String],
    files: List[Path] = Nil,
    dirs: List[Path] = 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 session_dir = Isabelle_System.make_directory(private_dir + Path.basic("session"))

      {
        var seen = Set.empty[JFile]
        for (path0 <- files) {
          val path = path0.canonical
          val file = path.file
          if (!seen(file)) {
            seen += file
            val target = session_dir + path.base
            if (target.is_file) {
              error("Duplicate session source file " + path.base + " --- from " + path)
            }
            Isabelle_System.copy_file(path, target)
          }
        }
      }

      /* 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 adhoc session */

      val session_entry =
        Sessions.Session_Entry(
          parent = Some(logic),
          theories = session_theories.map(a => (Nil, List(((a, Position.none), false)))),
          imports = session_imports)

      val session_info =
        Sessions.Info.make(session_entry, draft_session = true,
          dir = session_dir, options = options)

      Build.build(options, private_dir = Some(private_dir), progress = progress,
        infos = List(session_info), selection = Sessions.Selection.session(session_info.name))
    }
  }



  /** Isabelle tool wrapper **/

  val isabelle_tool = Isabelle_Tool("process_theories",
    "process theories within an adhoc session context",
    Scala_Project.here,
    { args =>
      val dirs = new mutable.ListBuffer[Path]
      val files = new mutable.ListBuffer[Path]
      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
      var options = Options.init()
      var verbose = false

      val getopts = Getopts("""
Usage: isabelle process_theories [OPTIONS] [THEORIES...]

  Options are:
    -F FILE      include addition session files, listed in FILE
    -d DIR       include session directory
    -f FILE      include addition session files
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    -v           verbose

  Process theories within an adhoc session context.
""",
        "F:" -> (arg => files ++= read_files(Path.explode(arg))),
        "d:" -> (arg => dirs += Path.explode(arg)),
        "f:" -> (arg => files += Path.explode(arg)),
        "l:" -> (arg => logic = 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, theories, files = files.toList, dirs = dirs.toList,
            progress = progress)
        }

      sys.exit(results.rc)
    })
}