--- a/src/Pure/Build/resources.ML Mon Aug 18 22:37:21 2025 +0100
+++ b/src/Pure/Build/resources.ML Wed Aug 20 11:17:13 2025 +0200
@@ -209,38 +209,38 @@
in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end)));
-(* manage source files *)
+(* theory resources *)
-type files =
+type data =
{master_dir: Path.T, (*master directory of theory source*)
imports: (string * Position.T) list, (*source specification of imports*)
provided: (Path.T * SHA1.digest) list}; (*source path, digest*)
-fun make_files (master_dir, imports, provided): files =
+fun make_data (master_dir, imports, provided): data =
{master_dir = master_dir, imports = imports, provided = provided};
-structure Files = Theory_Data
+structure Data = Theory_Data
(
- type T = files;
- val empty = make_files (Path.current, [], []);
+ type T = data;
+ val empty = make_data (Path.current, [], []);
fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) =
let val provided' = Library.merge (op =) (provided1, provided2)
- in make_files (master_dir, imports, provided') end
+ in make_data (master_dir, imports, provided') end
);
-fun map_files f =
- Files.map (fn {master_dir, imports, provided} =>
- make_files (f (master_dir, imports, provided)));
+fun map_data f =
+ Data.map (fn {master_dir, imports, provided} =>
+ make_data (f (master_dir, imports, provided)));
-val master_directory = #master_dir o Files.get;
-val imports_of = #imports o Files.get;
+val master_directory = #master_dir o Data.get;
+val imports_of = #imports o Data.get;
fun begin_theory master_dir {name, imports, keywords} parents =
let
val thy =
Theory.begin_theory name parents
- |> map_files (fn _ => (Path.explode (File.symbolic_path master_dir), imports, []))
+ |> map_data (fn _ => (Path.explode (File.symbolic_path master_dir), imports, []))
|> Thy_Header.add_keywords keywords;
val ctxt = Proof_Context.init_global thy;
val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords;
@@ -379,7 +379,7 @@
fun provide (src_path, digest) =
- map_files (fn (master_dir, imports, provided) =>
+ map_data (fn (master_dir, imports, provided) =>
if AList.defined (op =) provided src_path then
error ("Duplicate use of source file: " ^ Path.print src_path)
else (master_dir, imports, (src_path, digest) :: provided));
@@ -401,7 +401,7 @@
in ((full_path, digest), text) end;
fun loaded_files_current thy =
- #provided (Files.get thy) |>
+ #provided (Data.get thy) |>
forall (fn (src_path, digest) =>
(case try (load_file thy) src_path of
NONE => false
--- a/src/Pure/System/other_isabelle.scala Mon Aug 18 22:37:21 2025 +0100
+++ b/src/Pure/System/other_isabelle.scala Wed Aug 20 11:17:13 2025 +0200
@@ -90,42 +90,8 @@
def etc_settings: Path = etc + Path.explode("settings")
def etc_preferences: Path = etc + Path.explode("preferences")
-
- /* ML system settings */
-
- val ml_settings: ML_Settings =
- new ML_Settings {
- override def polyml_home: Path =
- getenv("POLYML_HOME") match {
- case "" =>
- try { expand_path(Path.variable("ML_HOME")).dir }
- catch { case ERROR(msg) => error("Bad ML_HOME: " + msg + error_context) }
- case s => Path.explode(s)
- }
-
- override def ml_system: String = getenv_strict("ML_SYSTEM")
-
- override def ml_platform: String =
- if (ssh.is_file(isabelle_home + Path.explode("lib/Tools/console"))) {
- val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
- val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
- val result = bash("bin/isabelle console -r", input = input)
- result.out match {
- case Pattern(a) if result.ok && a.nonEmpty => a
- case _ =>
- error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
- if_proper(result.err, "\n" + result.err) + error_context)
- }
- }
- else getenv_strict("ML_PLATFORM")
-
- override def ml_options: String =
- proper_string(getenv("ML_OPTIONS")) getOrElse
- getenv(if (ml_platform_is_64_32) "ML_OPTIONS32" else "ML_OPTIONS64")
- }
-
- def user_output_dir: Path =
- isabelle_home_user + Path.basic("heaps") + Path.basic(ml_settings.ml_identifier)
+ def cleanup(): Unit =
+ ssh.delete(host_db, etc_settings, etc_preferences, etc, isabelle_home_user)
/* components */
@@ -234,8 +200,39 @@
}
- /* cleanup */
+ /* ML system settings */
+
+ val ml_settings: ML_Settings =
+ new ML_Settings {
+ override def polyml_home: Path =
+ getenv("POLYML_HOME") match {
+ case "" =>
+ try { expand_path(Path.variable("ML_HOME")).dir }
+ catch { case ERROR(msg) => error("Bad ML_HOME: " + msg + error_context) }
+ case s => Path.explode(s)
+ }
+
+ override def ml_system: String = getenv_strict("ML_SYSTEM")
- def cleanup(): Unit =
- ssh.delete(host_db, etc_settings, etc_preferences, etc, isabelle_home_user)
+ override def ml_platform: String =
+ if (ssh.is_file(isabelle_home + Path.explode("lib/Tools/console"))) {
+ val Pattern = """.*val ML_PLATFORM = "(.*)".*""".r
+ val input = """val ML_PLATFORM = Option.getOpt (OS.Process.getEnv "ML_PLATFORM", "")"""
+ val result = bash("bin/isabelle console -r", input = input)
+ result.out match {
+ case Pattern(a) if result.ok && a.nonEmpty => a
+ case _ =>
+ error("Cannot get ML_PLATFORM from other Isabelle: " + isabelle_home +
+ if_proper(result.err, "\n" + result.err) + error_context)
+ }
+ }
+ else getenv_strict("ML_PLATFORM")
+
+ override def ml_options: String =
+ proper_string(getenv("ML_OPTIONS")) getOrElse
+ getenv(if (ml_platform_is_64_32) "ML_OPTIONS32" else "ML_OPTIONS64")
+ }
+
+ def user_output_dir: Path =
+ isabelle_home_user + Path.basic("heaps") + Path.basic(ml_settings.ml_identifier)
}
--- a/src/Pure/context.ML Mon Aug 18 22:37:21 2025 +0100
+++ b/src/Pure/context.ML Wed Aug 20 11:17:13 2025 +0200
@@ -1,14 +1,19 @@
(* Title: Pure/context.ML
- Author: Markus Wenzel, TU Muenchen
+ Author: Makarius
-Generic theory contexts with unique identity, arbitrarily typed data,
-monotonic development graph and history support. Generic proof
-contexts with arbitrarily typed data.
+Generic theory contexts with unique identity, arbitrarily typed data, and
+monotonic updates.
-Firm naming conventions:
+Generic proof contexts with arbitrarily typed data.
+
+Good names:
thy, thy', thy1, thy2: theory
ctxt, ctxt', ctxt1, ctxt2: Proof.context
context: Context.generic
+
+Bad names:
+ ctx: Proof.context
+ context: Proof.context
*)
signature BASIC_CONTEXT =