# HG changeset patch
# User wenzelm
# Date 1600953986 -7200
# Node ID 38497ecb4892b2703689c5d68e390fae1ea92748
# Parent  c0d04c740b8a30ef5423563793be89f05d3b5083
clarified signature;

diff -r c0d04c740b8a -r 38497ecb4892 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Sep 24 15:16:45 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 15:26:26 2020 +0200
@@ -9,7 +9,7 @@
   val add_driver:
     string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) ->
     theory -> theory
-  val overlord: bool Config.T
+  val debug: bool Config.T
   val successN: string
   val failureN: string
   val start_markerN: string
@@ -141,9 +141,9 @@
 
 (* driver invocation *)
 
-val overlord = Attrib.setup_config_bool \<^binding>\<open>code_test_overlord\<close> (K false)
+val debug = Attrib.setup_config_bool \<^binding>\<open>code_test_debug\<close> (K false)
 
-fun with_overlord_dir name f =
+fun with_debug_dir name f =
   let
     val dir =
       Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
@@ -157,8 +157,9 @@
       (case get_driver thy compiler of
         NONE => error ("No driver for target " ^ compiler)
       | SOME drv => drv)
-    val debug = Config.get (Proof_Context.init_global thy) overlord
-    val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
+    val with_dir =
+      if Config.get (Proof_Context.init_global thy) debug
+      then with_debug_dir else Isabelle_System.with_tmp_dir
     fun eval result =
       with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
       |> parse_result compiler