src/Pure/ML-Systems/use_context.ML
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 30672 beaadd5af500
permissions -rw-r--r--
tuned signature;
tuned comments;
     1 (*  Title:      Pure/ML-Systems/use_context.ML
     2     Author:     Makarius
     3 
     4 Common context for "use" operations (compiler invocation).
     5 *)
     6 
     7 type use_context =
     8  {tune_source: string -> string,
     9   name_space: ML_Name_Space.T,
    10   str_of_pos: int -> string -> string,
    11   print: string -> unit,
    12   error: string -> unit};
    13