src/Pure/RAW/use_context.ML
changeset 62490 39d01eaf5292
parent 62489 36f11bc393a2
child 62491 7187cb7a77c5
equal deleted inserted replaced
62489:36f11bc393a2 62490:39d01eaf5292
     1 (*  Title:      Pure/RAW/use_context.ML
       
     2     Author:     Makarius
       
     3 
       
     4 Common context for "use" operations (compiler invocation).
       
     5 *)
       
     6 
       
     7 type use_context =
       
     8  {name_space: ML_Name_Space.T,
       
     9   str_of_pos: int -> string -> string,
       
    10   print: string -> unit,
       
    11   error: string -> unit};
       
    12 
       
    13 val boot_context: use_context =
       
    14  {name_space = ML_Name_Space.global,
       
    15   str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
       
    16   print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
       
    17   error = fn s => raise Fail s};