src/Pure/RAW/use_context.ML
changeset 62490 39d01eaf5292
parent 62489 36f11bc393a2
child 62491 7187cb7a77c5
--- a/src/Pure/RAW/use_context.ML	Tue Mar 01 17:26:53 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/use_context.ML
-    Author:     Makarius
-
-Common context for "use" operations (compiler invocation).
-*)
-
-type use_context =
- {name_space: ML_Name_Space.T,
-  str_of_pos: int -> string -> string,
-  print: string -> unit,
-  error: string -> unit};
-
-val boot_context: use_context =
- {name_space = ML_Name_Space.global,
-  str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
-  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
-  error = fn s => raise Fail s};