diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,562 +1,562 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Miscellaneous Isabelle system operations. */ package isabelle import java.util.{Map => JMap, HashMap} import java.util.zip.ZipFile import java.io.{File => JFile, IOException} import java.net.ServerSocket import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes import scala.jdk.CollectionConverters._ object Isabelle_System { /* settings environment */ def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = { val env0 = isabelle.setup.Environment.settings() if (putenv.isEmpty) env0 else { val env = new HashMap(env0) for ((a, b) <- putenv) env.put(a, b) env } } def getenv(name: String, env: JMap[String, String] = settings()): String = Option(env.get(name)).getOrElse("") def getenv_strict(name: String, env: JMap[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) /* services */ type Service = Classpath.Service @volatile private var _classpath: Option[Classpath] = None def classpath(): Classpath = { if (_classpath.isEmpty) init() // unsynchronized check _classpath.get } def make_services[C](c: Class[C]): List[C] = classpath().make_services(c) /* init settings + classpath */ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = { isabelle.setup.Environment.init(isabelle_root, cygwin_root) synchronized { if (_classpath.isEmpty) _classpath = Some(Classpath()) } } /* getetc -- static distribution parameters */ def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = { val path = root + Path.basic("etc") + Path.basic(name) if (path.is_file) { Library.trim_split_lines(File.read(path)) match { case Nil => None case List(s) => Some(s) case _ => error("Single line expected in " + path.absolute) } } else None } /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) orElse Mercurial.id_repository(root, rev = "") getOrElse error("Failed to identify Isabelle distribution " + root.expand) object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here def apply(arg: String): String = isabelle_id() } def isabelle_tags(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse { if (Mercurial.is_repository(root)) { val hg = Mercurial.repository(root) hg.tags(rev = hg.parent()) } else "" } def export_isabelle_identifier(isabelle_identifier: String): String = "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = isabelle_identifier() match { case None => "" case Some(version) => " (" + version + ")" } def isabelle_name(): String = getenv_strict("ISABELLE_NAME") def identification(): String = "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading() /** file-system operations **/ /* scala functions */ private def apply_paths( args: List[String], fun: PartialFunction[List[Path], Unit] ): List[String] = { fun(args.map(Path.explode)) Nil } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = apply_paths(args, { case List(path) => fun(path) }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.java_path) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path, direct: Boolean = false): Unit = { def make_path(dir: Path): String = { val s = File.standard_path(dir.absolute) if (direct) Url.direct_path(s) else s } val p1 = make_path(dir1) val p2 = make_path(dir2) make_directory(if (direct) dir2.absolute else dir2.absolute.dir) val res = bash("cp -a " + Bash.string(p1) + " " + Bash.string(p2)) if (!res.ok) cat_error("Failed to copy " + quote(p1) + " to " + quote(p2), res.err) } def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = { new_directory(dir2) try { copy_dir(dir1, dir2, direct = true); body } finally { rm_tree(dir2) } } object Make_Directory extends Scala.Fun_Strings("make_directory") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, make_directory) } object Copy_Dir extends Scala.Fun_Strings("copy_dir") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir(_, _)) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed to copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) { error("Illegal path specification " + src1 + " beyond base directory " + base_dir.absolute) } copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun_Strings("copy_file") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_file) } object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit = { 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 def cygwin_link(): Unit = { if (native) { error("Failed to create native symlink on Windows: " + quote(src_file.toString) + "\n(but it could work as Administrator)") } else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target) } try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => cygwin_link() case _: FileSystemException if Platform.is_windows => cygwin_link() } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file( name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix(), initialized: Boolean = true ): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile if (initialized) file.deleteOnExit() else file.delete() file } def with_tmp_file[A]( name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix() )(body: Path => A): A = { val file = tmp_file(name, ext, base_dir = base_dir) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun_Strings("rm_tree") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit() dir } def with_tmp_dir[A]( name: String, base_dir: JFile = isabelle_tmp_prefix() )(body: Path => A): A = { val dir = tmp_dir(name, base_dir = base_dir) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /* TCP/IP ports */ def local_port(): Int = { val socket = new ServerSocket(0) val port = socket.getLocalPort socket.close() port } /* JVM shutdown hook */ def create_shutdown_hook(body: => Unit): Thread = { val shutdown_hook = Isabelle_Thread.create(new Runnable { def run: Unit = body }) try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } shutdown_hook } def remove_shutdown_hook(shutdown_hook: Thread): Unit = try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } /** external processes **/ /* GNU bash */ def bash(script: String, description: String = "", cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false, input: String = "", progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => () ): Process_Result = { Bash.process(script, description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } /* command-line tools */ def require_command(cmd: String, test: String = "--version"): Unit = { if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd)) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, strip: Boolean = false, redirect: Boolean = false ): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") + (if (!strip) "" else "--strip-components=1 ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def extract(archive: Path, dir: Path, strip: Boolean = false): Unit = { val name = archive.file_name make_directory(dir) if (File.is_zip(name) || File.is_jar(name)) { using(new ZipFile(archive.file)) { zip_file => val items = for (entry <- zip_file.entries().asScala.toList) yield { val input = JPath.of(entry.getName) val count = input.getNameCount val output = if (strip && count <= 1) None else if (strip) Some(input.subpath(1, count)) else Some(input) val result = output.map(dir.java_path.resolve(_)) for (res <- result) { if (entry.isDirectory) Files.createDirectories(res) else { val bytes = using(zip_file.getInputStream(entry))(Bytes.read_stream(_)) Files.createDirectories(res.getParent) Files.write(res, bytes.array) } } (entry, result) } for { (entry, Some(res)) <- items if !entry.isDirectory t <- Option(entry.getLastModifiedTime) } Files.setLastModifiedTime(res, t) } } else if (File.is_tar_bz2(name) || File.is_tgz(name) || File.is_tar_gz(name)) { val flags = if (File.is_tar_bz2(name)) "-xjf " else "-xzf " Isabelle_System.gnutar(flags + File.bash_path(archive), dir = dir, strip = strip).check } else error("Cannot extract " + archive) } def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { with_tmp_file("patch") { patch => Isabelle_System.bash( "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(patch), cwd = base_dir.file).check_rc(_ <= 1) File.read(patch) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, progress: Progress = new Progress): HTTP.Content = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } } def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Bytes.write(file, download(url_name, progress = progress).bytes) object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here - override def invoke(args: List[Bytes]): List[Bytes] = + override def invoke(session: Session, args: List[Bytes]): List[Bytes] = args.map(url => download(url.text).bytes) } /* repositories */ val isabelle_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/isabelle") val afp_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel") def official_releases(): List[String] = Library.trim_split_lines( isabelle_repository.read_file(Path.explode("Admin/Release/official"))) } diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala +++ b/src/Pure/System/scala.scala @@ -1,389 +1,403 @@ /* Title: Pure/System/scala.scala Author: Makarius Support for Scala at runtime. */ package isabelle import java.io.{File => JFile, PrintStream, ByteArrayOutputStream, OutputStream} import scala.collection.mutable import scala.annotation.tailrec import dotty.tools.dotc.CompilationUnit import dotty.tools.dotc.ast.Trees.PackageDef import dotty.tools.dotc.ast.untpd import dotty.tools.dotc.core.Contexts.{Context => CompilerContext} import dotty.tools.dotc.core.NameOps.moduleClassName import dotty.tools.dotc.core.{Phases, StdNames} import dotty.tools.dotc.interfaces import dotty.tools.dotc.reporting.{Diagnostic, ConsoleReporter} import dotty.tools.dotc.util.{SourceFile, SourcePosition, NoSourcePosition} import dotty.tools.repl import dotty.tools.repl.{ReplCompiler, ReplDriver} object Scala { /** registered functions **/ abstract class Fun(val name: String, val thread: Boolean = false) { override def toString: String = name def single: Boolean = false def bytes: Boolean = false def position: Properties.T = here.position def here: Scala_Project.Here - def invoke(args: List[Bytes]): List[Bytes] + def invoke(session: Session, args: List[Bytes]): List[Bytes] } trait Single_Fun extends Fun { override def single: Boolean = true } trait Bytes_Fun extends Fun { override def bytes: Boolean = true } abstract class Fun_Strings(name: String, thread: Boolean = false) extends Fun(name, thread = thread) { - override def invoke(args: List[Bytes]): List[Bytes] = + override def invoke(session: Session, args: List[Bytes]): List[Bytes] = apply(args.map(_.text)).map(Bytes.apply) def apply(args: List[String]): List[String] } abstract class Fun_String(name: String, thread: Boolean = false) extends Fun_Strings(name, thread = thread) with Single_Fun { override def apply(args: List[String]): List[String] = List(apply(Library.the_single(args))) def apply(arg: String): String } abstract class Fun_Bytes(name: String, thread: Boolean = false) extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun { - override def invoke(args: List[Bytes]): List[Bytes] = + override def invoke(session: Session, args: List[Bytes]): List[Bytes] = List(apply(Library.the_single(args))) def apply(arg: Bytes): Bytes } val encode_fun: XML.Encode.T[Fun] = { fun => import XML.Encode._ pair(string, pair(pair(bool, bool), properties))( fun.name, ((fun.single, fun.bytes), fun.position)) } class Functions(val functions: Fun*) extends Isabelle_System.Service lazy val functions: List[Fun] = Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions) /** demo functions **/ object Echo extends Fun_String("echo") { val here = Scala_Project.here def apply(arg: String): String = arg } object Sleep extends Fun_String("sleep") { val here = Scala_Project.here def apply(seconds: String): String = { val t = seconds match { case Value.Double(s) => Time.seconds(s) case _ => error("Malformed argument: " + quote(seconds)) } val t0 = Time.now() t.sleep() val t1 = Time.now() (t1 - t0).toString } } + object Theory_Name extends Fun("command_theory_name") with Single_Fun { + val here = Scala_Project.here + override def invoke(session: Session, args: List[Bytes]): List[Bytes] = { + val id = Value.Long.parse(Library.the_single(args).text) + val name = + session.get_state().lookup_id(id) match { + case None => "" + case Some(st) => st.command.node_name.theory + } + List(Bytes(name)) + } + } + /** compiler **/ object Compiler { object Message { object Kind extends Enumeration { val error, warning, info, other = Value } private val Header = """^--.* (Error|Warning|Info): .*$""".r val header_kind: String => Kind.Value = { case "Error" => Kind.error case "Warning" => Kind.warning case "Info" => Kind.info case _ => Kind.other } // see compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala def split(str: String): List[Message] = { var kind = Kind.other val text = new mutable.StringBuilder val result = new mutable.ListBuffer[Message] def flush(): Unit = { if (text.nonEmpty) { result += Message(kind, text.toString) } kind = Kind.other text.clear() } for (line <- Library.trim_split_lines(str)) { line match { case Header(k) => flush(); kind = header_kind(k) case _ => if (line.startsWith("-- ")) flush() } if (text.nonEmpty) { text += '\n' } text ++= line } flush() result.toList } } sealed case class Message(kind: Message.Kind.Value, text: String) { def is_error: Boolean = kind == Message.Kind.error override def toString: String = text } sealed case class Result( state: repl.State, messages: List[Message], unit: Option[CompilationUnit] = None ) { val errors: List[String] = messages.flatMap(msg => if (msg.is_error) Some(msg.text) else None) def ok: Boolean = errors.isEmpty def check_state: repl.State = if (ok) state else error(cat_lines(errors)) override def toString: String = if (ok) "Result(ok)" else "Result(error)" } def context( settings: List[String] = Nil, jar_files: List[JFile] = Nil, class_loader: Option[ClassLoader] = None ): Context = { val isabelle_settings = Word.explode(Isabelle_System.getenv_strict("ISABELLE_SCALAC_OPTIONS")) val classpath = Classpath(jar_files = jar_files) new Context(isabelle_settings ::: settings, classpath, class_loader) } class Context private [Compiler]( _settings: List[String], val classpath: Classpath, val class_loader: Option[ClassLoader] = None ) { def settings: List[String] = _settings ::: List("-classpath", classpath.platform_path) private val out_stream = new ByteArrayOutputStream(1024) private val out = new PrintStream(out_stream) private val driver: ReplDriver = new ReplDriver(settings.toArray, out, class_loader) def init_state: repl.State = driver.initialState def compile(source: String, state: repl.State = init_state): Result = { out.flush() out_stream.reset() given repl.State = state val state1 = driver.run(source) out.flush() val messages = Message.split(out_stream.toString(UTF8.charset)) out_stream.reset() Result(state1, messages) } } } object Toplevel extends Fun_String("scala_toplevel") { val here = Scala_Project.here def apply(source: String): String = { val errors = try { Compiler.context().compile(source).errors.map("Scala error: " + _) } catch { case ERROR(msg) => List(msg) } locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } } /** interpreter thread **/ object Interpreter { /* requests */ sealed abstract class Request case class Execute(command: (Compiler.Context, repl.State) => repl.State) extends Request case object Shutdown extends Request /* known interpreters */ private val known = Synchronized(Set.empty[Interpreter]) def add(interpreter: Interpreter): Unit = known.change(_ + interpreter) def del(interpreter: Interpreter): Unit = known.change(_ - interpreter) def get[A](which: PartialFunction[Interpreter, A]): Option[A] = known.value.collectFirst(which) } class Interpreter(context: Compiler.Context, out: OutputStream = Console.out) { interpreter => private val running = Synchronized[Option[Thread]](None) def running_thread(thread: Thread): Boolean = running.value.contains(thread) def interrupt_thread(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt }) private var state = context.init_state private lazy val thread: Consumer_Thread[Interpreter.Request] = Consumer_Thread.fork("Scala.Interpreter") { case Interpreter.Execute(command) => try { running.change(_ => Some(Thread.currentThread())) state = command(context, state) } finally { running.change(_ => None) Exn.Interrupt.dispose() } true case Interpreter.Shutdown => Interpreter.del(interpreter) false } def shutdown(): Unit = { thread.send(Interpreter.Shutdown) interrupt_thread() thread.shutdown() } def execute(command: (Compiler.Context, repl.State) => repl.State): Unit = thread.send(Interpreter.Execute(command)) def reset(): Unit = thread.send(Interpreter.Execute((context, _) => context.init_state)) Interpreter.add(interpreter) thread } /** invoke Scala functions from ML **/ /* invoke function */ object Tag extends Enumeration { val NULL, OK, ERROR, FAIL, INTERRUPT = Value } def function_thread(name: String): Boolean = functions.find(fun => fun.name == name) match { case Some(fun) => fun.thread case None => false } - def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) = + def function_body(session: Session, name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) = functions.find(fun => fun.name == name) match { case Some(fun) => - Exn.capture { fun.invoke(args) } match { + Exn.capture { fun.invoke(session, args) } match { case Exn.Res(null) => (Tag.NULL, Nil) case Exn.Res(res) => (Tag.OK, res) case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil) case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e)))) } case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name)))) } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var session: Session = null private var futures = Map.empty[String, Future[Unit]] override def init(session: Session): Unit = synchronized { this.session = session } override def exit(): Unit = synchronized { for ((id, future) <- futures) cancel(id, future) futures = Map.empty } private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit = synchronized { if (futures.isDefinedAt(id)) { session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res) futures -= id } } private def cancel(id: String, future: Future[Unit]): Unit = { future.cancel() result(id, Scala.Tag.INTERRUPT, Nil) } private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Invoke_Scala(name, id) => def body(): Unit = { - val (tag, res) = Scala.function_body(name, msg.chunks) + val (tag, res) = Scala.function_body(session, name, msg.chunks) result(id, tag, res) } val future = if (Scala.function_thread(name)) { Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body()) } else Future.fork(body()) futures += (id -> future) true case _ => false } } private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Cancel_Scala(id) => futures.get(id) match { case Some(future) => cancel(id, future) case None => } true case _ => false } } override val functions: Session.Protocol_Functions = List( Markup.Invoke_Scala.name -> invoke_scala, Markup.Cancel_Scala.name -> cancel_scala) } } class Scala_Functions extends Scala.Functions( Scala.Echo, Scala.Sleep, + Scala.Theory_Name, Scala.Toplevel, Scala_Build.Scala_Fun, Base64.Decode, Base64.Encode, Compress.XZ_Compress, Compress.XZ_Uncompress, Compress.Zstd_Compress, Compress.Zstd_Uncompress, Doc.Doc_Names, Bibtex.Check_Database, Isabelle_System.Make_Directory, Isabelle_System.Copy_Dir, Isabelle_System.Copy_File, Isabelle_System.Copy_File_Base, Isabelle_System.Rm_Tree, Isabelle_System.Download, Isabelle_System.Isabelle_Id, Isabelle_Tool.Isabelle_Tools, isabelle.atp.SystemOnTPTP.List_Systems, isabelle.atp.SystemOnTPTP.Run_System, Prismjs.Languages, Prismjs.Tokenize) diff --git a/src/Pure/Thy/bibtex.ML b/src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML +++ b/src/Pure/Thy/bibtex.ML @@ -1,119 +1,127 @@ (* Title: Pure/Thy/bibtex.ML Author: Makarius BibTeX support. *) signature BIBTEX = sig val check_database: Position.T -> string -> (string * Position.T) list * (string * Position.T) list val check_database_output: Position.T -> string -> unit val cite_macro: string Config.T val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory end; structure Bibtex: BIBTEX = struct (* check database *) type message = string * Position.T; fun check_database pos0 database = \<^scala>\bibtex_check_database\ database |> YXML.parse_body |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0)); fun check_database_output pos0 database = let val (errors, warnings) = check_database pos0 database in errors |> List.app (fn (msg, pos) => Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n " ^ msg)); warnings |> List.app (fn (msg, pos) => warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg)) end; (* document antiquotations *) val cite_macro = Attrib.setup_config_string \<^binding>\cite_macro\ (K ""); fun get_cite_macro ctxt = Config.get ctxt cite_macro; val _ = Theory.setup (Document_Antiquotation.setup_option \<^binding>\cite_macro\ (Config.put cite_macro)); local val parse_citations = Parse.and_list1 Args.name_position; +fun command_theory_name () = + let + fun err () = error ("Cannot determine command theory name: bad PIDE id"); + val res = + (case Position.id_of (Position.thread_data ()) of + SOME id => \<^scala>\command_theory_name\ id + | NONE => err ()); + in if res = "" then err () else res end; + +fun theory_name thy = + let val name0 = Context.theory_long_name thy; + in if name0 = Context.PureN then command_theory_name () else name0 end; + fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) = let val loc = the_default Input.empty opt_loc; val _ = Context_Position.reports ctxt (Document_Output.document_reports loc @ map (fn (name, pos) => (pos, Markup.citation name)) citations); - val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt); + val thy_name = theory_name (Proof_Context.theory_of ctxt); val bibtex_entries = Resources.theory_bibtex_entries thy_name; val _ = if null bibtex_entries andalso thy_name <> Context.PureN then () else citations |> List.app (fn (name, pos) => if member (op =) bibtex_entries name orelse name = "*" then () - else if thy_name = Context.PureN then - (if Context_Position.is_visible ctxt then - warning ("Missing theory context --- unchecked Bibtex entry " ^ - quote name ^ Position.here pos) - else ()) else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos)); val kind = if macro_name = "" then get_kind ctxt else macro_name; val location = Document_Output.output_document ctxt {markdown = false} loc; in Latex.cite {kind = kind, citations = citations, location = location} end; fun cite_command_old ctxt get_kind args = let val _ = if Context_Position.is_visible ctxt then legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^ Position.here_list (map snd (snd args))) else (); in cite_command ctxt get_kind (args, "") end; val cite_keywords = Thy_Header.bootstrap_keywords |> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]); fun cite_command_embedded ctxt get_kind input = let val parser = Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations -- Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) ""; val args = Parse.read_embedded ctxt cite_keywords parser input; in cite_command ctxt get_kind args end; fun cite_command_parser get_kind = Scan.option Args.cartouche_input -- parse_citations >> (fn args => fn ctxt => cite_command_old ctxt get_kind args) || Parse.embedded_input >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg); in fun cite_antiquotation binding get_kind = Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind)) (fn ctxt => fn cmd => cmd ctxt); end; val _ = Theory.setup (cite_antiquotation \<^binding>\cite\ get_cite_macro #> cite_antiquotation \<^binding>\nocite\ (K "nocite") #> cite_antiquotation \<^binding>\citet\ (K "citet") #> cite_antiquotation \<^binding>\citep\ (K "citep")); end; diff --git a/src/Pure/Tools/scala_build.scala b/src/Pure/Tools/scala_build.scala --- a/src/Pure/Tools/scala_build.scala +++ b/src/Pure/Tools/scala_build.scala @@ -1,123 +1,123 @@ /* Title: Pure/Tools/scala_build.scala Author: Makarius Manage and build Isabelle/Scala/Java modules. */ package isabelle import java.util.{Properties => JProperties} import java.io.{ByteArrayOutputStream, PrintStream} import java.nio.file.Files import java.nio.file.{Path => JPath} import scala.jdk.CollectionConverters._ object Scala_Build { class Context private[Scala_Build](java_context: isabelle.setup.Build.Context) { override def toString: String = java_context.toString def is_module(path: Path): Boolean = { val module_name = java_context.module_name() module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file) } def module_result: Option[Path] = { java_context.module_result() match { case "" => None case module => Some(File.path(java_context.path(module).toFile)) } } def sources: List[Path] = java_context.sources().asScala.toList.map(s => File.path(java_context.path(s).toFile)) def requirements: List[Path] = (for { s <- java_context.requirements().asScala.iterator p <- java_context.requirement_paths(s).asScala.iterator } yield (File.path(p.toFile))).toList def build( classpath: List[Path] = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")), fresh: Boolean = false ): String = { val java_classpath = new java.util.LinkedList[JPath] classpath.foreach(path => java_classpath.add(path.java_path)) val output0 = new ByteArrayOutputStream val output = new PrintStream(output0) def get_output(): String = { output.flush() Library.trim_line(output0.toString(UTF8.charset)) } try { isabelle.setup.Build.build(java_classpath, output, java_context, fresh) get_output() } catch { case ERROR(msg) => cat_error(get_output(), msg) } } } def context(dir: Path, component: Boolean = false, no_title: Boolean = false, do_build: Boolean = false, module: Option[Path] = None ): Context = { val props_name = if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS else isabelle.setup.Build.BUILD_PROPS val props_path = dir + Path.explode(props_name) val props = new JProperties props.load(Files.newBufferedReader(props_path.java_path)) if (no_title) props.remove(isabelle.setup.Build.TITLE) if (do_build) props.remove(isabelle.setup.Build.NO_BUILD) if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get)) new Context(new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode)) } sealed case class Result(output: String, jar_bytes: Bytes, jar_path: Option[Path]) { def write(): Unit = { if (jar_path.isDefined) { Isabelle_System.make_directory(jar_path.get.dir) Bytes.write(jar_path.get, jar_bytes) } } } def build_result(dir: Path, component: Boolean = false): Result = { Isabelle_System.with_tmp_file("result", "jar") { tmp_file => val output = context(dir, component = component, no_title = true, do_build = true, module = Some(tmp_file)).build(classpath = Classpath().jars.map(File.path)) val jar_bytes = Bytes.read(tmp_file) val jar_path = context(dir, component = component).module_result Result(output, jar_bytes, jar_path) } } object Scala_Fun extends Scala.Fun("scala_build") with Scala.Bytes_Fun { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = + def invoke(session: Session, args: List[Bytes]): List[Bytes] = args match { case List(dir) => val result = build_result(Path.explode(dir.text)) val jar_name = result.jar_path match { case Some(path) => path.file_name case None => "scala_build.jar" } List(Bytes("classpath/" + jar_name), result.jar_bytes, Bytes(result.output)) case _ => error("Bad arguments") } } def component_contexts(): List[Context] = isabelle.setup.Build.component_contexts().asScala.toList.map(new Context(_)) }