auxiliary operation for common uses of 'compile_generated_files';
authorwenzelm
Fri, 05 Apr 2019 17:05:32 +0200
changeset 70249 9b34dbeb1103
parent 70248 5caac4547e3b
child 70250 1eed61c3a5e5
auxiliary operation for common uses of 'compile_generated_files';
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 **)