--- a/etc/components Thu Mar 11 07:05:38 2021 +0000
+++ b/etc/components Sat Mar 13 15:39:48 2021 +0100
@@ -7,5 +7,4 @@
src/HOL/Library/Sum_of_Squares
src/HOL/SPARK
src/HOL/Tools
-src/HOL/Tools/ATP
src/HOL/TPTP
--- a/src/Doc/System/Scala.thy Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Doc/System/Scala.thy Sat Mar 13 15:39:48 2021 +0100
@@ -210,13 +210,11 @@
\begin{matharray}{rcl}
@{ML_antiquotation_def "scala_function"} & : & \<open>ML_antiquotation\<close> \\
@{ML_antiquotation_def "scala"} & : & \<open>ML_antiquotation\<close> \\
- @{ML_antiquotation_def "scala_thread"} & : & \<open>ML_antiquotation\<close> \\
\end{matharray}
\<^rail>\<open>
(@{ML_antiquotation scala_function} |
- @{ML_antiquotation scala} |
- @{ML_antiquotation scala_thread}) @{syntax embedded}
+ @{ML_antiquotation scala}) @{syntax embedded}
\<close>
\<^descr> \<open>@{scala_function name}\<close> inlines the checked function name as ML string
--- a/src/HOL/Sledgehammer.thy Thu Mar 11 07:05:38 2021 +0000
+++ b/src/HOL/Sledgehammer.thy Sat Mar 13 15:39:48 2021 +0100
@@ -13,6 +13,7 @@
"sledgehammer_params" :: thy_decl
begin
+ML_file \<open>Tools/ATP/system_on_tptp.ML\<close>
ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
--- a/src/HOL/Tools/ATP/etc/settings Thu Mar 11 07:05:38 2021 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ISABELLE_ATP="$COMPONENT"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML Sat Mar 13 15:39:48 2021 +0100
@@ -0,0 +1,24 @@
+(* Title: HOL/Tools/ATP/system_on_tptp.ML
+ Author: Makarius
+
+Support for remote ATPs via SystemOnTPTP.
+*)
+
+signature SYSTEM_ON_TPTP =
+sig
+ val get_url: unit -> string
+ val list_systems: unit -> {url: string, systems: string list}
+end
+
+structure SystemOnTPTP: SYSTEM_ON_TPTP =
+struct
+
+fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close>
+
+fun list_systems () =
+ let
+ val url = get_url ()
+ val systems = split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> url)
+ in {url = url, systems = systems} end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala Sat Mar 13 15:39:48 2021 +0100
@@ -0,0 +1,46 @@
+/* Title: HOL/Tools/ATP/system_on_tptp.scala
+ Author: Makarius
+
+Support for remote ATPs via SystemOnTPTP.
+*/
+
+package isabelle.atp
+
+import isabelle._
+
+import java.net.URL
+
+
+object SystemOnTPTP
+{
+ /* requests */
+
+ def get_url(options: Options): URL = Url(options.string("SystemOnTPTP"))
+
+ def post_request(
+ url: URL,
+ parameters: List[(String, Any)],
+ timeout: Time = HTTP.Client.default_timeout): HTTP.Content =
+ {
+ val parameters0 =
+ List("NoHTML" -> 1, "QuietFlag" -> "-q01")
+ .filterNot(p0 => parameters.exists(p => p0._1 == p._1))
+ try {
+ HTTP.Client.post(url, parameters0 ::: parameters,
+ timeout = timeout, user_agent = "Sledgehammer")
+ }
+ catch { case ERROR(msg) => cat_error("Failed to access SystemOnTPTP server", msg) }
+ }
+
+
+ /* list systems */
+
+ def list_systems(url: URL): List[String] =
+ post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")).text_lines
+
+ object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true)
+ {
+ val here = Scala_Project.here
+ def apply(url: String): String = cat_lines(list_systems(Url(url)))
+ }
+}
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 07:05:38 2021 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Mar 13 15:39:48 2021 +0100
@@ -1035,7 +1035,7 @@
(timeout, (solve_all, (max_solutions, (max_threads, kki))))
|> let open XML.Encode in pair int (pair bool (pair int (pair int string))) end
|> YXML.string_of_body
- |> \<^scala_thread>\<open>kodkod\<close>
+ |> \<^scala>\<open>kodkod\<close>
|> YXML.parse_body
|> let open XML.Decode in triple int string string end
--- a/src/HOL/Tools/Nitpick/kodkod.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Sat Mar 13 15:39:48 2021 +0100
@@ -154,7 +154,7 @@
/** scala function **/
- object Fun extends Scala.Fun("kodkod")
+ object Fun extends Scala.Fun("kodkod", thread = true)
{
val here = Scala_Project.here
def apply(args: String): String =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Mar 11 07:05:38 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sat Mar 13 15:39:48 2021 +0100
@@ -580,18 +580,13 @@
(* Remote ATP invocation via SystemOnTPTP *)
-val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
+val no_remote_systems = {url = "", systems = [] : string list}
+val remote_systems = Synchronized.var "atp_remote_systems" no_remote_systems
fun get_remote_systems () =
- Timeout.apply (seconds 10.0) (fn () =>
- (case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
- (output, 0) => split_lines output
- | (output, _) =>
- (warning
- (case extract_known_atp_failure known_perl_failures output of
- SOME failure => string_of_atp_failure failure
- | NONE => output); []))) ()
- handle Timeout.TIMEOUT _ => []
+ Timeout.apply (seconds 10.0) SystemOnTPTP.list_systems ()
+ handle ERROR msg => (warning msg; no_remote_systems)
+ | Timeout.TIMEOUT _ => no_remote_systems
fun find_remote_system name [] systems =
find_first (String.isPrefix (name ^ "---")) systems
@@ -601,9 +596,10 @@
| res => res
fun get_remote_system name versions =
- Synchronized.change_result remote_systems (fn systems =>
- (if null systems then get_remote_systems () else systems)
- |> `(`(find_remote_system name versions)))
+ Synchronized.change_result remote_systems (fn remote =>
+ (if #url remote <> SystemOnTPTP.get_url () orelse null (#systems remote)
+ then get_remote_systems () else remote) |> ` #systems)
+ |> `(find_remote_system name versions)
fun the_remote_system name versions =
(case get_remote_system name versions of
--- a/src/HOL/Tools/etc/options Thu Mar 11 07:05:38 2021 +0000
+++ b/src/HOL/Tools/etc/options Sat Mar 13 15:39:48 2021 +0100
@@ -35,6 +35,9 @@
public option vampire_noncommercial : string = "unknown"
-- "status of Vampire activation for noncommercial use (yes, no, unknown)"
+public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
+ -- "URL for SystemOnTPTP service"
+
public option MaSh : string = "sml"
-- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
--- a/src/HOL/Tools/etc/settings Thu Mar 11 07:05:38 2021 +0000
+++ b/src/HOL/Tools/etc/settings Sat Mar 13 15:39:48 2021 +0100
@@ -2,3 +2,5 @@
isabelle_scala_service 'isabelle.nitpick.Kodkod$Handler'
isabelle_scala_service 'isabelle.nitpick.Scala_Functions'
+
+ISABELLE_ATP="$COMPONENT/ATP"
--- a/src/Pure/Admin/components.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/Admin/components.scala Sat Mar 13 15:39:48 2021 +0100
@@ -67,8 +67,7 @@
val archive = base_dir + Path.explode(archive_name)
if (!archive.is_file) {
val remote = Components.default_component_repository + "/" + archive_name
- progress.echo("Getting " + remote)
- Bytes.write(archive, Url.read_bytes(Url(remote)))
+ Isabelle_System.download(remote, archive, progress = progress)
}
for (dir <- copy_dir) {
Isabelle_System.make_directory(dir)
--- a/src/Pure/General/bytes.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/General/bytes.scala Sat Mar 13 15:39:48 2021 +0100
@@ -53,7 +53,8 @@
def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
if (limit == 0) empty
else {
- val out = new ByteArrayOutputStream(if (limit == Integer.MAX_VALUE) hint else limit)
+ val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024
+ val out = new ByteArrayOutputStream(out_size)
val buf = new Array[Byte](8192)
var m = 0
--- a/src/Pure/General/http.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/General/http.scala Sat Mar 13 15:39:48 2021 +0100
@@ -7,14 +7,148 @@
package isabelle
-import java.net.{InetAddress, InetSocketAddress, URI}
+import java.io.{File => JFile}
+import java.net.{InetSocketAddress, URI, URL, URLConnection, HttpURLConnection}
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
-import scala.collection.immutable.SortedMap
-
object HTTP
{
+ /** content **/
+
+ val mime_type_bytes: String = "application/octet-stream"
+ val mime_type_text: String = "text/plain; charset=utf-8"
+ val mime_type_html: String = "text/html; charset=utf-8"
+
+ val default_mime_type: String = mime_type_bytes
+ val default_encoding: String = UTF8.charset_name
+
+ sealed case class Content(
+ bytes: Bytes,
+ file_name: String = "",
+ mime_type: String = default_mime_type,
+ encoding: String = default_encoding)
+ {
+ def text: String = new String(bytes.array, encoding)
+ def text_lines: List[String] = Library.trim_split_lines(text)
+ }
+
+ def read_content(file: JFile): Content =
+ {
+ val bytes = Bytes.read(file)
+ val file_name = file.getName
+ val mime_type =
+ Option(URLConnection.guessContentTypeFromName(file_name)).getOrElse(default_mime_type)
+ Content(bytes, file_name = file_name, mime_type = mime_type)
+ }
+
+ def read_content(path: Path): Content = read_content(path.file)
+
+
+
+ /** client **/
+
+ val NEWLINE: String = "\r\n"
+
+ object Client
+ {
+ val default_timeout = Time.seconds(180)
+
+ def open_connection(url: URL,
+ timeout: Time = default_timeout,
+ user_agent: String = ""): HttpURLConnection =
+ {
+ url.openConnection match {
+ case connection: HttpURLConnection =>
+ if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) {
+ val ms = timeout.ms.toInt
+ connection.setConnectTimeout(ms)
+ connection.setReadTimeout(ms)
+ }
+ proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s))
+ connection
+ case _ => error("Bad URL (not HTTP): " + quote(url.toString))
+ }
+ }
+
+ def get_content(connection: HttpURLConnection): Content =
+ {
+ val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r
+ using(connection.getInputStream)(stream =>
+ {
+ val bytes = Bytes.read_stream(stream, hint = connection.getContentLength)
+ val file_name = Url.file_name(connection.getURL)
+ val mime_type = Option(connection.getContentType).getOrElse(default_mime_type)
+ val encoding =
+ (connection.getContentEncoding, mime_type) match {
+ case (enc, _) if enc != null => enc
+ case (_, Charset(enc)) => enc
+ case _ => default_encoding
+ }
+ Content(bytes, file_name = file_name, mime_type = mime_type, encoding = encoding)
+ })
+ }
+
+ def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
+ get_content(open_connection(url, timeout = timeout, user_agent = user_agent))
+
+ def post(url: URL, parameters: List[(String, Any)],
+ timeout: Time = default_timeout,
+ user_agent: String = ""): Content =
+ {
+ val connection = open_connection(url, timeout = timeout, user_agent = user_agent)
+ connection.setRequestMethod("POST")
+ connection.setDoOutput(true)
+
+ val boundary = UUID.random_string()
+ connection.setRequestProperty(
+ "Content-Type", "multipart/form-data; boundary=" + quote(boundary))
+
+ using(connection.getOutputStream)(out =>
+ {
+ def output(s: String): Unit = out.write(UTF8.bytes(s))
+ def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE))
+ def output_boundary(end: Boolean = false): Unit =
+ output("--" + boundary + (if (end) "--" else "") + NEWLINE)
+ def output_name(name: String): Unit =
+ output("Content-Disposition: form-data; name=" + quote(name))
+ def output_value(value: Any): Unit =
+ {
+ output_newline(2)
+ output(value.toString)
+ }
+ def output_content(content: Content): Unit =
+ {
+ proper_string(content.file_name).foreach(s => output("; filename=" + quote(s)))
+ output_newline()
+ proper_string(content.mime_type).foreach(s => output("Content-Type: " + s))
+ output_newline(2)
+ content.bytes.write_stream(out)
+ }
+
+ output_newline(2)
+
+ for { (name, value) <- parameters } {
+ output_boundary()
+ output_name(name)
+ value match {
+ case content: Content => output_content(content)
+ case file: JFile => output_content(read_content(file))
+ case path: Path => output_content(read_content(path))
+ case _ => output_value(value)
+ }
+ output_newline()
+ }
+ output_boundary(end = true)
+ out.flush()
+ })
+
+ get_content(connection)
+ }
+ }
+
+
+
/** server **/
/* response */
@@ -23,12 +157,12 @@
{
def apply(
bytes: Bytes = Bytes.empty,
- content_type: String = "application/octet-stream"): Response =
+ content_type: String = mime_type_bytes): Response =
new Response(bytes, content_type)
val empty: Response = apply()
- def text(s: String): Response = apply(Bytes(s), "text/plain; charset=utf-8")
- def html(s: String): Response = apply(Bytes(s), "text/html; charset=utf-8")
+ def text(s: String): Response = apply(Bytes(s), mime_type_text)
+ def html(s: String): Response = apply(Bytes(s), mime_type_html)
}
class Response private[HTTP](val bytes: Bytes, val content_type: String)
@@ -56,18 +190,7 @@
}
- /* handler */
-
- class Handler private[HTTP](val root: String, val handler: HttpHandler)
- {
- override def toString: String = root
- }
-
- def handler(root: String, body: Exchange => Unit): Handler =
- new Handler(root, new HttpHandler { def handle(x: HttpExchange): Unit = body(new Exchange(x)) })
-
-
- /* particular methods */
+ /* handler for request method */
sealed case class Arg(method: String, uri: URI, request: Bytes)
{
@@ -79,27 +202,39 @@
})
}
- def method(name: String, root: String, body: Arg => Option[Response]): Handler =
- handler(root, http =>
- {
- val request = http.read_request()
- if (http.request_method == name) {
- val arg = Arg(name, http.request_uri, request)
- Exn.capture(body(arg)) match {
- case Exn.Res(Some(response)) =>
- http.write_response(200, response)
- case Exn.Res(None) =>
- http.write_response(404, Response.empty)
- case Exn.Exn(ERROR(msg)) =>
- http.write_response(500, Response.text(Output.error_message_text(msg)))
- case Exn.Exn(exn) => throw exn
+ object Handler
+ {
+ def apply(root: String, body: Exchange => Unit): Handler =
+ new Handler(root,
+ new HttpHandler { def handle(x: HttpExchange): Unit = body(new Exchange(x)) })
+
+ def method(name: String, root: String, body: Arg => Option[Response]): Handler =
+ apply(root, http =>
+ {
+ val request = http.read_request()
+ if (http.request_method == name) {
+ val arg = Arg(name, http.request_uri, request)
+ Exn.capture(body(arg)) match {
+ case Exn.Res(Some(response)) =>
+ http.write_response(200, response)
+ case Exn.Res(None) =>
+ http.write_response(404, Response.empty)
+ case Exn.Exn(ERROR(msg)) =>
+ http.write_response(500, Response.text(Output.error_message_text(msg)))
+ case Exn.Exn(exn) => throw exn
+ }
}
- }
- else http.write_response(400, Response.empty)
- })
+ else http.write_response(400, Response.empty)
+ })
- def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body)
- def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body)
+ def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body)
+ def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body)
+ }
+
+ class Handler private(val root: String, val handler: HttpHandler)
+ {
+ override def toString: String = root
+ }
/* server */
@@ -138,7 +273,7 @@
/* welcome */
val welcome: Handler =
- get("/", arg =>
+ Handler.get("/", arg =>
if (arg.uri.toString == "/") {
val id = Isabelle_System.isabelle_id()
Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
@@ -152,7 +287,7 @@
Isabelle_Fonts.fonts(hidden = true)
def fonts(root: String = "/fonts"): Handler =
- get(root, arg =>
+ Handler.get(root, arg =>
{
val uri_name = arg.uri.toString
if (uri_name == root) {
--- a/src/Pure/General/url.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/General/url.scala Sat Mar 13 15:39:48 2021 +0100
@@ -47,7 +47,10 @@
catch { case ERROR(_) => false }
- /* trim index */
+ /* file name */
+
+ def file_name(url: URL): String =
+ Library.take_suffix[Char](c => c != '/' && c != '\\', url.getFile.toString.toList)._2.mkString
def trim_index(url: URL): URL =
{
@@ -80,13 +83,6 @@
def read(name: String): String = read(Url(name), false)
def read_gzip(name: String): String = read(Url(name), true)
- def read_bytes(url: URL): Bytes =
- {
- val connection = url.openConnection
- val length = connection.getContentLength
- using(connection.getInputStream)(Bytes.read_stream(_, hint = length))
- }
-
/* file URIs */
--- a/src/Pure/PIDE/markup.ML Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/PIDE/markup.ML Sat Mar 13 15:39:48 2021 +0100
@@ -215,7 +215,7 @@
val commands_accepted: Properties.T
val assign_update: Properties.T
val removed_versions: Properties.T
- val invoke_scala: string -> string -> bool -> Properties.T
+ val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
val task_statistics: Properties.entry
val command_timing: Properties.entry
@@ -683,8 +683,7 @@
val assign_update = [(functionN, "assign_update")];
val removed_versions = [(functionN, "removed_versions")];
-fun invoke_scala name id thread =
- [(functionN, "invoke_scala"), (nameN, name), (idN, id), ("thread", Value.print_bool thread)];
+fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
--- a/src/Pure/PIDE/markup.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/PIDE/markup.scala Sat Mar 13 15:39:48 2021 +0100
@@ -636,10 +636,9 @@
object Invoke_Scala extends Function("invoke_scala")
{
- def unapply(props: Properties.T): Option[(String, String, Boolean)] =
+ def unapply(props: Properties.T): Option[(String, String)] =
props match {
- case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) =>
- Some((name, id, thread))
+ case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
case _ => None
}
}
--- a/src/Pure/PIDE/resources.ML Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/PIDE/resources.ML Sat Mar 13 15:39:48 2021 +0100
@@ -200,11 +200,7 @@
ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
let val name = check_scala_function ctxt arg
- in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #>
- ML_Antiquotation.value_embedded \<^binding>\<open>scala_thread\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
- let val name = check_scala_function ctxt arg
- in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
+ in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)));
(* manage source files *)
--- a/src/Pure/System/bash.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/System/bash.scala Sat Mar 13 15:39:48 2021 +0100
@@ -206,7 +206,7 @@
/* Scala function */
- object Process extends Scala.Fun("bash_process")
+ object Process extends Scala.Fun("bash_process", thread = true)
{
val here = Scala_Project.here
def apply(script: String): String =
--- a/src/Pure/System/isabelle_system.ML Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/System/isabelle_system.ML Sat Mar 13 15:39:48 2021 +0100
@@ -28,7 +28,7 @@
(* bash *)
fun bash_process script =
- Scala.function_thread "bash_process"
+ Scala.function "bash_process"
("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
|> split_strings0
|> (fn [] => raise Exn.Interrupt
@@ -112,6 +112,6 @@
(* download file *)
fun download url file =
- ignore (Scala.function_thread "download" (cat_strings0 [url, absolute_path file]));
+ ignore (Scala.function "download" (cat_strings0 [url, absolute_path file]));
end;
--- a/src/Pure/System/isabelle_system.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/System/isabelle_system.scala Sat Mar 13 15:39:48 2021 +0100
@@ -551,13 +551,13 @@
{
val url = Url(url_name)
progress.echo("Getting " + quote(url_name))
- val bytes =
- try { Url.read_bytes(url) }
+ val content =
+ try { HTTP.Client.get(url) }
catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
- Bytes.write(file, bytes)
+ Bytes.write(file, content.bytes)
}
- object Download extends Scala.Fun("download")
+ object Download extends Scala.Fun("download", thread = true)
{
val here = Scala_Project.here
def apply(arg: String): String =
--- a/src/Pure/System/scala.ML Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/System/scala.ML Sat Mar 13 15:39:48 2021 +0100
@@ -8,7 +8,6 @@
sig
exception Null
val function: string -> string -> string
- val function_thread: string -> string -> string
end;
structure Scala: SCALA =
@@ -37,13 +36,15 @@
| _ => raise Fail ("Bad tag: " ^ tag));
in Synchronized.change results (Symtab.map_entry id (K result)) end);
-fun gen_function thread name arg =
+in
+
+fun function name arg =
Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
let
val id = new_id ();
fun invoke () =
(Synchronized.change results (Symtab.update (id, Exn.Exn Match));
- Output.protocol_message (Markup.invoke_scala name id thread) [XML.Text arg]);
+ Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]);
fun cancel () =
(Synchronized.change results (Symtab.delete_safe id);
Output.protocol_message (Markup.cancel_scala id) []);
@@ -60,11 +61,6 @@
handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
end) ();
-in
-
-val function = gen_function false;
-val function_thread = gen_function true;
-
end;
end;
--- a/src/Pure/System/scala.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/System/scala.scala Sat Mar 13 15:39:48 2021 +0100
@@ -17,7 +17,8 @@
{
/** registered functions **/
- abstract class Fun(val name: String) extends Function[String, String]
+ abstract class Fun(val name: String, val thread: Boolean = false)
+ extends Function[String, String]
{
override def toString: String = name
def position: Properties.T = here.position
@@ -155,7 +156,13 @@
val NULL, OK, ERROR, FAIL, INTERRUPT = Value
}
- def function(name: String, arg: String): (Tag.Value, String) =
+ 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, arg: String): (Tag.Value, String) =
functions.find(fun => fun.name == name) match {
case Some(fun) =>
Exn.capture { fun(arg) } match {
@@ -202,14 +209,14 @@
private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
- case Markup.Invoke_Scala(name, id, thread) =>
+ case Markup.Invoke_Scala(name, id) =>
def body: Unit =
{
- val (tag, res) = Scala.function(name, msg.text)
+ val (tag, res) = Scala.function_body(name, msg.text)
result(id, tag, res)
}
val future =
- if (thread) {
+ if (Scala.function_thread(name)) {
Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body)
}
else Future.fork(body)
@@ -252,4 +259,5 @@
Isabelle_System.Copy_File_Base,
Isabelle_System.Rm_Tree,
Isabelle_System.Download,
- Isabelle_Tool.Isabelle_Tools)
+ Isabelle_Tool.Isabelle_Tools,
+ isabelle.atp.SystemOnTPTP.List_Systems)
--- a/src/Pure/Tools/phabricator.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/Tools/phabricator.scala Sat Mar 13 15:39:48 2021 +0100
@@ -218,7 +218,7 @@
val archive =
if (Url.is_wellformed(mercurial_source)) {
val archive = tmp_dir + Path.basic("mercurial.tar.gz")
- Bytes.write(archive, Url.read_bytes(Url(mercurial_source)))
+ Isabelle_System.download(mercurial_source, archive)
archive
}
else Path.explode(mercurial_source)
--- a/src/Pure/Tools/scala_project.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/Tools/scala_project.scala Sat Mar 13 15:39:48 2021 +0100
@@ -74,6 +74,7 @@
"src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"),
"src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"),
"src/HOL/SPARK/Tools" -> Path.explode("isabelle.spark"),
+ "src/HOL/Tools/ATP" -> Path.explode("isabelle.atp"),
"src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick"))
--- a/src/Pure/build-jars Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Pure/build-jars Sat Mar 13 15:39:48 2021 +0100
@@ -10,6 +10,7 @@
declare -a SOURCES=(
src/HOL/SPARK/Tools/spark.scala
+ src/HOL/Tools/ATP/system_on_tptp.scala
src/HOL/Tools/Nitpick/kodkod.scala
src/Pure/Admin/afp.scala
src/Pure/Admin/build_csdp.scala
--- a/src/Tools/jEdit/src/document_model.scala Thu Mar 11 07:05:38 2021 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Sat Mar 13 15:39:48 2021 +0100
@@ -314,7 +314,7 @@
val preview_root = http_root + "/preview"
val html =
- HTTP.get(preview_root, arg =>
+ HTTP.Handler.get(preview_root, arg =>
for {
query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
name = Library.perhaps_unprefix(plain_text_prefix, query)