src/Pure/ML-Systems/use_context.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/use_context.ML	Mon Mar 23 21:40:11 2009 +0100
@@ -0,0 +1,13 @@
+(*  Title:      Pure/ML-Systems/use_context.ML
+    Author:     Makarius
+
+Common context for "use" operations (compiler invocation).
+*)
+
+type use_context =
+ {tune_source: string -> string,
+  name_space: ML_Name_Space.T,
+  str_of_pos: int -> string -> string,
+  print: string -> unit,
+  error: string -> unit};
+