# HG changeset patch
# User wenzelm
# Date 1237892472 -3600
# Node ID 5f0919630aaaec5378be405cd4f60e9723559c21
# Parent  182fb8d27b48656f56083e85ca27fa44d4354033# Parent  e8ac1f9d94692f3ff3b4badcad3873879aa53786
merged

diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -8,7 +8,7 @@
 sig
   datatype 'a antiquote =
     Text of 'a |
-    Antiq of Symbol_Pos.T list * Position.T |
+    Antiq of Symbol_Pos.T list * Position.range |
     Open of Position.T |
     Close of Position.T
   val is_text: 'a antiquote -> bool
@@ -26,7 +26,7 @@
 
 datatype 'a antiquote =
   Text of 'a |
-  Antiq of Symbol_Pos.T list * Position.T |
+  Antiq of Symbol_Pos.T list * Position.range |
   Open of Position.T |
   Close of Position.T;
 
@@ -39,7 +39,7 @@
 val report_antiq = Position.report Markup.antiq;
 
 fun report report_text (Text x) = report_text x
-  | report _ (Antiq (_, pos)) = report_antiq pos
+  | report _ (Antiq (_, (pos, _))) = report_antiq pos
   | report _ (Open pos) = report_antiq pos
   | report _ (Close pos) = report_antiq pos;
 
@@ -79,7 +79,7 @@
   Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
     Symbol_Pos.!!! "missing closing brace of antiquotation"
       (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
-  >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
+  >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
 
 val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
 val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/General/output.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -47,7 +47,6 @@
   val debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
-  val ml_output: (string -> unit) * (string -> 'a)
   val accumulated_time: unit -> unit
 end;
 
@@ -101,7 +100,7 @@
 val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
 val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
 val prompt_fn = ref std_output;
-val status_fn = ref (fn s => ! writeln_fn s);
+val status_fn = ref (fn _: string => ());
 
 fun writeln s = ! writeln_fn (output s);
 fun priority s = ! priority_fn (output s);
@@ -120,8 +119,6 @@
 val debugging = ref false;
 fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
 
-val ml_output = (writeln, error);
-
 
 
 (** timing **)
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/General/position.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -24,6 +24,7 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
+  val report_text: Markup.T -> T -> string -> unit
   val report: Markup.T -> T -> unit
   val str_of: T -> string
   type range = T * T
@@ -121,9 +122,11 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
-fun report markup (pos as Pos (count, _)) =
+fun report_text markup (pos as Pos (count, _)) txt =
   if invalid_count count then ()
-  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) "");
+  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) txt);
+
+fun report markup pos = report_text markup pos "";
 
 
 (* str_of *)
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/General/secure.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -9,11 +9,8 @@
   val set_secure: unit -> unit
   val is_secure: unit -> bool
   val deny_secure: string -> unit
-  val use_text: ML_NameSpace.nameSpace -> int * string ->
-    (string -> unit) * (string -> 'a) -> bool -> string -> unit
-  val use_file: ML_NameSpace.nameSpace ->
-    (string -> unit) * (string -> 'a) -> bool -> string -> unit
-  val use: string -> unit
+  val use_text: use_context -> int * string -> bool -> string -> unit
+  val use_file: use_context -> bool -> string -> unit
   val toplevel_pp: string list -> string -> unit
   val commit: unit -> unit
   val system_out: string -> string * int
@@ -40,23 +37,17 @@
 
 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
 
-fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
-fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
-fun raw_toplevel_pp x =
-  toplevel_pp ML_Parse.fix_ints (Position.str_of oo Position.line_file) Output.ml_output x;
+val raw_use_text = use_text;
+val raw_use_file = use_file;
+val raw_toplevel_pp = toplevel_pp;
 
-fun use_text ns pos pr verbose txt =
-  (secure_mltext (); raw_use_text ns pos pr verbose txt);
+fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt);
+fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name);
 
-fun use_file ns pr verbose name =
-  (secure_mltext (); raw_use_file ns pr verbose name);
-
-fun use name = use_file ML_NameSpace.global Output.ml_output true name;
-
-fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp path pp);
+fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
 
 (*commit is dynamically bound!*)
-fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
+fun commit () = raw_use_text ML_Parse.global_context (0, "") false "commit();";
 
 
 (* shell commands *)
@@ -77,7 +68,8 @@
 (*override previous toplevel bindings!*)
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
-fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
+fun use s = Secure.use_file ML_Parse.global_context true s
+  handle ERROR msg => (writeln msg; raise Fail "ML error");
 val toplevel_pp = Secure.toplevel_pp;
 val system_out = Secure.system_out;
 val system = Secure.system;
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/IsaMakefile	Tue Mar 24 12:01:12 2009 +0100
@@ -70,7 +70,8 @@
   Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML		\
   ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
   ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
-  ML-Systems/install_pp_polyml-experimental.ML Proof/extraction.ML	\
+  ML-Systems/install_pp_polyml-experimental.ML				\
+  ML-Systems/use_context.ML Proof/extraction.ML				\
   Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
   Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML	\
   ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -150,23 +150,25 @@
   Pretty.mark (Markup.command_decl name (kind_of kind))
     (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
 
+fun status_writeln s = (Output.status s; writeln s);
+
 fun report () =
   let val (keywords, commands) = CRITICAL (fn () =>
     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   in map report_keyword keywords @ map report_command commands end
-  |> Pretty.chunks |> Pretty.string_of |> Output.status;
+  |> Pretty.chunks |> Pretty.string_of |> status_writeln;
 
 
 (* augment tables *)
 
 fun keyword name =
  (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
-  Output.status (Pretty.string_of (report_keyword name)));
+  status_writeln (Pretty.string_of (report_keyword name)));
 
 fun command name kind =
  (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   change_commands (Symtab.update (name, kind));
-  Output.status (Pretty.string_of (report_command (name, kind))));
+  status_writeln (Pretty.string_of (report_command (name, kind))));
 
 
 (* command categories *)
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/ml_name_space.ML
--- a/src/Pure/ML-Systems/ml_name_space.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/ml_name_space.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -4,7 +4,7 @@
 ML name space -- dummy version of Poly/ML 5.2 facility.
 *)
 
-structure ML_NameSpace =
+structure ML_Name_Space =
 struct
 
 type valueVal = unit;
@@ -14,7 +14,7 @@
 type signatureVal = unit;
 type functorVal = unit;
 
-type nameSpace =
+type T =
  {lookupVal:    string -> valueVal option,
   lookupType:   string -> typeVal option,
   lookupFix:    string -> fixityVal option,
@@ -34,7 +34,7 @@
   allSig:       unit -> (string * signatureVal) list,
   allFunct:     unit -> (string * functorVal) list};
 
-val global: nameSpace =
+val global: T =
  {lookupVal = fn _ => NONE,
   lookupType = fn _ => NONE,
   lookupFix = fn _ => NONE,
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -46,6 +46,7 @@
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
 
 
 (*low-level pointer equality*)
@@ -120,7 +121,7 @@
 end;
 
 (*dummy implementation*)
-fun toplevel_pp _ _ _ _ _ = ();
+fun toplevel_pp _ _ _ = ();
 
 (*dummy implementation*)
 fun ml_prompts p1 p2 = ();
@@ -185,18 +186,18 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_text (tune: string -> string) _ _ _ _ _ txt =
+fun use_text ({tune_source, ...}: use_context) _ _ txt =
   let
     val tmp_name = FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;
   in
-    TextIO.output (tmp_file, tune txt);
+    TextIO.output (tmp_file, tune_source txt);
     TextIO.closeOut tmp_file;
     use tmp_name;
     FileSys.remove tmp_name
   end;
 
-fun use_file _ _ _ _ _ name = use name;
+fun use_file _ _ name = use name;
 
 
 
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml-4.1.3.ML
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -6,6 +6,7 @@
 use "ML-Systems/polyml_old_basis.ML";
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml-4.1.4.ML
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -6,6 +6,7 @@
 use "ML-Systems/polyml_old_basis.ML";
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml-4.2.0.ML
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -5,6 +5,7 @@
 
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -5,6 +5,7 @@
 
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler5.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -4,6 +4,7 @@
 *)
 
 use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler5.ML";
 use "ML-Systems/polyml_pp.ML";
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -4,6 +4,14 @@
 *)
 
 open Thread;
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+end;
+
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/multithreading_polyml.ML";
 
@@ -14,12 +22,6 @@
 
 (* runtime compilation *)
 
-structure ML_NameSpace =
-struct
-  open PolyML.NameSpace;
-  val global = PolyML.globalNameSpace;
-end;
-
 local
 
 fun drop_newline s =
@@ -28,11 +30,11 @@
 
 in
 
-fun use_text (tune: string -> string) str_of_pos
-    name_space (start_line, name) (print, err) verbose txt =
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+    (start_line, name) verbose txt =
   let
     val current_line = ref start_line;
-    val in_buffer = ref (String.explode (tune txt));
+    val in_buffer = ref (String.explode (tune_source txt));
     val out_buffer = ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
@@ -42,10 +44,11 @@
       | c :: cs =>
           (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
     fun put s = out_buffer := s :: ! out_buffer;
-    fun put_message {message, hard, location = {startLine = line, ...}, context} =
+    fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
      (put (if hard then "Error: " else "Warning: ");
-      PolyML.prettyPrint (put, 76) message;
-      put (str_of_pos line name ^ "\n"));
+      PolyML.prettyPrint (put, 76) msg1;
+      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
+      put ("At" ^ str_of_pos line name ^ "\n"));
 
     val parameters =
      [PolyML.Compiler.CPOutStream put,
@@ -58,30 +61,50 @@
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        err (output ()); raise exn);
+        error (output ()); raise exn);
   in if verbose then print (output ()) else () end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
 
 end;
 
 
 (* toplevel pretty printing *)
 
-fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
-  | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
-  | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+val pretty_ml =
+  let
+    fun convert len (PrettyBlock (ind, _, context, prts)) =
+          let
+            fun property name default =
+              (case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
+                SOME (ContextProperty (_, b)) => b
+              | NONE => default);
+            val bg = property "begin" "";
+            val en = property "end" "";
+            val len' = property "length" len;
+          in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
+      | convert len (PrettyString s) =
+          ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
+      | convert _ (PrettyBreak (wd, _)) =
+          ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+  in convert "" end;
 
-fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
-  | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
+fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
+      let val context =
+        (if bg = "" then [] else [ContextProperty ("begin", bg)]) @
+        (if en = "" then [] else [ContextProperty ("end", en)])
+      in PrettyBlock (ind, false, context, map ml_pretty prts) end
+  | ml_pretty (ML_Pretty.String (s, len)) =
+      if len = size s then PrettyString s
+      else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s])
   | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
   | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
 
-fun toplevel_pp tune str_of_pos output (_: string list) pp =
-  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+fun toplevel_pp context (_: string list) pp =
+  use_text context (1, "pp") false
     ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -4,6 +4,14 @@
 *)
 
 open Thread;
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+end;
+
 use "ML-Systems/polyml_common.ML";
 
 if ml_system = "polyml-5.2"
@@ -17,12 +25,6 @@
 
 (* runtime compilation *)
 
-structure ML_NameSpace =
-struct
-  open PolyML.NameSpace;
-  val global = PolyML.globalNameSpace;
-end;
-
 local
 
 fun drop_newline s =
@@ -31,11 +33,11 @@
 
 in
 
-fun use_text (tune: string -> string) str_of_pos
-    name_space (start_line, name) (print, err) verbose txt =
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+    (start_line, name) verbose txt =
   let
     val current_line = ref start_line;
-    val in_buffer = ref (String.explode (tune txt));
+    val in_buffer = ref (String.explode (tune_source txt));
     val out_buffer = ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
@@ -58,14 +60,14 @@
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        err (output ()); raise exn);
+        error (output ()); raise exn);
   in if verbose then print (output ()) else () end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
 
 end;
 
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -9,8 +9,8 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/system_shell.ML";
-use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
 
 
 (** ML system and platform related **)
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml_old_compiler4.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -3,9 +3,9 @@
 Runtime compilation -- for old PolyML.compiler (version 4.x).
 *)
 
-fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line: int, name) verbose txt =
   let
-    val in_buffer = ref (explode (tune txt));
+    val in_buffer = ref (explode (tune_source txt));
     val out_buffer = ref ([]: string list);
     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
 
@@ -21,12 +21,12 @@
       | _ => (PolyML.compiler (get, put) (); exec ()));
   in
     exec () handle exn =>
-      (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+      (error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml_old_compiler5.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -3,9 +3,9 @@
 Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
 *)
 
-fun use_text (tune: string -> string) _ _ (line, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
   let
-    val in_buffer = ref (explode (tune txt));
+    val in_buffer = ref (explode (tune_source txt));
     val out_buffer = ref ([]: string list);
     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
 
@@ -21,12 +21,12 @@
         [] => ()
       | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
   in
-    exec () handle exn => (err (output ()); raise exn);
+    exec () handle exn => (error (output ()); raise exn);
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/polyml_pp.ML
--- a/src/Pure/ML-Systems/polyml_pp.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_pp.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -14,7 +14,7 @@
       | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
   in pprint end;
 
-fun toplevel_pp tune str_of_pos output (_: string list) pp =
-  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+fun toplevel_pp context (_: string list) pp =
+  use_text context (1, "pp") false
     ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
 
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -14,6 +14,7 @@
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
 
 
 (*low-level pointer equality*)
@@ -100,7 +101,7 @@
 
 (* ML command execution *)
 
-fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
   let
     val ref out_orig = Control.Print.out;
 
@@ -111,22 +112,20 @@
       in String.substring (str, 0, Int.max (0, size str - 1)) end;
   in
     Control.Print.out := out;
-    Backend.Interact.useStream (TextIO.openString (tune txt)) handle exn =>
+    Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn =>
       (Control.Print.out := out_orig;
-        err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+        error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
     Control.Print.out := out_orig;
     if verbose then print (output ()) else ()
   end;
 
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+  in use_text context (1, name) verbose txt end;
 
-fun forget_structure name =
-  use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false
-    ("structure " ^ name ^ " = struct end");
+fun forget_structure _ = ();
 
 
 (* toplevel pretty printing *)
@@ -143,8 +142,8 @@
       | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
   in pprint end;
 
-fun toplevel_pp tune str_of_pos output path pp =
-  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+fun toplevel_pp context path pp =
+  use_text context (1, "pp") false
     ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
       "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
 
diff -r 182fb8d27b48 -r 5f0919630aaa 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	Tue Mar 24 12:01:12 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};
+
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -20,7 +20,8 @@
   val the_local_context: unit -> Proof.context
   val exec: (unit -> unit) -> Context.generic -> Context.generic
   val inherit_env: Context.generic -> Context.generic -> Context.generic
-  val name_space: ML_NameSpace.nameSpace
+  val name_space: ML_Name_Space.T
+  val local_context: use_context
   val stored_thms: thm list ref
   val ml_store_thm: string * thm -> unit
   val ml_store_thms: string * thm list -> unit
@@ -31,13 +32,10 @@
   val trace: bool ref
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
-  val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
-    Position.T -> Symbol_Pos.text -> unit
   val eval: bool -> Position.T -> Symbol_Pos.text -> unit
   val eval_file: Path.T -> unit
   val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
-  val evaluate: Proof.context -> (string -> unit) * (string -> 'b) -> bool ->
-    string * (unit -> 'a) option ref -> string -> 'a
+  val evaluate: Proof.context -> bool -> string * (unit -> 'a) option ref -> string -> 'a
   val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
 end
 
@@ -61,12 +59,12 @@
 structure ML_Env = GenericDataFun
 (
   type T =
-    ML_NameSpace.valueVal Symtab.table *
-    ML_NameSpace.typeVal Symtab.table *
-    ML_NameSpace.fixityVal Symtab.table *
-    ML_NameSpace.structureVal Symtab.table *
-    ML_NameSpace.signatureVal Symtab.table *
-    ML_NameSpace.functorVal Symtab.table;
+    ML_Name_Space.valueVal Symtab.table *
+    ML_Name_Space.typeVal Symtab.table *
+    ML_Name_Space.fixityVal Symtab.table *
+    ML_Name_Space.structureVal Symtab.table *
+    ML_Name_Space.signatureVal Symtab.table *
+    ML_Name_Space.functorVal Symtab.table;
   val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
   val extend = I;
   fun merge _
@@ -82,23 +80,23 @@
 
 val inherit_env = ML_Env.put o ML_Env.get;
 
-val name_space: ML_NameSpace.nameSpace =
+val name_space: ML_Name_Space.T =
   let
     fun lookup sel1 sel2 name =
       Context.thread_data ()
       |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name)
-      |> (fn NONE => sel2 ML_NameSpace.global name | some => some);
+      |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
 
     fun all sel1 sel2 () =
       Context.thread_data ()
       |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context)))
-      |> append (sel2 ML_NameSpace.global ())
+      |> append (sel2 ML_Name_Space.global ())
       |> sort_distinct (string_ord o pairself #1);
 
     fun enter ap1 sel2 entry =
       if is_some (Context.thread_data ()) then
         Context.>> (ML_Env.map (ap1 (Symtab.update entry)))
-      else sel2 ML_NameSpace.global entry;
+      else sel2 ML_Name_Space.global entry;
   in
    {lookupVal    = lookup #1 #lookupVal,
     lookupType   = lookup #2 #lookupType,
@@ -120,6 +118,13 @@
     allFunct     = all #6 #allFunct}
   end;
 
+val local_context: use_context =
+ {tune_source = ML_Parse.fix_ints,
+  name_space = name_space,
+  str_of_pos = Position.str_of oo Position.line_file,
+  print = writeln,
+  error = error};
+
 
 (* theorem bindings *)
 
@@ -134,7 +139,7 @@
       else if not (ML_Syntax.is_identifier name) then
         error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
       else setmp stored_thms ths' (fn () =>
-        use_text name_space (0, "") Output.ml_output true
+        use_text local_context (0, "") true
           ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
   in () end;
 
@@ -214,12 +219,12 @@
           fun no_decl _ = ([], []);
 
           fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
-            | expand (Antiquote.Antiq x) (scope, background) =
+            | expand (Antiquote.Antiq (ss, range)) (scope, background) =
                 let
                   val context = Stack.top scope;
-                  val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
+                  val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
                   val (decl, background') = f {background = background, struct_name = struct_name};
-                  val decl' = pairself ML_Lex.tokenize o decl;
+                  val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
                 in (decl', (Stack.map_top (K context') scope, background')) end
             | expand (Antiquote.Open _) (scope, background) =
                 (no_decl, (Stack.push scope, background))
@@ -233,10 +238,10 @@
 
 val trace = ref false;
 
-fun eval_wrapper pr verbose pos txt =
+fun eval verbose pos txt =
   let
-    fun eval_raw p = use_text name_space
-      (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr;
+    fun eval_raw p = use_text local_context
+      (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p));
 
     (*prepare source text*)
     val _ = Position.report Markup.ML_source pos;
@@ -260,20 +265,18 @@
 end;
 
 
-(* ML evaluation *)
+(* derived versions *)
 
-val eval = eval_wrapper Output.ml_output;
 fun eval_file path = eval true (Path.position path) (File.read path);
 
 fun eval_in ctxt verbose pos txt =
   Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
 
-fun evaluate ctxt pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
+fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   let
     val _ = r := NONE;
     val _ = Context.setmp_thread_data (SOME (Context.Proof ctxt)) (fn () =>
-      eval_wrapper pr verbose Position.none
-        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))")) ();
+      eval verbose Position.none ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))")) ();
   in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
 
 fun expression pos bind body txt =
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -13,6 +13,7 @@
   val stopper: token Scan.stopper
   val is_regular: token -> bool
   val is_improper: token -> bool
+  val set_range: Position.range -> token -> token
   val pos_of: token -> Position.T
   val kind_of: token -> token_kind
   val content_of: token -> string
@@ -42,6 +43,8 @@
 
 (* position *)
 
+fun set_range range (Token (_, x)) = Token (range, x);
+
 fun pos_of (Token ((pos, _), _)) = pos;
 fun end_pos_of (Token ((_, pos), _)) = pos;
 
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -7,38 +7,38 @@
 signature ML_PARSE =
 sig
   val fix_ints: string -> string
+  val global_context: use_context
 end;
 
 structure ML_Parse: ML_PARSE =
 struct
 
-structure T = ML_Lex;
-
-
 (** error handling **)
 
 fun !!! scan =
   let
     fun get_pos [] = " (past end-of-file!)"
-      | get_pos (tok :: _) = Position.str_of (T.pos_of tok);
+      | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok);
 
     fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
       | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
   in Scan.!! err scan end;
 
 fun bad_input x =
-  (Scan.some (fn tok => (case T.kind_of tok of T.Error msg => SOME msg | _ => NONE)) :|--
+  (Scan.some (fn tok => (case ML_Lex.kind_of tok of ML_Lex.Error msg => SOME msg | _ => NONE)) :|--
     (fn msg => Scan.fail_with (K msg))) x;
 
 
 (** basic parsers **)
 
 fun $$$ x =
-  Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.content_of tok = x) >> T.content_of;
-val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.content_of;
+  Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Keyword andalso ML_Lex.content_of tok = x)
+    >> ML_Lex.content_of;
 
-val regular = Scan.one T.is_regular >> T.content_of;
-val improper = Scan.one T.is_improper >> T.content_of;
+val int = Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Int) >> ML_Lex.content_of;
+
+val regular = Scan.one ML_Lex.is_regular >> ML_Lex.content_of;
+val improper = Scan.one ML_Lex.is_improper >> ML_Lex.content_of;
 
 val blanks = Scan.repeat improper >> implode;
 
@@ -55,11 +55,21 @@
 
 fun do_fix_ints s =
   Source.of_string s
-  |> T.source
-  |> Source.source T.stopper (Scan.bulk (!!! fix_int)) NONE
+  |> ML_Lex.source
+  |> Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE
   |> Source.exhaust
   |> implode;
 
 val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
 
+
+(* global use_context *)
+
+val global_context: use_context =
+ {tune_source = fix_ints,
+  name_space = ML_Name_Space.global,
+  str_of_pos = Position.str_of oo Position.line_file,
+  print = writeln,
+  error = error};
+
 end;
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ML/ml_test.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -7,7 +7,7 @@
 signature ML_TEST =
 sig
   val get_result: Proof.context -> PolyML.parseTree list
-  val eval: bool -> bool -> Position.T -> ML_Lex.token list -> unit
+  val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
 
 structure ML_Test: ML_TEST =
@@ -25,9 +25,10 @@
 
 val get_result = Result.get o Context.Proof;
 
-fun eval do_run verbose pos toks =
+
+fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks =
   let
-    val (print, err) = Output.ml_output;
+    (* input *)
 
     val input = toks |> map (fn tok =>
       (serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok)));
@@ -51,50 +52,106 @@
            SOME c));
     fun get_index () = (case ! in_buffer of [] => 0 | (i, _) :: _ => i);
 
+
+    (* output *)
+
     val out_buffer = ref ([]: string list);
+    fun output () = implode (rev (! out_buffer));
     fun put s = out_buffer := s :: ! out_buffer;
-    fun output () = implode (rev (! out_buffer));
 
     fun put_message {message, hard, location, context = _} =
      (put (if hard then "Error: " else "Warning: ");
       put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
       put (Position.str_of (pos_of location) ^ "\n"));
 
+
+    (* results *)
+
+    fun apply_result {fixes, types, signatures, structures, functors, values} =
+      let
+        fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) =
+              let
+                fun make_prefix context =
+                  (case get_first (fn ContextParentStructure p => SOME p | _ => NONE) context of
+                    SOME (name, sub_context) => make_prefix sub_context ^ name ^ "."
+                  | NONE => prefix);
+                val this_prefix = make_prefix context;
+              in PrettyBlock (ind, consistent, context, map (add_prefix this_prefix) prts) end
+          | add_prefix prefix (prt as PrettyString s) =
+              if prefix = "" then prt else PrettyString (prefix ^ s)
+          | add_prefix _ (prt as PrettyBreak _) = prt;
+
+        val depth = get_print_depth ();
+        val with_struct = ! PolyML.Compiler.printTypesWithStructureName;
+
+        fun display disp x =
+          if depth > 0 then
+            (disp x
+              |> with_struct ? add_prefix ""
+              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
+          else ();
+
+        fun apply_fix (a, b) =
+          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
+        fun apply_type (a, b) =
+          (display PolyML.NameSpace.displayType (b, depth); #enterType space (a, b));
+        fun apply_sig (a, b) =
+          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
+        fun apply_struct (a, b) =
+          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
+        fun apply_funct (a, b) =
+          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
+        fun apply_val (a, b) =
+          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
+      in
+        List.app apply_fix fixes;
+        List.app apply_type types;
+        List.app apply_sig signatures;
+        List.app apply_struct structures;
+        List.app apply_funct functors;
+        List.app apply_val values
+      end;
+
     fun result_fun (parse_tree, code) () =
      (Context.>> (Result.map (append (the_list parse_tree)));
-      if is_none code then warning "Static Errors" else ());
+      (case code of NONE => error "Static Errors" | SOME result => apply_result (result ())));
+
+
+    (* compiler invocation *)
 
     val parameters =
      [PolyML.Compiler.CPOutStream put,
-      PolyML.Compiler.CPNameSpace ML_Context.name_space,
+      PolyML.Compiler.CPNameSpace space,
       PolyML.Compiler.CPErrorMessageProc put_message,
       PolyML.Compiler.CPLineNo (fn () => ! current_line),
       PolyML.Compiler.CPLineOffset get_index,
       PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
-     (if do_run then [] else [PolyML.Compiler.CPCompilerResultFun result_fun]);
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+      PolyML.Compiler.CPCompilerResultFun result_fun];
     val _ =
       (while not (List.null (! in_buffer)) do
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        err (output ()); raise exn);
+        error (output ()); raise exn);
   in if verbose then print (output ()) else () end;
 
+val eval = use_text ML_Context.local_context;
+
 
 (* ML test command *)
 
-fun ML_test do_run (txt, pos) =
+fun ML_test (txt, pos) =
   let
     val _ = Position.report Markup.ML_source pos;
     val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
     val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
 
     val _ = Context.setmp_thread_data env_ctxt
-        (fn () => (eval true false Position.none env; Context.thread_data ())) ()
+        (fn () => (eval false Position.none env; Context.thread_data ())) ()
       |> (fn NONE => () | SOME context' => Context.>> (ML_Context.inherit_env context'));
-    val _ = eval do_run true pos body;
-    val _ = eval true false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
+    val _ = eval true pos body;
+    val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
   in () end;
 
 
@@ -107,12 +164,7 @@
 val _ =
   OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
     (P.ML_source >> (fn src =>
-      Toplevel.generic_theory (ML_Context.exec (fn () => ML_test true src) #> inherit_env)));
-
-val _ =
-  OuterSyntax.command "ML_parse" "advanced ML compiler test (parse only)" (K.tag_ml K.thy_decl)
-    (P.ML_source >> (fn src =>
-      Toplevel.generic_theory (ML_Context.exec (fn () => ML_test false src) #> inherit_env)));
+      Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> inherit_env)));
 
 end;
 
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -76,7 +76,7 @@
 
 fun setup_messages () =
  (Output.writeln_fn := message "" "" "";
-  Output.status_fn := (fn s => ! Output.priority_fn s);
+  Output.status_fn := (fn _ => ());
   Output.priority_fn := message (special "I") (special "J") "";
   Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   Output.debug_fn := message (special "K") (special "L") "+++ ";
diff -r 182fb8d27b48 -r 5f0919630aaa src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -148,8 +148,8 @@
 fun eval_antiquote lex state (txt, pos) =
   let
     fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
-      | expand (Antiquote.Antiq x) =
-          let val (opts, src) = T.read_antiq lex antiq x in
+      | expand (Antiquote.Antiq (ss, (pos, _))) =
+          let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
             options opts (fn () => command src state) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings (options opts (fn () => command src state))) ()
diff -r 182fb8d27b48 -r 5f0919630aaa src/Tools/Compute_Oracle/am_compiler.ML
--- a/src/Tools/Compute_Oracle/am_compiler.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_compiler.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -185,7 +185,7 @@
 
     in
 	compiled_rewriter := NONE;	
-	use_text ML_Context.name_space (1, "") Output.ml_output false (!buffer);
+	use_text ML_Context.local_context (1, "") false (!buffer);
 	case !compiled_rewriter of 
 	    NONE => raise (Compile "cannot communicate with compiled function")
 	  | SOME r => (compiled_rewriter := NONE; r)
diff -r 182fb8d27b48 -r 5f0919630aaa src/Tools/Compute_Oracle/am_sml.ML
--- a/src/Tools/Compute_Oracle/am_sml.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -492,7 +492,7 @@
 
 fun writeTextFile name s = File.write (Path.explode name) s
 
-fun use_source src = use_text ML_Context.name_space (1, "") Output.ml_output false src
+fun use_source src = use_text ML_Context.local_context (1, "") false src
     
 fun compile cache_patterns const_arity eqs = 
     let
diff -r 182fb8d27b48 -r 5f0919630aaa src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Tools/code/code_ml.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -969,7 +969,7 @@
         val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
-      in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
+      in ML_Context.evaluate ctxt false reff sml_code end;
   in eval'' thy (rpair eval') ct end;
 
 fun eval_term reff = eval Code_Thingol.eval_term I reff;
@@ -1037,7 +1037,7 @@
 fun isar_seri_sml module_name =
   Code_Target.parse_args (Scan.succeed ())
   #> (fn () => serialize_ml target_SML
-      (SOME (use_text ML_Context.name_space (1, "generated code") Output.ml_output false))
+      (SOME (use_text ML_Context.local_context (1, "generated code") false))
       pr_sml_module pr_sml_stmt module_name);
 
 fun isar_seri_ocaml module_name =
diff -r 182fb8d27b48 -r 5f0919630aaa src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Mar 24 09:15:59 2009 +0100
+++ b/src/Tools/nbe.ML	Tue Mar 24 12:01:12 2009 +0100
@@ -277,14 +277,12 @@
       in
         s
         |> tracing (fn s => "\n--- code to be evaluated:\n" ^ s)
-        |> ML_Context.evaluate ctxt
-            (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
-            Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n")
-            (!trace) univs_cookie
+        |> ML_Context.evaluate ctxt (!trace) univs_cookie
         |> (fn f => f deps_vals)
         |> (fn univs => cs ~~ univs)
       end;
 
+
 (* preparing function equations *)
 
 fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) =