From 5a7cbf2da596803223a414eae9a0707e73be5b95 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Tue, 20 Jun 2023 11:05:11 +0200
Subject: [PATCH] Add file checking in figure_content

---
 Isabelle_DOF/thys/Isa_COL.thy | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy
index f8ca87f..3e224b5 100644
--- a/Isabelle_DOF/thys/Isa_COL.thy
+++ b/Isabelle_DOF/thys/Isa_COL.thy
@@ -376,7 +376,9 @@ fun fig_content_antiquotation name scan =
           
 
 fun figure_content ctxt (cfg_trans,file:Input.source) =
-  let val (wdth_val_s, ht_s, caption) = process_args cfg_trans
+  let val _   = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
+      (* ToDo: must be declared source of type png or jpeg or pdf, ... *)
+      val (wdth_val_s, ht_s, caption) = process_args cfg_trans
       val args = ["keepaspectratio","width=" ^ wdth_val_s, ht_s]
                  |> commas
                  |> enclose "[" "]"