# HG changeset patch
# User wenzelm
# Date 1737112259 -3600
# Node ID 5a7bf0f038e2b12659485b47eb1ae07443d9a88a
# Parent  acd9849d4e9e7216db9a69db977af6a605ad2706
more robust import_file path: proper master_directory;
support for compressed proofs.zst (e.g. via "zstd -8");

diff -r acd9849d4e9e -r 5a7bf0f038e2 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 11:49:31 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 12:10:59 2025 +0100
@@ -442,12 +442,16 @@
     process tstate (parse_line str)
   end
 
-fun process_file path thy =
-  #1 (fold process_line (File.read_lines path) (thy, init_state))
+fun process_file path0 thy =
+  let
+    val path = File.absolute_path (Resources.master_directory thy + path0)
+    val lines =
+      if Path.is_zst path then Bytes.read path |> Zstd.uncompress |> Bytes.trim_split_lines
+      else File.read_lines path
+  in #1 (fold process_line lines (thy, init_state)) end
 
 val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
   "import a recorded proof file"
   (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
 
-
 end