Skip to content
Success

Changes

Summary

  1. merged
  2. tuned signature;
  3. support for "cluster" table with "hosts" array, and params/options as for "host" table; support for "isabelle build -H cluster.name";
  4. clarified signature: more operations, allow recursive get;
  5. tuned signature;
  6. tuned signature: more operations;
  7. clarified signature;
  8. tuned output;
  9. more robust: prefer strict operations;
  10. tuned message;
  11. tuned signature: more operations;
  12. more specific name for type class
Changeset 78966:7419b8d473ac by wenzelm:
merged
Changeset 78965:890783dc4bc6 by wenzelm:
tuned signature;
The file was modified src/Pure/System/registry.scala (diff)
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78964:a2de1f6ff94e by wenzelm:
support for &quot;cluster&quot; table with &quot;hosts&quot; array, and params/options as for &quot;host&quot; table;<br>support for &quot;isabelle build -H cluster.name&quot;;
The file was modified src/Pure/System/registry.scala (diff)
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78963:30360ee939f4 by wenzelm:
clarified signature: more operations, allow recursive get;
The file was modified src/Pure/System/registry.scala (diff)
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78962:7a58c1199de3 by wenzelm:
tuned signature;
The file was modified src/Pure/System/registry.scala (diff)
Changeset 78961:11045cf2b5c2 by wenzelm:
tuned signature: more operations;
The file was modified src/Pure/General/long_name.scala (diff)
The file was modified src/Pure/System/registry.scala (diff)
Changeset 78960:f4e7dec70fa4 by wenzelm:
clarified signature;
The file was modified src/Pure/System/registry.scala (diff)
Changeset 78959:78698a97afb3 by wenzelm:
tuned output;
The file was modified src/Pure/System/registry.scala (diff)
Changeset 78958:c125f75a5144 by wenzelm:
more robust: prefer strict operations;
The file was modified src/Pure/General/mailman.scala (diff)
The file was modified src/Pure/ML/ml_heap.scala (diff)
The file was modified src/Pure/Tools/profiling.scala (diff)
Changeset 78957:932b2a7139e2 by wenzelm:
tuned message;
The file was modified src/Pure/General/path.scala (diff)
Changeset 78956:12abaffb0346 by wenzelm:
tuned signature: more operations;
The file was modified src/Pure/Admin/build_history.scala (diff)
The file was modified src/Pure/General/bytes.scala (diff)
The file was modified src/Pure/General/file.scala (diff)
The file was modified src/Pure/ML/ml_heap.scala (diff)
The file was modified src/Pure/PIDE/headless.scala (diff)
Changeset 78955:74147aa81dbb by haftmann:
more specific name for type class
The file was modified NEWS (diff)
The file was modified src/HOL/Bit_Operations.thy (diff)
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Library/Word.thy (diff)
The file was modified src/HOL/String.thy (diff)