# HG changeset patch
# User wenzelm
# Date 1460040823 -7200
# Node ID 3c0f53eae16632d4996f2f57061b39578671fe56
# Parent  0951d6cec68c5cc34895380b6ea54c2611645bc9
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;

diff -r 0951d6cec68c -r 3c0f53eae166 src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -184,7 +184,7 @@
 
     in
         compiled_rewriter := NONE;      
-        ML_Compiler0.use_text ML_Env.context
+        ML_Compiler0.ML ML_Env.context
           {line = 1, file = "", verbose = false, debug = false} (!buffer);
         case !compiled_rewriter of 
             NONE => raise (Compile "cannot communicate with compiled function")
diff -r 0951d6cec68c -r 3c0f53eae166 src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -486,7 +486,7 @@
 fun writeTextFile name s = File.write (Path.explode name) s
 
 fun use_source src =
-  ML_Compiler0.use_text ML_Env.context
+  ML_Compiler0.ML ML_Env.context
     {line = 1, file = "", verbose = false, debug = false} src
     
 fun compile rules = 
diff -r 0951d6cec68c -r 3c0f53eae166 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -206,7 +206,7 @@
 
 fun exec verbose code =
   ML_Context.exec (fn () =>
-    ML_Compiler0.use_text ML_Env.context
+    ML_Compiler0.ML ML_Env.context
       {line = 0, file = "generated code", verbose = verbose, debug = false} code)
 
 fun with_overlord_dir name f =
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -7,7 +7,7 @@
 signature ML_COMPILER =
 sig
   type flags =
-    {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
+    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
       debug: bool option, writeln: string -> unit, warning: string -> unit}
   val debug_flags: bool option -> flags
   val flags: flags
@@ -21,19 +21,18 @@
 (* flags *)
 
 type flags =
-  {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
+  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
 
 fun debug_flags opt_debug : flags =
-  {SML_syntax = false, SML_env = false, exchange = false, redirect = false, verbose = false,
+  {SML = false, exchange = false, redirect = false, verbose = false,
     debug = opt_debug, writeln = writeln, warning = warning};
 
 val flags = debug_flags NONE;
 
 fun verbose b (flags: flags) =
-  {SML_syntax = #SML_syntax flags, SML_env = #SML_env flags, exchange = #exchange flags,
-    redirect = #redirect flags, verbose = b, debug = #debug flags,
-    writeln = #writeln flags, warning = #warning flags};
+  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
+    debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
 
 
 (* parse trees *)
@@ -145,7 +144,7 @@
 
 fun eval (flags: flags) pos toks =
   let
-    val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
+    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
     val opt_context = Context.get_generic_context ();
 
 
@@ -154,7 +153,7 @@
     val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
     val input_explode =
-      if #SML_syntax flags then String.explode
+      if #SML flags then String.explode
       else maps (String.explode o Symbol.esc) o Symbol.explode;
 
     val input_buffer =
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -2,7 +2,7 @@
     Author:     Makarius
 
 Runtime compilation and evaluation for bootstrap.
-Initial ML use operations.
+Initial ML file operations.
 *)
 
 signature ML_COMPILER0 =
@@ -15,11 +15,11 @@
     print: string -> unit,
     error: string -> unit}
   val make_context: ML_Name_Space.T -> context
-  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
-  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
+  val ML: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
+  val ML_file: context -> {debug: bool, verbose: bool} -> string -> unit
   val debug_option: bool option -> bool
-  val use_operations: (bool option -> string -> unit) ->
-    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
+  val ML_file_operations: (bool option -> string -> unit) ->
+    {ML_file: string -> unit, ML_file_debug: string -> unit, ML_file_no_debug: string -> unit}
 end;
 
 structure ML_Compiler0: ML_COMPILER0 =
@@ -53,7 +53,7 @@
   error = fn s => error s};
 
 
-(* use operations *)
+(* ML file operations *)
 
 local
 
@@ -77,8 +77,7 @@
 
 in
 
-fun use_text ({name_space, print_depth, here, print, error, ...}: context)
-    {line, file, verbose, debug} text =
+fun ML {name_space, print_depth, here, print, error, ...} {line, file, verbose, debug} text =
   let
     val current_line = Unsynchronized.ref line;
     val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
@@ -118,14 +117,14 @@
 
 end;
 
-fun use_file context {verbose, debug} file =
+fun ML_file context {verbose, debug} file =
   let
     val instream = TextIO.openIn file;
     val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
+  in ML context {line = 1, file = file, verbose = verbose, debug = debug} text end;
 
-fun use_operations (use_ : bool option -> string -> unit) =
-  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
+fun ML_file_operations (f: bool option -> string -> unit) =
+  {ML_file = f NONE, ML_file_debug = f (SOME true), ML_file_no_debug = f (SOME false)};
 
 
 fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
@@ -134,12 +133,12 @@
 end;
 
 
-(* initial use operations *)
+(* initial ML_file operations *)
 
-val {use, use_debug, use_no_debug} =
+val {ML_file, ML_file_debug, ML_file_no_debug} =
   let val context = ML_Compiler0.make_context ML_Name_Space.global in
-    ML_Compiler0.use_operations (fn opt_debug => fn file =>
-      ML_Compiler0.use_file context
+    ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
+      ML_Compiler0.ML_file context
         {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
       handle ERROR msg => (#print context msg; raise error "ML error"))
   end;
@@ -149,7 +148,7 @@
 
 if Thread_Data.is_virtual then ()
 else
-  ML_Compiler0.use_text
+  ML_Compiler0.ML
     (ML_Compiler0.make_context
       (ML_Name_Space.global_values
         [("prettyRepresentation", "ML_system_pretty"),
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_compiler1.ML
--- a/src/Pure/ML/ml_compiler1.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_compiler1.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -1,10 +1,10 @@
 (*  Title:      Pure/ML/ml_compiler1.ML
     Author:     Makarius
 
-Refined ML use operations for bootstrap.
+Refined ML file operations for bootstrap.
 *)
 
-val {use, use_debug, use_no_debug} =
+val {ML_file, ML_file_debug, ML_file_no_debug} =
   let
     val context: ML_Compiler0.context =
      {name_space = ML_Name_Space.global,
@@ -13,10 +13,10 @@
       print = writeln,
       error = error};
   in
-    ML_Compiler0.use_operations (fn opt_debug => fn file =>
+    ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
       Position.setmp_thread_data (Position.file_only file)
         (fn () =>
-          ML_Compiler0.use_file context
+          ML_Compiler0.ML_file context
             {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
           handle ERROR msg => (writeln msg; error "ML error")) ())
   end;
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_compiler2.ML
--- a/src/Pure/ML/ml_compiler2.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_compiler2.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -1,11 +1,11 @@
 (*  Title:      Pure/ML/ml_compiler2.ML
     Author:     Makarius
 
-Isabelle/ML use operations.
+Isabelle/ML file operations.
 *)
 
-val {use, use_debug, use_no_debug} =
-  ML_Compiler0.use_operations (fn opt_debug => fn file =>
+val {ML_file, ML_file_debug, ML_file_no_debug} =
+  ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
     let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
       ML_Context.eval_file flags (Path.explode file)
         handle ERROR msg => (writeln msg; error "ML error")
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -210,7 +210,7 @@
   in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
 
 fun eval_source flags source =
-  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
+  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
 
 fun eval_in ctxt flags pos ants =
   Context.setmp_generic_context (Option.map Context.Proof ctxt)
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -13,6 +13,7 @@
     Context.generic -> Context.generic
   val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
   val init_bootstrap: Context.generic -> Context.generic
+  val SML_environment: bool Config.T
   val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
   val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
   val context: ML_Compiler0.context
@@ -91,6 +92,18 @@
 val get_breakpoint = Inttab.lookup o #breakpoints o Env.get;
 
 
+(* SML environment for Isabelle/ML *)
+
+val SML_environment =
+  Config.bool (Config.declare ("SML_environment", @{here}) (fn _ => Config.Bool false));
+
+fun sml_env SML =
+  SML orelse
+    (case Context.get_generic_context () of
+      NONE => false
+    | SOME context => Config.get_generic context SML_environment);
+
+
 (* name space *)
 
 val init_bootstrap =
@@ -114,7 +127,7 @@
   Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
     let
       val (tables', sml_tables') =
-        (tables, sml_tables) |> (if SML then apsnd else apfst)
+        (tables, sml_tables) |> (if sml_env SML then apsnd else apfst)
           (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
             let
               val val2 = fold Symtab.update (#allVal space ()) val1;
@@ -129,7 +142,7 @@
 fun make_name_space {SML, exchange} : ML_Name_Space.T =
   let
     fun lookup sel1 sel2 name =
-      if SML then
+      if sml_env SML then
         Context.the_generic_context ()
         |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
       else
@@ -138,7 +151,7 @@
         |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
 
     fun all sel1 sel2 () =
-      (if SML then
+      (if sml_env SML then
         Context.the_generic_context ()
         |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
       else
@@ -148,7 +161,7 @@
       |> sort_distinct (string_ord o apply2 #1);
 
     fun enter ap1 sel2 entry =
-      if SML <> exchange then
+      if sml_env SML <> exchange then
         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
           let val sml_tables' = ap1 (Symtab.update entry) sml_tables
           in make_data (bootstrap, tables, sml_tables', breakpoints) end))
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_file.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -8,7 +8,6 @@
 sig
   val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
   val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
-  val use: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure ML_File: ML_FILE =
@@ -19,10 +18,9 @@
     val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
-    val (SML_syntax, SML_env) = SML src_path;
     val flags =
-      {SML_syntax = SML_syntax, SML_env = SML_env, exchange = false, redirect = true,
-        verbose = true, debug = debug, writeln = writeln, warning = warning};
+      {SML = SML, exchange = false, redirect = true, verbose = true,
+        debug = debug, writeln = writeln, warning = warning};
   in
     gthy
     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
@@ -30,17 +28,7 @@
     |> Context.mapping provide (Local_Theory.background_theory provide)
   end);
 
-val ML = command (K (false, false));
-val SML = command (K (true, true));
-
-val use =
-  command (fn path =>
-    (case try (#2 o Path.split_ext) path of
-      SOME "ML" => (false, true)
-    | SOME "sml" => (true, true)
-    | SOME "sig" => (true, true)
-    | _ =>
-        error ("Bad file name " ^ Path.print path ^
-          "\nExpected .ML for Isabelle/ML or .sml/.sig for Standard ML")));
+val ML = command false;
+val SML = command true;
 
 end;
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -61,7 +61,7 @@
   (* bootstrap environment *)
 
   val bootstrap_values =
-    ["use", "exit", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
+    ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
   val bootstrap_structures =
     ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data"];
 
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_pervasive1.ML
--- a/src/Pure/ML/ml_pervasive1.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_pervasive1.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -12,3 +12,5 @@
 Proofterm.proofs := 0;
 
 Context.put_generic_context NONE;
+
+val use = ML_file;
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_root.scala
--- a/src/Pure/ML/ml_root.scala	Thu Apr 07 15:32:47 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-/*  Title:      Pure/ML/ml_root.scala
-    Author:     Makarius
-
-Support for ML project ROOT file, with imitation of ML "use" commands.
-*/
-
-package isabelle
-
-
-object ML_Root
-{
-  /* parser */
-
-  val USE = "use"
-  val USE_DEBUG = "use_debug"
-  val USE_NO_DEBUG = "use_no_debug"
-  val USE_THY = "use_thy"
-
-  lazy val syntax =
-    Outer_Syntax.init() + ";" +
-      (USE, Some((Keyword.THY_LOAD, Nil)), None) +
-      (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
-      (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
-      (USE_THY, Some((Keyword.THY_LOAD, List("thy"))), None)
-
-  private object Parser extends Parse.Parser
-  {
-    val entry: Parser[Path] =
-      command(USE_THY) ~! string ^^
-        { case _ ~ a => Resources.thy_path(Path.explode(a)) } |
-      (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG)) ~! string ^^
-        { case _ ~ a => Path.explode(a) }
-
-    val entries: Parser[List[Path]] =
-      rep(entry <~ $$$(";"))
-  }
-
-  def read_files(root: Path): List[Path] =
-  {
-    val toks = Token.explode(syntax.keywords, File.read(root))
-    val start = Token.Pos.file(root.implode)
-
-    Parser.parse_all(Parser.entries, Token.reader(toks, start)) match {
-      case Parser.Success(entries, _) => entries
-      case bad => error(bad.toString)
-    }
-  }
-}
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML_Bootstrap.thy
--- a/src/Pure/ML_Bootstrap.thy	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML_Bootstrap.thy	Thu Apr 07 16:53:43 2016 +0200
@@ -6,31 +6,10 @@
 
 theory ML_Bootstrap
 imports Pure
-keywords "use" "use_debug" "use_no_debug" :: thy_load
 begin
 
 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
 SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close>
-
-ML \<open>
-local
-
-val _ =
-  Outer_Syntax.command @{command_keyword use}
-    "read and evaluate Isabelle/ML or SML file"
-    (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
-
-val _ =
-  Outer_Syntax.command @{command_keyword use_debug}
-    "read and evaluate Isabelle/ML or SML file (with debugger information)"
-    (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
-
-val _ =
-  Outer_Syntax.command @{command_keyword use_no_debug}
-    "read and evaluate Isabelle/ML or SML file (no debugger information)"
-    (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
-
-in end
-\<close>
+setup \<open>Config.put_global ML_Env.SML_environment true\<close>
 
 end
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 07 16:53:43 2016 +0200
@@ -100,41 +100,43 @@
 ML \<open>
 local
 
+val semi = Scan.option @{keyword ";"};
+
 val _ =
   Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
-    (Resources.parse_files "ML_file" >> ML_File.ML NONE);
+    (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE);
 
 val _ =
   Outer_Syntax.command @{command_keyword ML_file_debug}
     "read and evaluate Isabelle/ML file (with debugger information)"
-    (Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true));
+    (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true));
 
 val _ =
   Outer_Syntax.command @{command_keyword ML_file_no_debug}
     "read and evaluate Isabelle/ML file (no debugger information)"
-    (Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false));
+    (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false));
 
 val _ =
   Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
-    (Resources.parse_files "SML_file" >> ML_File.SML NONE);
+    (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE);
 
 val _ =
   Outer_Syntax.command @{command_keyword SML_file_debug}
     "read and evaluate Standard ML file (with debugger information)"
-    (Resources.parse_files "SML_file_debug" >> ML_File.SML (SOME true));
+    (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true));
 
 val _ =
   Outer_Syntax.command @{command_keyword SML_file_no_debug}
     "read and evaluate Standard ML file (no debugger information)"
-    (Resources.parse_files "SML_file_no_debug" >> ML_File.SML (SOME false));
+    (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false));
 
 val _ =
   Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
-            verbose = true, debug = NONE, writeln = writeln, warning = warning};
+          {SML = true, exchange = true, redirect = false, verbose = true,
+            debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -145,8 +147,8 @@
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
-            verbose = true, debug = NONE, writeln = writeln, warning = warning};
+          {SML = false, exchange = true, redirect = false, verbose = true,
+            debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ROOT.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -1,25 +1,25 @@
 (*** Isabelle/Pure bootstrap ***)
 
-use "ML/ml_name_space.ML";
+ML_file "ML/ml_name_space.ML";
 
 
 (** bootstrap phase 0: Poly/ML setup **)
 
-use "ML/ml_pervasive0.ML";
-use "ML/ml_system.ML";
-use "System/distribution.ML";
+ML_file "ML/ml_pervasive0.ML";
+ML_file "ML/ml_system.ML";
+ML_file "System/distribution.ML";
 
-use "General/exn.ML";
+ML_file "General/exn.ML";
 
-use "Concurrent/multithreading.ML";
-use "Concurrent/unsynchronized.ML";
+ML_file "Concurrent/multithreading.ML";
+ML_file "Concurrent/unsynchronized.ML";
 
-use "ML/ml_heap.ML";
-use "ML/ml_profiling.ML";
-use "ML/ml_print_depth0.ML";
-use "ML/ml_pretty.ML";
-use "ML/ml_compiler0.ML";
-use_no_debug "ML/ml_debugger.ML";
+ML_file "ML/ml_heap.ML";
+ML_file "ML/ml_profiling.ML";
+ML_file "ML/ml_print_depth0.ML";
+ML_file "ML/ml_pretty.ML";
+ML_file "ML/ml_compiler0.ML";
+ML_file_no_debug "ML/ml_debugger.ML";
 
 
 
@@ -27,307 +27,307 @@
 
 (* library of general tools *)
 
-use "General/basics.ML";
-use "library.ML";
-use "General/print_mode.ML";
-use "General/alist.ML";
-use "General/table.ML";
+ML_file "General/basics.ML";
+ML_file "library.ML";
+ML_file "General/print_mode.ML";
+ML_file "General/alist.ML";
+ML_file "General/table.ML";
 
-use "Concurrent/synchronized.ML";
-use "Concurrent/counter.ML";
+ML_file "Concurrent/synchronized.ML";
+ML_file "Concurrent/counter.ML";
 
-use "General/random.ML";
-use "General/properties.ML";
-use "General/output.ML";
-use "PIDE/markup.ML";
-use "General/scan.ML";
-use "General/source.ML";
-use "General/symbol.ML";
-use "General/position.ML";
-use "General/symbol_pos.ML";
-use "General/input.ML";
-use "General/antiquote.ML";
-use "ML/ml_lex.ML";
-use "ML/ml_compiler1.ML";
+ML_file "General/random.ML";
+ML_file "General/properties.ML";
+ML_file "General/output.ML";
+ML_file "PIDE/markup.ML";
+ML_file "General/scan.ML";
+ML_file "General/source.ML";
+ML_file "General/symbol.ML";
+ML_file "General/position.ML";
+ML_file "General/symbol_pos.ML";
+ML_file "General/input.ML";
+ML_file "General/antiquote.ML";
+ML_file "ML/ml_lex.ML";
+ML_file "ML/ml_compiler1.ML";
 
 
 (** bootstrap phase 2: towards ML within Isar context *)
 
 (* library of general tools *)
 
-use "General/integer.ML";
-use "General/stack.ML";
-use "General/queue.ML";
-use "General/heap.ML";
-use "General/same.ML";
-use "General/ord_list.ML";
-use "General/balanced_tree.ML";
-use "General/linear_set.ML";
-use "General/buffer.ML";
-use "General/pretty.ML";
-use "PIDE/xml.ML";
-use "General/path.ML";
-use "General/url.ML";
-use "General/file.ML";
-use "General/long_name.ML";
-use "General/binding.ML";
-use "General/socket_io.ML";
-use "General/seq.ML";
-use "General/timing.ML";
-use "General/sha1.ML";
+ML_file "General/integer.ML";
+ML_file "General/stack.ML";
+ML_file "General/queue.ML";
+ML_file "General/heap.ML";
+ML_file "General/same.ML";
+ML_file "General/ord_list.ML";
+ML_file "General/balanced_tree.ML";
+ML_file "General/linear_set.ML";
+ML_file "General/buffer.ML";
+ML_file "General/pretty.ML";
+ML_file "PIDE/xml.ML";
+ML_file "General/path.ML";
+ML_file "General/url.ML";
+ML_file "General/file.ML";
+ML_file "General/long_name.ML";
+ML_file "General/binding.ML";
+ML_file "General/socket_io.ML";
+ML_file "General/seq.ML";
+ML_file "General/timing.ML";
+ML_file "General/sha1.ML";
 
-use "PIDE/yxml.ML";
-use "PIDE/document_id.ML";
+ML_file "PIDE/yxml.ML";
+ML_file "PIDE/document_id.ML";
 
-use "General/change_table.ML";
-use "General/graph.ML";
+ML_file "General/change_table.ML";
+ML_file "General/graph.ML";
 
 
 (* fundamental structures *)
 
-use "name.ML";
-use "term.ML";
-use "context.ML";
-use "context_position.ML";
-use "System/options.ML";
-use "config.ML";
+ML_file "name.ML";
+ML_file "term.ML";
+ML_file "context.ML";
+ML_file "context_position.ML";
+ML_file "System/options.ML";
+ML_file "config.ML";
 
 
 (* concurrency within the ML runtime *)
 
-use "ML/exn_properties.ML";
+ML_file "ML/exn_properties.ML";
 
-use "ML/ml_statistics.ML";
+ML_file "ML/ml_statistics.ML";
 
-use "Concurrent/thread_data_virtual.ML";
-use "Concurrent/standard_thread.ML";
-use "Concurrent/single_assignment.ML";
+ML_file "Concurrent/thread_data_virtual.ML";
+ML_file "Concurrent/standard_thread.ML";
+ML_file "Concurrent/single_assignment.ML";
 
-use "Concurrent/par_exn.ML";
-use "Concurrent/task_queue.ML";
-use "Concurrent/future.ML";
-use "Concurrent/event_timer.ML";
-use "Concurrent/timeout.ML";
-use "Concurrent/lazy.ML";
-use "Concurrent/par_list.ML";
+ML_file "Concurrent/par_exn.ML";
+ML_file "Concurrent/task_queue.ML";
+ML_file "Concurrent/future.ML";
+ML_file "Concurrent/event_timer.ML";
+ML_file "Concurrent/timeout.ML";
+ML_file "Concurrent/lazy.ML";
+ML_file "Concurrent/par_list.ML";
 
-use "Concurrent/mailbox.ML";
-use "Concurrent/cache.ML";
+ML_file "Concurrent/mailbox.ML";
+ML_file "Concurrent/cache.ML";
 
-use "PIDE/active.ML";
+ML_file "PIDE/active.ML";
 
 
 (* inner syntax *)
 
-use "Syntax/type_annotation.ML";
-use "Syntax/term_position.ML";
-use "Syntax/lexicon.ML";
-use "Syntax/ast.ML";
-use "Syntax/syntax_ext.ML";
-use "Syntax/parser.ML";
-use "Syntax/syntax_trans.ML";
-use "Syntax/mixfix.ML";
-use "Syntax/printer.ML";
-use "Syntax/syntax.ML";
+ML_file "Syntax/type_annotation.ML";
+ML_file "Syntax/term_position.ML";
+ML_file "Syntax/lexicon.ML";
+ML_file "Syntax/ast.ML";
+ML_file "Syntax/syntax_ext.ML";
+ML_file "Syntax/parser.ML";
+ML_file "Syntax/syntax_trans.ML";
+ML_file "Syntax/mixfix.ML";
+ML_file "Syntax/printer.ML";
+ML_file "Syntax/syntax.ML";
 
 
 (* core of tactical proof system *)
 
-use "term_ord.ML";
-use "term_subst.ML";
-use "term_xml.ML";
-use "General/completion.ML";
-use "General/name_space.ML";
-use "sorts.ML";
-use "type.ML";
-use "logic.ML";
-use "Syntax/simple_syntax.ML";
-use "net.ML";
-use "item_net.ML";
-use "envir.ML";
-use "consts.ML";
-use "primitive_defs.ML";
-use "sign.ML";
-use "defs.ML";
-use "term_sharing.ML";
-use "pattern.ML";
-use "unify.ML";
-use "theory.ML";
-use "proofterm.ML";
-use "thm.ML";
-use "more_pattern.ML";
-use "more_unify.ML";
-use "more_thm.ML";
-use "facts.ML";
-use "global_theory.ML";
-use "pure_thy.ML";
-use "drule.ML";
-use "morphism.ML";
-use "variable.ML";
-use "conv.ML";
-use "goal_display.ML";
-use "tactical.ML";
-use "search.ML";
-use "tactic.ML";
-use "raw_simplifier.ML";
-use "conjunction.ML";
-use "assumption.ML";
+ML_file "term_ord.ML";
+ML_file "term_subst.ML";
+ML_file "term_xml.ML";
+ML_file "General/completion.ML";
+ML_file "General/name_space.ML";
+ML_file "sorts.ML";
+ML_file "type.ML";
+ML_file "logic.ML";
+ML_file "Syntax/simple_syntax.ML";
+ML_file "net.ML";
+ML_file "item_net.ML";
+ML_file "envir.ML";
+ML_file "consts.ML";
+ML_file "primitive_defs.ML";
+ML_file "sign.ML";
+ML_file "defs.ML";
+ML_file "term_sharing.ML";
+ML_file "pattern.ML";
+ML_file "unify.ML";
+ML_file "theory.ML";
+ML_file "proofterm.ML";
+ML_file "thm.ML";
+ML_file "more_pattern.ML";
+ML_file "more_unify.ML";
+ML_file "more_thm.ML";
+ML_file "facts.ML";
+ML_file "global_theory.ML";
+ML_file "pure_thy.ML";
+ML_file "drule.ML";
+ML_file "morphism.ML";
+ML_file "variable.ML";
+ML_file "conv.ML";
+ML_file "goal_display.ML";
+ML_file "tactical.ML";
+ML_file "search.ML";
+ML_file "tactic.ML";
+ML_file "raw_simplifier.ML";
+ML_file "conjunction.ML";
+ML_file "assumption.ML";
 
 
 (* Isar -- Intelligible Semi-Automated Reasoning *)
 
 (*ML support and global execution*)
-use "ML/ml_syntax.ML";
-use "ML/ml_env.ML";
-use "ML/ml_options.ML";
-use "ML/ml_print_depth.ML";
-use_no_debug "ML/exn_debugger.ML";
-use_no_debug "Isar/runtime.ML";
-use "PIDE/execution.ML";
-use "ML/ml_compiler.ML";
+ML_file "ML/ml_syntax.ML";
+ML_file "ML/ml_env.ML";
+ML_file "ML/ml_options.ML";
+ML_file "ML/ml_print_depth.ML";
+ML_file_no_debug "ML/exn_debugger.ML";
+ML_file_no_debug "Isar/runtime.ML";
+ML_file "PIDE/execution.ML";
+ML_file "ML/ml_compiler.ML";
 
-use "skip_proof.ML";
-use "goal.ML";
+ML_file "skip_proof.ML";
+ML_file "goal.ML";
 
 (*proof context*)
-use "Isar/object_logic.ML";
-use "Isar/rule_cases.ML";
-use "Isar/auto_bind.ML";
-use "type_infer.ML";
-use "Syntax/local_syntax.ML";
-use "Isar/proof_context.ML";
-use "type_infer_context.ML";
-use "Syntax/syntax_phases.ML";
-use "Isar/local_defs.ML";
+ML_file "Isar/object_logic.ML";
+ML_file "Isar/rule_cases.ML";
+ML_file "Isar/auto_bind.ML";
+ML_file "type_infer.ML";
+ML_file "Syntax/local_syntax.ML";
+ML_file "Isar/proof_context.ML";
+ML_file "type_infer_context.ML";
+ML_file "Syntax/syntax_phases.ML";
+ML_file "Isar/local_defs.ML";
 
 (*outer syntax*)
-use "Isar/keyword.ML";
-use "Isar/token.ML";
-use "Isar/parse.ML";
-use "Isar/args.ML";
+ML_file "Isar/keyword.ML";
+ML_file "Isar/token.ML";
+ML_file "Isar/parse.ML";
+ML_file "Isar/args.ML";
 
 (*theory specifications*)
-use "Isar/local_theory.ML";
-use "Thy/thy_header.ML";
-use "PIDE/command_span.ML";
-use "Thy/thy_syntax.ML";
-use "Thy/markdown.ML";
-use "Thy/html.ML";
-use "Thy/latex.ML";
+ML_file "Isar/local_theory.ML";
+ML_file "Thy/thy_header.ML";
+ML_file "PIDE/command_span.ML";
+ML_file "Thy/thy_syntax.ML";
+ML_file "Thy/markdown.ML";
+ML_file "Thy/html.ML";
+ML_file "Thy/latex.ML";
 
 (*ML with context and antiquotations*)
-use "ML/ml_context.ML";
-use "ML/ml_antiquotation.ML";
-use "ML/ml_compiler2.ML";
+ML_file "ML/ml_context.ML";
+ML_file "ML/ml_antiquotation.ML";
+ML_file "ML/ml_compiler2.ML";
 
 
 
 (** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *)
 
 (*basic proof engine*)
-use "par_tactical.ML";
-use "Isar/proof_display.ML";
-use "Isar/attrib.ML";
-use "Isar/context_rules.ML";
-use "Isar/method.ML";
-use "Isar/proof.ML";
-use "Isar/element.ML";
-use "Isar/obtain.ML";
-use "Isar/subgoal.ML";
-use "Isar/calculation.ML";
+ML_file "par_tactical.ML";
+ML_file "Isar/proof_display.ML";
+ML_file "Isar/attrib.ML";
+ML_file "Isar/context_rules.ML";
+ML_file "Isar/method.ML";
+ML_file "Isar/proof.ML";
+ML_file "Isar/element.ML";
+ML_file "Isar/obtain.ML";
+ML_file "Isar/subgoal.ML";
+ML_file "Isar/calculation.ML";
 
 (*local theories and targets*)
-use "Isar/locale.ML";
-use "Isar/generic_target.ML";
-use "Isar/overloading.ML";
-use "axclass.ML";
-use "Isar/class.ML";
-use "Isar/named_target.ML";
-use "Isar/expression.ML";
-use "Isar/interpretation.ML";
-use "Isar/class_declaration.ML";
-use "Isar/bundle.ML";
-use "Isar/experiment.ML";
+ML_file "Isar/locale.ML";
+ML_file "Isar/generic_target.ML";
+ML_file "Isar/overloading.ML";
+ML_file "axclass.ML";
+ML_file "Isar/class.ML";
+ML_file "Isar/named_target.ML";
+ML_file "Isar/expression.ML";
+ML_file "Isar/interpretation.ML";
+ML_file "Isar/class_declaration.ML";
+ML_file "Isar/bundle.ML";
+ML_file "Isar/experiment.ML";
 
-use "simplifier.ML";
-use "Tools/plugin.ML";
+ML_file "simplifier.ML";
+ML_file "Tools/plugin.ML";
 
 (*executable theory content*)
-use "Isar/code.ML";
+ML_file "Isar/code.ML";
 
 (*specifications*)
-use "Isar/parse_spec.ML";
-use "Isar/spec_rules.ML";
-use "Isar/specification.ML";
-use "Isar/typedecl.ML";
+ML_file "Isar/parse_spec.ML";
+ML_file "Isar/spec_rules.ML";
+ML_file "Isar/specification.ML";
+ML_file "Isar/typedecl.ML";
 
 (*toplevel transactions*)
-use "Isar/proof_node.ML";
-use "Isar/toplevel.ML";
+ML_file "Isar/proof_node.ML";
+ML_file "Isar/toplevel.ML";
 
 (*proof term operations*)
-use "Proof/reconstruct.ML";
-use "Proof/proof_syntax.ML";
-use "Proof/proof_rewrite_rules.ML";
-use "Proof/proof_checker.ML";
-use "Proof/extraction.ML";
+ML_file "Proof/reconstruct.ML";
+ML_file "Proof/proof_syntax.ML";
+ML_file "Proof/proof_rewrite_rules.ML";
+ML_file "Proof/proof_checker.ML";
+ML_file "Proof/extraction.ML";
 
 (*Isabelle system*)
-use "System/$ISABELLE_WINDOWS_PREFIX/bash.ML";
-use "System/isabelle_system.ML";
+ML_file "System/$ISABELLE_WINDOWS_PREFIX/bash.ML";
+ML_file "System/isabelle_system.ML";
 
 
 (*theory documents*)
-use "Thy/term_style.ML";
-use "Isar/outer_syntax.ML";
-use "Thy/thy_output.ML";
-use "Thy/document_antiquotations.ML";
-use "General/graph_display.ML";
-use "Thy/present.ML";
-use "pure_syn.ML";
-use "PIDE/command.ML";
-use "PIDE/query_operation.ML";
-use "PIDE/resources.ML";
-use "Thy/thy_info.ML";
-use "PIDE/session.ML";
-use "PIDE/protocol_message.ML";
-use "PIDE/document.ML";
+ML_file "Thy/term_style.ML";
+ML_file "Isar/outer_syntax.ML";
+ML_file "Thy/thy_output.ML";
+ML_file "Thy/document_antiquotations.ML";
+ML_file "General/graph_display.ML";
+ML_file "Thy/present.ML";
+ML_file "pure_syn.ML";
+ML_file "PIDE/command.ML";
+ML_file "PIDE/query_operation.ML";
+ML_file "PIDE/resources.ML";
+ML_file "Thy/thy_info.ML";
+ML_file "PIDE/session.ML";
+ML_file "PIDE/protocol_message.ML";
+ML_file "PIDE/document.ML";
 
 (*theory and proof operations*)
-use "Isar/isar_cmd.ML";
+ML_file "Isar/isar_cmd.ML";
 
 
 (* Isabelle/Isar system *)
 
-use "System/command_line.ML";
-use "System/system_channel.ML";
-use "System/message_channel.ML";
-use "System/isabelle_process.ML";
-use "System/invoke_scala.ML";
-use "PIDE/protocol.ML";
+ML_file "System/command_line.ML";
+ML_file "System/system_channel.ML";
+ML_file "System/message_channel.ML";
+ML_file "System/isabelle_process.ML";
+ML_file "System/invoke_scala.ML";
+ML_file "PIDE/protocol.ML";
 
 
 (* miscellaneous tools and packages for Pure Isabelle *)
 
-use "ML/ml_pp.ML";
-use "ML/ml_antiquotations.ML";
-use "ML/ml_thms.ML";
-use "ML/ml_file.ML";
+ML_file "ML/ml_pp.ML";
+ML_file "ML/ml_antiquotations.ML";
+ML_file "ML/ml_thms.ML";
+ML_file "ML/ml_file.ML";
 
-use "Tools/build.ML";
-use "Tools/named_thms.ML";
-use "Tools/print_operation.ML";
-use "Tools/bibtex.ML";
-use "Tools/rail.ML";
-use "Tools/rule_insts.ML";
-use "Tools/thm_deps.ML";
-use "Tools/thy_deps.ML";
-use "Tools/class_deps.ML";
-use "Tools/find_theorems.ML";
-use "Tools/find_consts.ML";
-use "Tools/simplifier_trace.ML";
-use_no_debug "Tools/debugger.ML";
-use "Tools/named_theorems.ML";
-use "Tools/jedit.ML";
+ML_file "Tools/build.ML";
+ML_file "Tools/named_thms.ML";
+ML_file "Tools/print_operation.ML";
+ML_file "Tools/bibtex.ML";
+ML_file "Tools/rail.ML";
+ML_file "Tools/rule_insts.ML";
+ML_file "Tools/thm_deps.ML";
+ML_file "Tools/thy_deps.ML";
+ML_file "Tools/class_deps.ML";
+ML_file "Tools/find_theorems.ML";
+ML_file "Tools/find_consts.ML";
+ML_file "Tools/simplifier_trace.ML";
+ML_file_no_debug "Tools/debugger.ML";
+ML_file "Tools/named_theorems.ML";
+ML_file "Tools/jedit.ML";
 
 (* :mode=isabelle: *)
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ROOT0.ML
--- a/src/Pure/ROOT0.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ROOT0.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -1,3 +1,3 @@
 (*** Isabelle/Pure bootstrap: initial setup ***)
 
-use "Concurrent/thread_data.ML";
+ML_file "Concurrent/thread_data.ML";
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ROOT1.ML
--- a/src/Pure/ROOT1.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ROOT1.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -3,4 +3,4 @@
 use_thy "Pure";
 use_thy "ML_Bootstrap";
 
-use "ML/ml_pervasive1.ML";
+ML_file "ML/ml_pervasive1.ML";
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 07 16:53:43 2016 +0200
@@ -20,10 +20,15 @@
 
   def pure_name(name: String): Boolean = name == "Pure"
 
-  val pure_roots: List[Path] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML").map(Path.explode(_))
+  val pure_roots: List[String] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML")
 
-  def pure_files(dir: Path): List[Path] =
-    (pure_roots ::: pure_roots.flatMap(root => ML_Root.read_files(dir + root))).map(dir + _)
+  def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
+  {
+    val loaded_files =
+      pure_roots.flatMap(root =>
+        resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
+    (pure_roots ::: loaded_files).map(file => dir + Path.explode(file))
+  }
 
 
   /* info */
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/Tools/build.scala	Thu Apr 07 16:53:43 2016 +0200
@@ -174,9 +174,12 @@
 
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
             val loaded_files =
-              if (inlined_files)
-                (if (Sessions.pure_name(name)) Sessions.pure_files(info.dir) else Nil) :::
-                  thy_deps.loaded_files
+              if (inlined_files) {
+                val pure_files =
+                  if (Sessions.pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
+                  else Nil
+                pure_files ::: thy_deps.loaded_files
+              }
               else Nil
 
             val all_files =
@@ -257,7 +260,7 @@
       Future.thread("build") {
         val process =
           if (Sessions.pure_name(name)) {
-            val roots = Sessions.pure_roots.flatMap(root => List("--use", File.platform_path(root)))
+            val roots = Sessions.pure_roots.flatMap(root => List("--use", root))
             val eval =
               "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
               " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -135,7 +135,7 @@
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
-    {SML_syntax = SML, SML_env = SML, exchange = false, redirect = false, verbose = verbose,
+    {SML = SML, exchange = false, redirect = false, verbose = verbose,
       debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;
 
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala	Thu Apr 07 16:53:43 2016 +0200
@@ -39,6 +39,7 @@
     val eval_init =
       if (heaps.isEmpty) {
         List(
+          "val ML_file = PolyML.use",
           if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") "structure FixedInt = IntInf"
           else "",
           if (Platform.is_windows)
diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/build-jars	Thu Apr 07 16:53:43 2016 +0200
@@ -54,7 +54,6 @@
   Isar/parse.scala
   Isar/token.scala
   ML/ml_lex.scala
-  ML/ml_root.scala
   ML/ml_syntax.scala
   PIDE/batch_session.scala
   PIDE/command.scala
diff -r 0951d6cec68c -r 3c0f53eae166 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -81,7 +81,7 @@
 fun exec ctxt verbose code =
  (if Config.get ctxt trace then tracing code else ();
   ML_Context.exec (fn () =>
-    ML_Compiler0.use_text ML_Env.context
+    ML_Compiler0.ML ML_Env.context
       {line = 0, file = "generated code", verbose = verbose, debug = false} code));
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
@@ -536,7 +536,7 @@
     val thy' = Loaded_Values.put [] thy;
     val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
     val _ =
-      ML_Compiler0.use_text notifying_context
+      ML_Compiler0.ML notifying_context
         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
         (File.read filepath);
     val thy'' = Context.the_global_context ();
diff -r 0951d6cec68c -r 3c0f53eae166 src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -136,7 +136,7 @@
     val _ =
       Context.setmp_generic_context (SOME (Context.Proof ctxt))
         (fn () =>
-          ML_Compiler0.use_text context
+          ML_Compiler0.ML context
             {line = 0, file = "generated code", verbose = true, debug = false} s) ()
   in
     Gen_Construction.parse_pred (! return)
@@ -146,7 +146,7 @@
 fun run_test ctxt s =
   Context.setmp_generic_context (SOME (Context.Proof ctxt))
     (fn () =>
-      ML_Compiler0.use_text ML_Env.context
+      ML_Compiler0.ML ML_Env.context
         {line = 0, file = "generated code", verbose = false, debug = false} s) ();
 
 (*split input into tokens*)