# HG changeset patch
# User wenzelm
# Date 1554476732 -7200
# Node ID 9b34dbeb11035d8673153f084660c8be9acc1753
# Parent  5caac4547e3b4b9836cb77c0e7aec12ea1155c23
auxiliary operation for common uses of 'compile_generated_files';

diff -r 5caac4547e3b -r 9b34dbeb1103 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Apr 05 15:02:55 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Fri Apr 05 17:05:32 2019 +0200
@@ -44,6 +44,7 @@
     ((string * Position.T) list * (string * Position.T)) list ->
     ((string * Position.T) list * bool option) list ->
     string * Position.T -> Input.source -> unit
+  val execute: Path.T -> Input.source -> string -> string
 end;
 
 structure Generated_Files: GENERATED_FILES =
@@ -310,6 +311,15 @@
     source;
 
 
+(* execute compiler -- auxiliary *)
+
+fun execute dir title compile =
+  Isabelle_System.bash_output_check ("cd " ^ File.bash_path dir ^ " && " ^ compile)
+    handle ERROR msg =>
+      let val (s, pos) = Input.source_content title
+      in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end;
+
+
 
 (** concrete file types **)