# HG changeset patch
# User wenzelm
# Date 1615743131 -3600
# Node ID 00b77365552e0708c82d19a6227bec339fd302f8
# Parent  dbc32e3c47e3056d23657e997d7425ff9dd87d58
clarified signature: refer to file name instead of file content;

diff -r dbc32e3c47e3 -r 00b77365552e src/HOL/Tools/ATP/system_on_tptp.ML
--- a/src/HOL/Tools/ATP/system_on_tptp.ML	Sun Mar 14 18:27:55 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Sun Mar 14 18:32:11 2021 +0100
@@ -8,7 +8,7 @@
 sig
   val get_url: unit -> string
   val list_systems: unit -> {url: string, systems: string list}
-  val run_system: {system: string, problem: string, extra: string, timeout: Time.time} ->
+  val run_system: {system: string, problem: Path.T, extra: string, timeout: Time.time} ->
     {output: string, timing: Time.time}
 end
 
@@ -24,7 +24,9 @@
   in {url = url, systems = systems} end
 
 fun run_system {system, problem, extra, timeout} =
-  cat_strings0 [get_url (), system, problem, extra, string_of_int (Time.toMilliseconds timeout)]
+  cat_strings0
+    [get_url (), system, Isabelle_System.absolute_path problem,
+      extra, string_of_int (Time.toMilliseconds timeout)]
   |> \<^scala>\<open>SystemOnTPTP.run_system\<close>
   |> split_strings0 |> (fn [output, timing] =>
     {output = output, timing = Time.fromMilliseconds (Value.parse_int timing)})
diff -r dbc32e3c47e3 -r 00b77365552e src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Mar 14 18:27:55 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Mar 14 18:32:11 2021 +0100
@@ -72,7 +72,8 @@
     val here = Scala_Project.here
     def apply(arg: String): String =
     {
-      val List(url, system, problem, extra, Value.Int(timeout)) = Library.split_strings0(arg)
+      val List(url, system, problem_path, extra, Value.Int(timeout)) = Library.split_strings0(arg)
+      val problem = File.read(Path.explode(problem_path))
       val res = run_system(Url(url), system, problem, extra = extra, timeout = Time.ms(timeout))
 
       val bad_prover = "WARNING: " + system + " does not exist"
diff -r dbc32e3c47e3 -r 00b77365552e src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sun Mar 14 18:27:55 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sun Mar 14 18:32:11 2021 +0100
@@ -11,6 +11,7 @@
   val bash: string -> int
   val bash_functions: unit -> string list
   val check_bash_function: Proof.context -> string * Position.T -> string
+  val absolute_path: Path.T -> string
   val make_directory: Path.T -> Path.T
   val copy_dir: Path.T -> Path.T -> unit
   val copy_file: Path.T -> Path.T -> unit