more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
authorwenzelm
Thu Apr 07 16:53:43 2016 +0200 (2016-04-07)
changeset 629023c0f53eae166
parent 62901 0951d6cec68c
child 62903 adcce7b8d8ba
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;
src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler0.ML
src/Pure/ML/ml_compiler1.ML
src/Pure/ML/ml_compiler2.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_file.ML
src/Pure/ML/ml_name_space.ML
src/Pure/ML/ml_pervasive1.ML
src/Pure/ML/ml_root.scala
src/Pure/ML_Bootstrap.thy
src/Pure/Pure.thy
src/Pure/ROOT.ML
src/Pure/ROOT0.ML
src/Pure/ROOT1.ML
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/debugger.ML
src/Pure/Tools/ml_process.scala
src/Pure/build-jars
src/Tools/Code/code_runtime.ML
src/Tools/Spec_Check/spec_check.ML
     1.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Thu Apr 07 15:32:47 2016 +0200
     1.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Thu Apr 07 16:53:43 2016 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4  
     1.5      in
     1.6          compiled_rewriter := NONE;      
     1.7 -        ML_Compiler0.use_text ML_Env.context
     1.8 +        ML_Compiler0.ML ML_Env.context
     1.9            {line = 1, file = "", verbose = false, debug = false} (!buffer);
    1.10          case !compiled_rewriter of 
    1.11              NONE => raise (Compile "cannot communicate with compiled function")
     2.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Thu Apr 07 15:32:47 2016 +0200
     2.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Thu Apr 07 16:53:43 2016 +0200
     2.3 @@ -486,7 +486,7 @@
     2.4  fun writeTextFile name s = File.write (Path.explode name) s
     2.5  
     2.6  fun use_source src =
     2.7 -  ML_Compiler0.use_text ML_Env.context
     2.8 +  ML_Compiler0.ML ML_Env.context
     2.9      {line = 1, file = "", verbose = false, debug = false} src
    2.10      
    2.11  fun compile rules = 
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Apr 07 15:32:47 2016 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Apr 07 16:53:43 2016 +0200
     3.3 @@ -206,7 +206,7 @@
     3.4  
     3.5  fun exec verbose code =
     3.6    ML_Context.exec (fn () =>
     3.7 -    ML_Compiler0.use_text ML_Env.context
     3.8 +    ML_Compiler0.ML ML_Env.context
     3.9        {line = 0, file = "generated code", verbose = verbose, debug = false} code)
    3.10  
    3.11  fun with_overlord_dir name f =
     4.1 --- a/src/Pure/ML/ml_compiler.ML	Thu Apr 07 15:32:47 2016 +0200
     4.2 +++ b/src/Pure/ML/ml_compiler.ML	Thu Apr 07 16:53:43 2016 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  signature ML_COMPILER =
     4.5  sig
     4.6    type flags =
     4.7 -    {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
     4.8 +    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
     4.9        debug: bool option, writeln: string -> unit, warning: string -> unit}
    4.10    val debug_flags: bool option -> flags
    4.11    val flags: flags
    4.12 @@ -21,19 +21,18 @@
    4.13  (* flags *)
    4.14  
    4.15  type flags =
    4.16 -  {SML_syntax: bool, SML_env: bool, exchange: bool, redirect: bool, verbose: bool,
    4.17 +  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    4.18      debug: bool option, writeln: string -> unit, warning: string -> unit};
    4.19  
    4.20  fun debug_flags opt_debug : flags =
    4.21 -  {SML_syntax = false, SML_env = false, exchange = false, redirect = false, verbose = false,
    4.22 +  {SML = false, exchange = false, redirect = false, verbose = false,
    4.23      debug = opt_debug, writeln = writeln, warning = warning};
    4.24  
    4.25  val flags = debug_flags NONE;
    4.26  
    4.27  fun verbose b (flags: flags) =
    4.28 -  {SML_syntax = #SML_syntax flags, SML_env = #SML_env flags, exchange = #exchange flags,
    4.29 -    redirect = #redirect flags, verbose = b, debug = #debug flags,
    4.30 -    writeln = #writeln flags, warning = #warning flags};
    4.31 +  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
    4.32 +    debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
    4.33  
    4.34  
    4.35  (* parse trees *)
    4.36 @@ -145,7 +144,7 @@
    4.37  
    4.38  fun eval (flags: flags) pos toks =
    4.39    let
    4.40 -    val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
    4.41 +    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
    4.42      val opt_context = Context.get_generic_context ();
    4.43  
    4.44  
    4.45 @@ -154,7 +153,7 @@
    4.46      val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
    4.47  
    4.48      val input_explode =
    4.49 -      if #SML_syntax flags then String.explode
    4.50 +      if #SML flags then String.explode
    4.51        else maps (String.explode o Symbol.esc) o Symbol.explode;
    4.52  
    4.53      val input_buffer =
     5.1 --- a/src/Pure/ML/ml_compiler0.ML	Thu Apr 07 15:32:47 2016 +0200
     5.2 +++ b/src/Pure/ML/ml_compiler0.ML	Thu Apr 07 16:53:43 2016 +0200
     5.3 @@ -2,7 +2,7 @@
     5.4      Author:     Makarius
     5.5  
     5.6  Runtime compilation and evaluation for bootstrap.
     5.7 -Initial ML use operations.
     5.8 +Initial ML file operations.
     5.9  *)
    5.10  
    5.11  signature ML_COMPILER0 =
    5.12 @@ -15,11 +15,11 @@
    5.13      print: string -> unit,
    5.14      error: string -> unit}
    5.15    val make_context: ML_Name_Space.T -> context
    5.16 -  val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
    5.17 -  val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
    5.18 +  val ML: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
    5.19 +  val ML_file: context -> {debug: bool, verbose: bool} -> string -> unit
    5.20    val debug_option: bool option -> bool
    5.21 -  val use_operations: (bool option -> string -> unit) ->
    5.22 -    {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit}
    5.23 +  val ML_file_operations: (bool option -> string -> unit) ->
    5.24 +    {ML_file: string -> unit, ML_file_debug: string -> unit, ML_file_no_debug: string -> unit}
    5.25  end;
    5.26  
    5.27  structure ML_Compiler0: ML_COMPILER0 =
    5.28 @@ -53,7 +53,7 @@
    5.29    error = fn s => error s};
    5.30  
    5.31  
    5.32 -(* use operations *)
    5.33 +(* ML file operations *)
    5.34  
    5.35  local
    5.36  
    5.37 @@ -77,8 +77,7 @@
    5.38  
    5.39  in
    5.40  
    5.41 -fun use_text ({name_space, print_depth, here, print, error, ...}: context)
    5.42 -    {line, file, verbose, debug} text =
    5.43 +fun ML {name_space, print_depth, here, print, error, ...} {line, file, verbose, debug} text =
    5.44    let
    5.45      val current_line = Unsynchronized.ref line;
    5.46      val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
    5.47 @@ -118,14 +117,14 @@
    5.48  
    5.49  end;
    5.50  
    5.51 -fun use_file context {verbose, debug} file =
    5.52 +fun ML_file context {verbose, debug} file =
    5.53    let
    5.54      val instream = TextIO.openIn file;
    5.55      val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    5.56 -  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    5.57 +  in ML context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    5.58  
    5.59 -fun use_operations (use_ : bool option -> string -> unit) =
    5.60 -  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
    5.61 +fun ML_file_operations (f: bool option -> string -> unit) =
    5.62 +  {ML_file = f NONE, ML_file_debug = f (SOME true), ML_file_no_debug = f (SOME false)};
    5.63  
    5.64  
    5.65  fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
    5.66 @@ -134,12 +133,12 @@
    5.67  end;
    5.68  
    5.69  
    5.70 -(* initial use operations *)
    5.71 +(* initial ML_file operations *)
    5.72  
    5.73 -val {use, use_debug, use_no_debug} =
    5.74 +val {ML_file, ML_file_debug, ML_file_no_debug} =
    5.75    let val context = ML_Compiler0.make_context ML_Name_Space.global in
    5.76 -    ML_Compiler0.use_operations (fn opt_debug => fn file =>
    5.77 -      ML_Compiler0.use_file context
    5.78 +    ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
    5.79 +      ML_Compiler0.ML_file context
    5.80          {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
    5.81        handle ERROR msg => (#print context msg; raise error "ML error"))
    5.82    end;
    5.83 @@ -149,7 +148,7 @@
    5.84  
    5.85  if Thread_Data.is_virtual then ()
    5.86  else
    5.87 -  ML_Compiler0.use_text
    5.88 +  ML_Compiler0.ML
    5.89      (ML_Compiler0.make_context
    5.90        (ML_Name_Space.global_values
    5.91          [("prettyRepresentation", "ML_system_pretty"),
     6.1 --- a/src/Pure/ML/ml_compiler1.ML	Thu Apr 07 15:32:47 2016 +0200
     6.2 +++ b/src/Pure/ML/ml_compiler1.ML	Thu Apr 07 16:53:43 2016 +0200
     6.3 @@ -1,10 +1,10 @@
     6.4  (*  Title:      Pure/ML/ml_compiler1.ML
     6.5      Author:     Makarius
     6.6  
     6.7 -Refined ML use operations for bootstrap.
     6.8 +Refined ML file operations for bootstrap.
     6.9  *)
    6.10  
    6.11 -val {use, use_debug, use_no_debug} =
    6.12 +val {ML_file, ML_file_debug, ML_file_no_debug} =
    6.13    let
    6.14      val context: ML_Compiler0.context =
    6.15       {name_space = ML_Name_Space.global,
    6.16 @@ -13,10 +13,10 @@
    6.17        print = writeln,
    6.18        error = error};
    6.19    in
    6.20 -    ML_Compiler0.use_operations (fn opt_debug => fn file =>
    6.21 +    ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
    6.22        Position.setmp_thread_data (Position.file_only file)
    6.23          (fn () =>
    6.24 -          ML_Compiler0.use_file context
    6.25 +          ML_Compiler0.ML_file context
    6.26              {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
    6.27            handle ERROR msg => (writeln msg; error "ML error")) ())
    6.28    end;
     7.1 --- a/src/Pure/ML/ml_compiler2.ML	Thu Apr 07 15:32:47 2016 +0200
     7.2 +++ b/src/Pure/ML/ml_compiler2.ML	Thu Apr 07 16:53:43 2016 +0200
     7.3 @@ -1,11 +1,11 @@
     7.4  (*  Title:      Pure/ML/ml_compiler2.ML
     7.5      Author:     Makarius
     7.6  
     7.7 -Isabelle/ML use operations.
     7.8 +Isabelle/ML file operations.
     7.9  *)
    7.10  
    7.11 -val {use, use_debug, use_no_debug} =
    7.12 -  ML_Compiler0.use_operations (fn opt_debug => fn file =>
    7.13 +val {ML_file, ML_file_debug, ML_file_no_debug} =
    7.14 +  ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
    7.15      let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
    7.16        ML_Context.eval_file flags (Path.explode file)
    7.17          handle ERROR msg => (writeln msg; error "ML error")
     8.1 --- a/src/Pure/ML/ml_context.ML	Thu Apr 07 15:32:47 2016 +0200
     8.2 +++ b/src/Pure/ML/ml_context.ML	Thu Apr 07 16:53:43 2016 +0200
     8.3 @@ -210,7 +210,7 @@
     8.4    in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
     8.5  
     8.6  fun eval_source flags source =
     8.7 -  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
     8.8 +  eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
     8.9  
    8.10  fun eval_in ctxt flags pos ants =
    8.11    Context.setmp_generic_context (Option.map Context.Proof ctxt)
     9.1 --- a/src/Pure/ML/ml_env.ML	Thu Apr 07 15:32:47 2016 +0200
     9.2 +++ b/src/Pure/ML/ml_env.ML	Thu Apr 07 16:53:43 2016 +0200
     9.3 @@ -13,6 +13,7 @@
     9.4      Context.generic -> Context.generic
     9.5    val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
     9.6    val init_bootstrap: Context.generic -> Context.generic
     9.7 +  val SML_environment: bool Config.T
     9.8    val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
     9.9    val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    9.10    val context: ML_Compiler0.context
    9.11 @@ -91,6 +92,18 @@
    9.12  val get_breakpoint = Inttab.lookup o #breakpoints o Env.get;
    9.13  
    9.14  
    9.15 +(* SML environment for Isabelle/ML *)
    9.16 +
    9.17 +val SML_environment =
    9.18 +  Config.bool (Config.declare ("SML_environment", @{here}) (fn _ => Config.Bool false));
    9.19 +
    9.20 +fun sml_env SML =
    9.21 +  SML orelse
    9.22 +    (case Context.get_generic_context () of
    9.23 +      NONE => false
    9.24 +    | SOME context => Config.get_generic context SML_environment);
    9.25 +
    9.26 +
    9.27  (* name space *)
    9.28  
    9.29  val init_bootstrap =
    9.30 @@ -114,7 +127,7 @@
    9.31    Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    9.32      let
    9.33        val (tables', sml_tables') =
    9.34 -        (tables, sml_tables) |> (if SML then apsnd else apfst)
    9.35 +        (tables, sml_tables) |> (if sml_env SML then apsnd else apfst)
    9.36            (fn (val1, type1, fixity1, structure1, signature1, functor1) =>
    9.37              let
    9.38                val val2 = fold Symtab.update (#allVal space ()) val1;
    9.39 @@ -129,7 +142,7 @@
    9.40  fun make_name_space {SML, exchange} : ML_Name_Space.T =
    9.41    let
    9.42      fun lookup sel1 sel2 name =
    9.43 -      if SML then
    9.44 +      if sml_env SML then
    9.45          Context.the_generic_context ()
    9.46          |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
    9.47        else
    9.48 @@ -138,7 +151,7 @@
    9.49          |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
    9.50  
    9.51      fun all sel1 sel2 () =
    9.52 -      (if SML then
    9.53 +      (if sml_env SML then
    9.54          Context.the_generic_context ()
    9.55          |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
    9.56        else
    9.57 @@ -148,7 +161,7 @@
    9.58        |> sort_distinct (string_ord o apply2 #1);
    9.59  
    9.60      fun enter ap1 sel2 entry =
    9.61 -      if SML <> exchange then
    9.62 +      if sml_env SML <> exchange then
    9.63          Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    9.64            let val sml_tables' = ap1 (Symtab.update entry) sml_tables
    9.65            in make_data (bootstrap, tables, sml_tables', breakpoints) end))
    10.1 --- a/src/Pure/ML/ml_file.ML	Thu Apr 07 15:32:47 2016 +0200
    10.2 +++ b/src/Pure/ML/ml_file.ML	Thu Apr 07 16:53:43 2016 +0200
    10.3 @@ -8,7 +8,6 @@
    10.4  sig
    10.5    val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    10.6    val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    10.7 -  val use: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    10.8  end;
    10.9  
   10.10  structure ML_File: ML_FILE =
   10.11 @@ -19,10 +18,9 @@
   10.12      val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
   10.13      val provide = Resources.provide (src_path, digest);
   10.14      val source = Input.source true (cat_lines lines) (pos, pos);
   10.15 -    val (SML_syntax, SML_env) = SML src_path;
   10.16      val flags =
   10.17 -      {SML_syntax = SML_syntax, SML_env = SML_env, exchange = false, redirect = true,
   10.18 -        verbose = true, debug = debug, writeln = writeln, warning = warning};
   10.19 +      {SML = SML, exchange = false, redirect = true, verbose = true,
   10.20 +        debug = debug, writeln = writeln, warning = warning};
   10.21    in
   10.22      gthy
   10.23      |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
   10.24 @@ -30,17 +28,7 @@
   10.25      |> Context.mapping provide (Local_Theory.background_theory provide)
   10.26    end);
   10.27  
   10.28 -val ML = command (K (false, false));
   10.29 -val SML = command (K (true, true));
   10.30 -
   10.31 -val use =
   10.32 -  command (fn path =>
   10.33 -    (case try (#2 o Path.split_ext) path of
   10.34 -      SOME "ML" => (false, true)
   10.35 -    | SOME "sml" => (true, true)
   10.36 -    | SOME "sig" => (true, true)
   10.37 -    | _ =>
   10.38 -        error ("Bad file name " ^ Path.print path ^
   10.39 -          "\nExpected .ML for Isabelle/ML or .sml/.sig for Standard ML")));
   10.40 +val ML = command false;
   10.41 +val SML = command true;
   10.42  
   10.43  end;
    11.1 --- a/src/Pure/ML/ml_name_space.ML	Thu Apr 07 15:32:47 2016 +0200
    11.2 +++ b/src/Pure/ML/ml_name_space.ML	Thu Apr 07 16:53:43 2016 +0200
    11.3 @@ -61,7 +61,7 @@
    11.4    (* bootstrap environment *)
    11.5  
    11.6    val bootstrap_values =
    11.7 -    ["use", "exit", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
    11.8 +    ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
    11.9    val bootstrap_structures =
   11.10      ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data"];
   11.11  
    12.1 --- a/src/Pure/ML/ml_pervasive1.ML	Thu Apr 07 15:32:47 2016 +0200
    12.2 +++ b/src/Pure/ML/ml_pervasive1.ML	Thu Apr 07 16:53:43 2016 +0200
    12.3 @@ -12,3 +12,5 @@
    12.4  Proofterm.proofs := 0;
    12.5  
    12.6  Context.put_generic_context NONE;
    12.7 +
    12.8 +val use = ML_file;
    13.1 --- a/src/Pure/ML/ml_root.scala	Thu Apr 07 15:32:47 2016 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,48 +0,0 @@
    13.4 -/*  Title:      Pure/ML/ml_root.scala
    13.5 -    Author:     Makarius
    13.6 -
    13.7 -Support for ML project ROOT file, with imitation of ML "use" commands.
    13.8 -*/
    13.9 -
   13.10 -package isabelle
   13.11 -
   13.12 -
   13.13 -object ML_Root
   13.14 -{
   13.15 -  /* parser */
   13.16 -
   13.17 -  val USE = "use"
   13.18 -  val USE_DEBUG = "use_debug"
   13.19 -  val USE_NO_DEBUG = "use_no_debug"
   13.20 -  val USE_THY = "use_thy"
   13.21 -
   13.22 -  lazy val syntax =
   13.23 -    Outer_Syntax.init() + ";" +
   13.24 -      (USE, Some((Keyword.THY_LOAD, Nil)), None) +
   13.25 -      (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
   13.26 -      (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
   13.27 -      (USE_THY, Some((Keyword.THY_LOAD, List("thy"))), None)
   13.28 -
   13.29 -  private object Parser extends Parse.Parser
   13.30 -  {
   13.31 -    val entry: Parser[Path] =
   13.32 -      command(USE_THY) ~! string ^^
   13.33 -        { case _ ~ a => Resources.thy_path(Path.explode(a)) } |
   13.34 -      (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG)) ~! string ^^
   13.35 -        { case _ ~ a => Path.explode(a) }
   13.36 -
   13.37 -    val entries: Parser[List[Path]] =
   13.38 -      rep(entry <~ $$$(";"))
   13.39 -  }
   13.40 -
   13.41 -  def read_files(root: Path): List[Path] =
   13.42 -  {
   13.43 -    val toks = Token.explode(syntax.keywords, File.read(root))
   13.44 -    val start = Token.Pos.file(root.implode)
   13.45 -
   13.46 -    Parser.parse_all(Parser.entries, Token.reader(toks, start)) match {
   13.47 -      case Parser.Success(entries, _) => entries
   13.48 -      case bad => error(bad.toString)
   13.49 -    }
   13.50 -  }
   13.51 -}
    14.1 --- a/src/Pure/ML_Bootstrap.thy	Thu Apr 07 15:32:47 2016 +0200
    14.2 +++ b/src/Pure/ML_Bootstrap.thy	Thu Apr 07 16:53:43 2016 +0200
    14.3 @@ -6,31 +6,10 @@
    14.4  
    14.5  theory ML_Bootstrap
    14.6  imports Pure
    14.7 -keywords "use" "use_debug" "use_no_debug" :: thy_load
    14.8  begin
    14.9  
   14.10  setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
   14.11  SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close>
   14.12 -
   14.13 -ML \<open>
   14.14 -local
   14.15 -
   14.16 -val _ =
   14.17 -  Outer_Syntax.command @{command_keyword use}
   14.18 -    "read and evaluate Isabelle/ML or SML file"
   14.19 -    (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
   14.20 -
   14.21 -val _ =
   14.22 -  Outer_Syntax.command @{command_keyword use_debug}
   14.23 -    "read and evaluate Isabelle/ML or SML file (with debugger information)"
   14.24 -    (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
   14.25 -
   14.26 -val _ =
   14.27 -  Outer_Syntax.command @{command_keyword use_no_debug}
   14.28 -    "read and evaluate Isabelle/ML or SML file (no debugger information)"
   14.29 -    (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
   14.30 -
   14.31 -in end
   14.32 -\<close>
   14.33 +setup \<open>Config.put_global ML_Env.SML_environment true\<close>
   14.34  
   14.35  end
    15.1 --- a/src/Pure/Pure.thy	Thu Apr 07 15:32:47 2016 +0200
    15.2 +++ b/src/Pure/Pure.thy	Thu Apr 07 16:53:43 2016 +0200
    15.3 @@ -100,41 +100,43 @@
    15.4  ML \<open>
    15.5  local
    15.6  
    15.7 +val semi = Scan.option @{keyword ";"};
    15.8 +
    15.9  val _ =
   15.10    Outer_Syntax.command @{command_keyword ML_file} "read and evaluate Isabelle/ML file"
   15.11 -    (Resources.parse_files "ML_file" >> ML_File.ML NONE);
   15.12 +    (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE);
   15.13  
   15.14  val _ =
   15.15    Outer_Syntax.command @{command_keyword ML_file_debug}
   15.16      "read and evaluate Isabelle/ML file (with debugger information)"
   15.17 -    (Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true));
   15.18 +    (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true));
   15.19  
   15.20  val _ =
   15.21    Outer_Syntax.command @{command_keyword ML_file_no_debug}
   15.22      "read and evaluate Isabelle/ML file (no debugger information)"
   15.23 -    (Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false));
   15.24 +    (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false));
   15.25  
   15.26  val _ =
   15.27    Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
   15.28 -    (Resources.parse_files "SML_file" >> ML_File.SML NONE);
   15.29 +    (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE);
   15.30  
   15.31  val _ =
   15.32    Outer_Syntax.command @{command_keyword SML_file_debug}
   15.33      "read and evaluate Standard ML file (with debugger information)"
   15.34 -    (Resources.parse_files "SML_file_debug" >> ML_File.SML (SOME true));
   15.35 +    (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true));
   15.36  
   15.37  val _ =
   15.38    Outer_Syntax.command @{command_keyword SML_file_no_debug}
   15.39      "read and evaluate Standard ML file (no debugger information)"
   15.40 -    (Resources.parse_files "SML_file_no_debug" >> ML_File.SML (SOME false));
   15.41 +    (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false));
   15.42  
   15.43  val _ =
   15.44    Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
   15.45      (Parse.ML_source >> (fn source =>
   15.46        let
   15.47          val flags: ML_Compiler.flags =
   15.48 -          {SML_syntax = true, SML_env = true, exchange = true, redirect = false,
   15.49 -            verbose = true, debug = NONE, writeln = writeln, warning = warning};
   15.50 +          {SML = true, exchange = true, redirect = false, verbose = true,
   15.51 +            debug = NONE, writeln = writeln, warning = warning};
   15.52        in
   15.53          Toplevel.theory
   15.54            (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
   15.55 @@ -145,8 +147,8 @@
   15.56      (Parse.ML_source >> (fn source =>
   15.57        let
   15.58          val flags: ML_Compiler.flags =
   15.59 -          {SML_syntax = false, SML_env = false, exchange = true, redirect = false,
   15.60 -            verbose = true, debug = NONE, writeln = writeln, warning = warning};
   15.61 +          {SML = false, exchange = true, redirect = false, verbose = true,
   15.62 +            debug = NONE, writeln = writeln, warning = warning};
   15.63        in
   15.64          Toplevel.generic_theory
   15.65            (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
    16.1 --- a/src/Pure/ROOT.ML	Thu Apr 07 15:32:47 2016 +0200
    16.2 +++ b/src/Pure/ROOT.ML	Thu Apr 07 16:53:43 2016 +0200
    16.3 @@ -1,25 +1,25 @@
    16.4  (*** Isabelle/Pure bootstrap ***)
    16.5  
    16.6 -use "ML/ml_name_space.ML";
    16.7 +ML_file "ML/ml_name_space.ML";
    16.8  
    16.9  
   16.10  (** bootstrap phase 0: Poly/ML setup **)
   16.11  
   16.12 -use "ML/ml_pervasive0.ML";
   16.13 -use "ML/ml_system.ML";
   16.14 -use "System/distribution.ML";
   16.15 +ML_file "ML/ml_pervasive0.ML";
   16.16 +ML_file "ML/ml_system.ML";
   16.17 +ML_file "System/distribution.ML";
   16.18  
   16.19 -use "General/exn.ML";
   16.20 +ML_file "General/exn.ML";
   16.21  
   16.22 -use "Concurrent/multithreading.ML";
   16.23 -use "Concurrent/unsynchronized.ML";
   16.24 +ML_file "Concurrent/multithreading.ML";
   16.25 +ML_file "Concurrent/unsynchronized.ML";
   16.26  
   16.27 -use "ML/ml_heap.ML";
   16.28 -use "ML/ml_profiling.ML";
   16.29 -use "ML/ml_print_depth0.ML";
   16.30 -use "ML/ml_pretty.ML";
   16.31 -use "ML/ml_compiler0.ML";
   16.32 -use_no_debug "ML/ml_debugger.ML";
   16.33 +ML_file "ML/ml_heap.ML";
   16.34 +ML_file "ML/ml_profiling.ML";
   16.35 +ML_file "ML/ml_print_depth0.ML";
   16.36 +ML_file "ML/ml_pretty.ML";
   16.37 +ML_file "ML/ml_compiler0.ML";
   16.38 +ML_file_no_debug "ML/ml_debugger.ML";
   16.39  
   16.40  
   16.41  
   16.42 @@ -27,307 +27,307 @@
   16.43  
   16.44  (* library of general tools *)
   16.45  
   16.46 -use "General/basics.ML";
   16.47 -use "library.ML";
   16.48 -use "General/print_mode.ML";
   16.49 -use "General/alist.ML";
   16.50 -use "General/table.ML";
   16.51 +ML_file "General/basics.ML";
   16.52 +ML_file "library.ML";
   16.53 +ML_file "General/print_mode.ML";
   16.54 +ML_file "General/alist.ML";
   16.55 +ML_file "General/table.ML";
   16.56  
   16.57 -use "Concurrent/synchronized.ML";
   16.58 -use "Concurrent/counter.ML";
   16.59 +ML_file "Concurrent/synchronized.ML";
   16.60 +ML_file "Concurrent/counter.ML";
   16.61  
   16.62 -use "General/random.ML";
   16.63 -use "General/properties.ML";
   16.64 -use "General/output.ML";
   16.65 -use "PIDE/markup.ML";
   16.66 -use "General/scan.ML";
   16.67 -use "General/source.ML";
   16.68 -use "General/symbol.ML";
   16.69 -use "General/position.ML";
   16.70 -use "General/symbol_pos.ML";
   16.71 -use "General/input.ML";
   16.72 -use "General/antiquote.ML";
   16.73 -use "ML/ml_lex.ML";
   16.74 -use "ML/ml_compiler1.ML";
   16.75 +ML_file "General/random.ML";
   16.76 +ML_file "General/properties.ML";
   16.77 +ML_file "General/output.ML";
   16.78 +ML_file "PIDE/markup.ML";
   16.79 +ML_file "General/scan.ML";
   16.80 +ML_file "General/source.ML";
   16.81 +ML_file "General/symbol.ML";
   16.82 +ML_file "General/position.ML";
   16.83 +ML_file "General/symbol_pos.ML";
   16.84 +ML_file "General/input.ML";
   16.85 +ML_file "General/antiquote.ML";
   16.86 +ML_file "ML/ml_lex.ML";
   16.87 +ML_file "ML/ml_compiler1.ML";
   16.88  
   16.89  
   16.90  (** bootstrap phase 2: towards ML within Isar context *)
   16.91  
   16.92  (* library of general tools *)
   16.93  
   16.94 -use "General/integer.ML";
   16.95 -use "General/stack.ML";
   16.96 -use "General/queue.ML";
   16.97 -use "General/heap.ML";
   16.98 -use "General/same.ML";
   16.99 -use "General/ord_list.ML";
  16.100 -use "General/balanced_tree.ML";
  16.101 -use "General/linear_set.ML";
  16.102 -use "General/buffer.ML";
  16.103 -use "General/pretty.ML";
  16.104 -use "PIDE/xml.ML";
  16.105 -use "General/path.ML";
  16.106 -use "General/url.ML";
  16.107 -use "General/file.ML";
  16.108 -use "General/long_name.ML";
  16.109 -use "General/binding.ML";
  16.110 -use "General/socket_io.ML";
  16.111 -use "General/seq.ML";
  16.112 -use "General/timing.ML";
  16.113 -use "General/sha1.ML";
  16.114 +ML_file "General/integer.ML";
  16.115 +ML_file "General/stack.ML";
  16.116 +ML_file "General/queue.ML";
  16.117 +ML_file "General/heap.ML";
  16.118 +ML_file "General/same.ML";
  16.119 +ML_file "General/ord_list.ML";
  16.120 +ML_file "General/balanced_tree.ML";
  16.121 +ML_file "General/linear_set.ML";
  16.122 +ML_file "General/buffer.ML";
  16.123 +ML_file "General/pretty.ML";
  16.124 +ML_file "PIDE/xml.ML";
  16.125 +ML_file "General/path.ML";
  16.126 +ML_file "General/url.ML";
  16.127 +ML_file "General/file.ML";
  16.128 +ML_file "General/long_name.ML";
  16.129 +ML_file "General/binding.ML";
  16.130 +ML_file "General/socket_io.ML";
  16.131 +ML_file "General/seq.ML";
  16.132 +ML_file "General/timing.ML";
  16.133 +ML_file "General/sha1.ML";
  16.134  
  16.135 -use "PIDE/yxml.ML";
  16.136 -use "PIDE/document_id.ML";
  16.137 +ML_file "PIDE/yxml.ML";
  16.138 +ML_file "PIDE/document_id.ML";
  16.139  
  16.140 -use "General/change_table.ML";
  16.141 -use "General/graph.ML";
  16.142 +ML_file "General/change_table.ML";
  16.143 +ML_file "General/graph.ML";
  16.144  
  16.145  
  16.146  (* fundamental structures *)
  16.147  
  16.148 -use "name.ML";
  16.149 -use "term.ML";
  16.150 -use "context.ML";
  16.151 -use "context_position.ML";
  16.152 -use "System/options.ML";
  16.153 -use "config.ML";
  16.154 +ML_file "name.ML";
  16.155 +ML_file "term.ML";
  16.156 +ML_file "context.ML";
  16.157 +ML_file "context_position.ML";
  16.158 +ML_file "System/options.ML";
  16.159 +ML_file "config.ML";
  16.160  
  16.161  
  16.162  (* concurrency within the ML runtime *)
  16.163  
  16.164 -use "ML/exn_properties.ML";
  16.165 +ML_file "ML/exn_properties.ML";
  16.166  
  16.167 -use "ML/ml_statistics.ML";
  16.168 +ML_file "ML/ml_statistics.ML";
  16.169  
  16.170 -use "Concurrent/thread_data_virtual.ML";
  16.171 -use "Concurrent/standard_thread.ML";
  16.172 -use "Concurrent/single_assignment.ML";
  16.173 +ML_file "Concurrent/thread_data_virtual.ML";
  16.174 +ML_file "Concurrent/standard_thread.ML";
  16.175 +ML_file "Concurrent/single_assignment.ML";
  16.176  
  16.177 -use "Concurrent/par_exn.ML";
  16.178 -use "Concurrent/task_queue.ML";
  16.179 -use "Concurrent/future.ML";
  16.180 -use "Concurrent/event_timer.ML";
  16.181 -use "Concurrent/timeout.ML";
  16.182 -use "Concurrent/lazy.ML";
  16.183 -use "Concurrent/par_list.ML";
  16.184 +ML_file "Concurrent/par_exn.ML";
  16.185 +ML_file "Concurrent/task_queue.ML";
  16.186 +ML_file "Concurrent/future.ML";
  16.187 +ML_file "Concurrent/event_timer.ML";
  16.188 +ML_file "Concurrent/timeout.ML";
  16.189 +ML_file "Concurrent/lazy.ML";
  16.190 +ML_file "Concurrent/par_list.ML";
  16.191  
  16.192 -use "Concurrent/mailbox.ML";
  16.193 -use "Concurrent/cache.ML";
  16.194 +ML_file "Concurrent/mailbox.ML";
  16.195 +ML_file "Concurrent/cache.ML";
  16.196  
  16.197 -use "PIDE/active.ML";
  16.198 +ML_file "PIDE/active.ML";
  16.199  
  16.200  
  16.201  (* inner syntax *)
  16.202  
  16.203 -use "Syntax/type_annotation.ML";
  16.204 -use "Syntax/term_position.ML";
  16.205 -use "Syntax/lexicon.ML";
  16.206 -use "Syntax/ast.ML";
  16.207 -use "Syntax/syntax_ext.ML";
  16.208 -use "Syntax/parser.ML";
  16.209 -use "Syntax/syntax_trans.ML";
  16.210 -use "Syntax/mixfix.ML";
  16.211 -use "Syntax/printer.ML";
  16.212 -use "Syntax/syntax.ML";
  16.213 +ML_file "Syntax/type_annotation.ML";
  16.214 +ML_file "Syntax/term_position.ML";
  16.215 +ML_file "Syntax/lexicon.ML";
  16.216 +ML_file "Syntax/ast.ML";
  16.217 +ML_file "Syntax/syntax_ext.ML";
  16.218 +ML_file "Syntax/parser.ML";
  16.219 +ML_file "Syntax/syntax_trans.ML";
  16.220 +ML_file "Syntax/mixfix.ML";
  16.221 +ML_file "Syntax/printer.ML";
  16.222 +ML_file "Syntax/syntax.ML";
  16.223  
  16.224  
  16.225  (* core of tactical proof system *)
  16.226  
  16.227 -use "term_ord.ML";
  16.228 -use "term_subst.ML";
  16.229 -use "term_xml.ML";
  16.230 -use "General/completion.ML";
  16.231 -use "General/name_space.ML";
  16.232 -use "sorts.ML";
  16.233 -use "type.ML";
  16.234 -use "logic.ML";
  16.235 -use "Syntax/simple_syntax.ML";
  16.236 -use "net.ML";
  16.237 -use "item_net.ML";
  16.238 -use "envir.ML";
  16.239 -use "consts.ML";
  16.240 -use "primitive_defs.ML";
  16.241 -use "sign.ML";
  16.242 -use "defs.ML";
  16.243 -use "term_sharing.ML";
  16.244 -use "pattern.ML";
  16.245 -use "unify.ML";
  16.246 -use "theory.ML";
  16.247 -use "proofterm.ML";
  16.248 -use "thm.ML";
  16.249 -use "more_pattern.ML";
  16.250 -use "more_unify.ML";
  16.251 -use "more_thm.ML";
  16.252 -use "facts.ML";
  16.253 -use "global_theory.ML";
  16.254 -use "pure_thy.ML";
  16.255 -use "drule.ML";
  16.256 -use "morphism.ML";
  16.257 -use "variable.ML";
  16.258 -use "conv.ML";
  16.259 -use "goal_display.ML";
  16.260 -use "tactical.ML";
  16.261 -use "search.ML";
  16.262 -use "tactic.ML";
  16.263 -use "raw_simplifier.ML";
  16.264 -use "conjunction.ML";
  16.265 -use "assumption.ML";
  16.266 +ML_file "term_ord.ML";
  16.267 +ML_file "term_subst.ML";
  16.268 +ML_file "term_xml.ML";
  16.269 +ML_file "General/completion.ML";
  16.270 +ML_file "General/name_space.ML";
  16.271 +ML_file "sorts.ML";
  16.272 +ML_file "type.ML";
  16.273 +ML_file "logic.ML";
  16.274 +ML_file "Syntax/simple_syntax.ML";
  16.275 +ML_file "net.ML";
  16.276 +ML_file "item_net.ML";
  16.277 +ML_file "envir.ML";
  16.278 +ML_file "consts.ML";
  16.279 +ML_file "primitive_defs.ML";
  16.280 +ML_file "sign.ML";
  16.281 +ML_file "defs.ML";
  16.282 +ML_file "term_sharing.ML";
  16.283 +ML_file "pattern.ML";
  16.284 +ML_file "unify.ML";
  16.285 +ML_file "theory.ML";
  16.286 +ML_file "proofterm.ML";
  16.287 +ML_file "thm.ML";
  16.288 +ML_file "more_pattern.ML";
  16.289 +ML_file "more_unify.ML";
  16.290 +ML_file "more_thm.ML";
  16.291 +ML_file "facts.ML";
  16.292 +ML_file "global_theory.ML";
  16.293 +ML_file "pure_thy.ML";
  16.294 +ML_file "drule.ML";
  16.295 +ML_file "morphism.ML";
  16.296 +ML_file "variable.ML";
  16.297 +ML_file "conv.ML";
  16.298 +ML_file "goal_display.ML";
  16.299 +ML_file "tactical.ML";
  16.300 +ML_file "search.ML";
  16.301 +ML_file "tactic.ML";
  16.302 +ML_file "raw_simplifier.ML";
  16.303 +ML_file "conjunction.ML";
  16.304 +ML_file "assumption.ML";
  16.305  
  16.306  
  16.307  (* Isar -- Intelligible Semi-Automated Reasoning *)
  16.308  
  16.309  (*ML support and global execution*)
  16.310 -use "ML/ml_syntax.ML";
  16.311 -use "ML/ml_env.ML";
  16.312 -use "ML/ml_options.ML";
  16.313 -use "ML/ml_print_depth.ML";
  16.314 -use_no_debug "ML/exn_debugger.ML";
  16.315 -use_no_debug "Isar/runtime.ML";
  16.316 -use "PIDE/execution.ML";
  16.317 -use "ML/ml_compiler.ML";
  16.318 +ML_file "ML/ml_syntax.ML";
  16.319 +ML_file "ML/ml_env.ML";
  16.320 +ML_file "ML/ml_options.ML";
  16.321 +ML_file "ML/ml_print_depth.ML";
  16.322 +ML_file_no_debug "ML/exn_debugger.ML";
  16.323 +ML_file_no_debug "Isar/runtime.ML";
  16.324 +ML_file "PIDE/execution.ML";
  16.325 +ML_file "ML/ml_compiler.ML";
  16.326  
  16.327 -use "skip_proof.ML";
  16.328 -use "goal.ML";
  16.329 +ML_file "skip_proof.ML";
  16.330 +ML_file "goal.ML";
  16.331  
  16.332  (*proof context*)
  16.333 -use "Isar/object_logic.ML";
  16.334 -use "Isar/rule_cases.ML";
  16.335 -use "Isar/auto_bind.ML";
  16.336 -use "type_infer.ML";
  16.337 -use "Syntax/local_syntax.ML";
  16.338 -use "Isar/proof_context.ML";
  16.339 -use "type_infer_context.ML";
  16.340 -use "Syntax/syntax_phases.ML";
  16.341 -use "Isar/local_defs.ML";
  16.342 +ML_file "Isar/object_logic.ML";
  16.343 +ML_file "Isar/rule_cases.ML";
  16.344 +ML_file "Isar/auto_bind.ML";
  16.345 +ML_file "type_infer.ML";
  16.346 +ML_file "Syntax/local_syntax.ML";
  16.347 +ML_file "Isar/proof_context.ML";
  16.348 +ML_file "type_infer_context.ML";
  16.349 +ML_file "Syntax/syntax_phases.ML";
  16.350 +ML_file "Isar/local_defs.ML";
  16.351  
  16.352  (*outer syntax*)
  16.353 -use "Isar/keyword.ML";
  16.354 -use "Isar/token.ML";
  16.355 -use "Isar/parse.ML";
  16.356 -use "Isar/args.ML";
  16.357 +ML_file "Isar/keyword.ML";
  16.358 +ML_file "Isar/token.ML";
  16.359 +ML_file "Isar/parse.ML";
  16.360 +ML_file "Isar/args.ML";
  16.361  
  16.362  (*theory specifications*)
  16.363 -use "Isar/local_theory.ML";
  16.364 -use "Thy/thy_header.ML";
  16.365 -use "PIDE/command_span.ML";
  16.366 -use "Thy/thy_syntax.ML";
  16.367 -use "Thy/markdown.ML";
  16.368 -use "Thy/html.ML";
  16.369 -use "Thy/latex.ML";
  16.370 +ML_file "Isar/local_theory.ML";
  16.371 +ML_file "Thy/thy_header.ML";
  16.372 +ML_file "PIDE/command_span.ML";
  16.373 +ML_file "Thy/thy_syntax.ML";
  16.374 +ML_file "Thy/markdown.ML";
  16.375 +ML_file "Thy/html.ML";
  16.376 +ML_file "Thy/latex.ML";
  16.377  
  16.378  (*ML with context and antiquotations*)
  16.379 -use "ML/ml_context.ML";
  16.380 -use "ML/ml_antiquotation.ML";
  16.381 -use "ML/ml_compiler2.ML";
  16.382 +ML_file "ML/ml_context.ML";
  16.383 +ML_file "ML/ml_antiquotation.ML";
  16.384 +ML_file "ML/ml_compiler2.ML";
  16.385  
  16.386  
  16.387  
  16.388  (** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *)
  16.389  
  16.390  (*basic proof engine*)
  16.391 -use "par_tactical.ML";
  16.392 -use "Isar/proof_display.ML";
  16.393 -use "Isar/attrib.ML";
  16.394 -use "Isar/context_rules.ML";
  16.395 -use "Isar/method.ML";
  16.396 -use "Isar/proof.ML";
  16.397 -use "Isar/element.ML";
  16.398 -use "Isar/obtain.ML";
  16.399 -use "Isar/subgoal.ML";
  16.400 -use "Isar/calculation.ML";
  16.401 +ML_file "par_tactical.ML";
  16.402 +ML_file "Isar/proof_display.ML";
  16.403 +ML_file "Isar/attrib.ML";
  16.404 +ML_file "Isar/context_rules.ML";
  16.405 +ML_file "Isar/method.ML";
  16.406 +ML_file "Isar/proof.ML";
  16.407 +ML_file "Isar/element.ML";
  16.408 +ML_file "Isar/obtain.ML";
  16.409 +ML_file "Isar/subgoal.ML";
  16.410 +ML_file "Isar/calculation.ML";
  16.411  
  16.412  (*local theories and targets*)
  16.413 -use "Isar/locale.ML";
  16.414 -use "Isar/generic_target.ML";
  16.415 -use "Isar/overloading.ML";
  16.416 -use "axclass.ML";
  16.417 -use "Isar/class.ML";
  16.418 -use "Isar/named_target.ML";
  16.419 -use "Isar/expression.ML";
  16.420 -use "Isar/interpretation.ML";
  16.421 -use "Isar/class_declaration.ML";
  16.422 -use "Isar/bundle.ML";
  16.423 -use "Isar/experiment.ML";
  16.424 +ML_file "Isar/locale.ML";
  16.425 +ML_file "Isar/generic_target.ML";
  16.426 +ML_file "Isar/overloading.ML";
  16.427 +ML_file "axclass.ML";
  16.428 +ML_file "Isar/class.ML";
  16.429 +ML_file "Isar/named_target.ML";
  16.430 +ML_file "Isar/expression.ML";
  16.431 +ML_file "Isar/interpretation.ML";
  16.432 +ML_file "Isar/class_declaration.ML";
  16.433 +ML_file "Isar/bundle.ML";
  16.434 +ML_file "Isar/experiment.ML";
  16.435  
  16.436 -use "simplifier.ML";
  16.437 -use "Tools/plugin.ML";
  16.438 +ML_file "simplifier.ML";
  16.439 +ML_file "Tools/plugin.ML";
  16.440  
  16.441  (*executable theory content*)
  16.442 -use "Isar/code.ML";
  16.443 +ML_file "Isar/code.ML";
  16.444  
  16.445  (*specifications*)
  16.446 -use "Isar/parse_spec.ML";
  16.447 -use "Isar/spec_rules.ML";
  16.448 -use "Isar/specification.ML";
  16.449 -use "Isar/typedecl.ML";
  16.450 +ML_file "Isar/parse_spec.ML";
  16.451 +ML_file "Isar/spec_rules.ML";
  16.452 +ML_file "Isar/specification.ML";
  16.453 +ML_file "Isar/typedecl.ML";
  16.454  
  16.455  (*toplevel transactions*)
  16.456 -use "Isar/proof_node.ML";
  16.457 -use "Isar/toplevel.ML";
  16.458 +ML_file "Isar/proof_node.ML";
  16.459 +ML_file "Isar/toplevel.ML";
  16.460  
  16.461  (*proof term operations*)
  16.462 -use "Proof/reconstruct.ML";
  16.463 -use "Proof/proof_syntax.ML";
  16.464 -use "Proof/proof_rewrite_rules.ML";
  16.465 -use "Proof/proof_checker.ML";
  16.466 -use "Proof/extraction.ML";
  16.467 +ML_file "Proof/reconstruct.ML";
  16.468 +ML_file "Proof/proof_syntax.ML";
  16.469 +ML_file "Proof/proof_rewrite_rules.ML";
  16.470 +ML_file "Proof/proof_checker.ML";
  16.471 +ML_file "Proof/extraction.ML";
  16.472  
  16.473  (*Isabelle system*)
  16.474 -use "System/$ISABELLE_WINDOWS_PREFIX/bash.ML";
  16.475 -use "System/isabelle_system.ML";
  16.476 +ML_file "System/$ISABELLE_WINDOWS_PREFIX/bash.ML";
  16.477 +ML_file "System/isabelle_system.ML";
  16.478  
  16.479  
  16.480  (*theory documents*)
  16.481 -use "Thy/term_style.ML";
  16.482 -use "Isar/outer_syntax.ML";
  16.483 -use "Thy/thy_output.ML";
  16.484 -use "Thy/document_antiquotations.ML";
  16.485 -use "General/graph_display.ML";
  16.486 -use "Thy/present.ML";
  16.487 -use "pure_syn.ML";
  16.488 -use "PIDE/command.ML";
  16.489 -use "PIDE/query_operation.ML";
  16.490 -use "PIDE/resources.ML";
  16.491 -use "Thy/thy_info.ML";
  16.492 -use "PIDE/session.ML";
  16.493 -use "PIDE/protocol_message.ML";
  16.494 -use "PIDE/document.ML";
  16.495 +ML_file "Thy/term_style.ML";
  16.496 +ML_file "Isar/outer_syntax.ML";
  16.497 +ML_file "Thy/thy_output.ML";
  16.498 +ML_file "Thy/document_antiquotations.ML";
  16.499 +ML_file "General/graph_display.ML";
  16.500 +ML_file "Thy/present.ML";
  16.501 +ML_file "pure_syn.ML";
  16.502 +ML_file "PIDE/command.ML";
  16.503 +ML_file "PIDE/query_operation.ML";
  16.504 +ML_file "PIDE/resources.ML";
  16.505 +ML_file "Thy/thy_info.ML";
  16.506 +ML_file "PIDE/session.ML";
  16.507 +ML_file "PIDE/protocol_message.ML";
  16.508 +ML_file "PIDE/document.ML";
  16.509  
  16.510  (*theory and proof operations*)
  16.511 -use "Isar/isar_cmd.ML";
  16.512 +ML_file "Isar/isar_cmd.ML";
  16.513  
  16.514  
  16.515  (* Isabelle/Isar system *)
  16.516  
  16.517 -use "System/command_line.ML";
  16.518 -use "System/system_channel.ML";
  16.519 -use "System/message_channel.ML";
  16.520 -use "System/isabelle_process.ML";
  16.521 -use "System/invoke_scala.ML";
  16.522 -use "PIDE/protocol.ML";
  16.523 +ML_file "System/command_line.ML";
  16.524 +ML_file "System/system_channel.ML";
  16.525 +ML_file "System/message_channel.ML";
  16.526 +ML_file "System/isabelle_process.ML";
  16.527 +ML_file "System/invoke_scala.ML";
  16.528 +ML_file "PIDE/protocol.ML";
  16.529  
  16.530  
  16.531  (* miscellaneous tools and packages for Pure Isabelle *)
  16.532  
  16.533 -use "ML/ml_pp.ML";
  16.534 -use "ML/ml_antiquotations.ML";
  16.535 -use "ML/ml_thms.ML";
  16.536 -use "ML/ml_file.ML";
  16.537 +ML_file "ML/ml_pp.ML";
  16.538 +ML_file "ML/ml_antiquotations.ML";
  16.539 +ML_file "ML/ml_thms.ML";
  16.540 +ML_file "ML/ml_file.ML";
  16.541  
  16.542 -use "Tools/build.ML";
  16.543 -use "Tools/named_thms.ML";
  16.544 -use "Tools/print_operation.ML";
  16.545 -use "Tools/bibtex.ML";
  16.546 -use "Tools/rail.ML";
  16.547 -use "Tools/rule_insts.ML";
  16.548 -use "Tools/thm_deps.ML";
  16.549 -use "Tools/thy_deps.ML";
  16.550 -use "Tools/class_deps.ML";
  16.551 -use "Tools/find_theorems.ML";
  16.552 -use "Tools/find_consts.ML";
  16.553 -use "Tools/simplifier_trace.ML";
  16.554 -use_no_debug "Tools/debugger.ML";
  16.555 -use "Tools/named_theorems.ML";
  16.556 -use "Tools/jedit.ML";
  16.557 +ML_file "Tools/build.ML";
  16.558 +ML_file "Tools/named_thms.ML";
  16.559 +ML_file "Tools/print_operation.ML";
  16.560 +ML_file "Tools/bibtex.ML";
  16.561 +ML_file "Tools/rail.ML";
  16.562 +ML_file "Tools/rule_insts.ML";
  16.563 +ML_file "Tools/thm_deps.ML";
  16.564 +ML_file "Tools/thy_deps.ML";
  16.565 +ML_file "Tools/class_deps.ML";
  16.566 +ML_file "Tools/find_theorems.ML";
  16.567 +ML_file "Tools/find_consts.ML";
  16.568 +ML_file "Tools/simplifier_trace.ML";
  16.569 +ML_file_no_debug "Tools/debugger.ML";
  16.570 +ML_file "Tools/named_theorems.ML";
  16.571 +ML_file "Tools/jedit.ML";
  16.572  
  16.573  (* :mode=isabelle: *)
    17.1 --- a/src/Pure/ROOT0.ML	Thu Apr 07 15:32:47 2016 +0200
    17.2 +++ b/src/Pure/ROOT0.ML	Thu Apr 07 16:53:43 2016 +0200
    17.3 @@ -1,3 +1,3 @@
    17.4  (*** Isabelle/Pure bootstrap: initial setup ***)
    17.5  
    17.6 -use "Concurrent/thread_data.ML";
    17.7 +ML_file "Concurrent/thread_data.ML";
    18.1 --- a/src/Pure/ROOT1.ML	Thu Apr 07 15:32:47 2016 +0200
    18.2 +++ b/src/Pure/ROOT1.ML	Thu Apr 07 16:53:43 2016 +0200
    18.3 @@ -3,4 +3,4 @@
    18.4  use_thy "Pure";
    18.5  use_thy "ML_Bootstrap";
    18.6  
    18.7 -use "ML/ml_pervasive1.ML";
    18.8 +ML_file "ML/ml_pervasive1.ML";
    19.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 07 15:32:47 2016 +0200
    19.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 07 16:53:43 2016 +0200
    19.3 @@ -20,10 +20,15 @@
    19.4  
    19.5    def pure_name(name: String): Boolean = name == "Pure"
    19.6  
    19.7 -  val pure_roots: List[Path] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML").map(Path.explode(_))
    19.8 +  val pure_roots: List[String] = List("ROOT0.ML", "ROOT.ML", "ROOT1.ML")
    19.9  
   19.10 -  def pure_files(dir: Path): List[Path] =
   19.11 -    (pure_roots ::: pure_roots.flatMap(root => ML_Root.read_files(dir + root))).map(dir + _)
   19.12 +  def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
   19.13 +  {
   19.14 +    val loaded_files =
   19.15 +      pure_roots.flatMap(root =>
   19.16 +        resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
   19.17 +    (pure_roots ::: loaded_files).map(file => dir + Path.explode(file))
   19.18 +  }
   19.19  
   19.20  
   19.21    /* info */
    20.1 --- a/src/Pure/Tools/build.scala	Thu Apr 07 15:32:47 2016 +0200
    20.2 +++ b/src/Pure/Tools/build.scala	Thu Apr 07 16:53:43 2016 +0200
    20.3 @@ -174,9 +174,12 @@
    20.4  
    20.5              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    20.6              val loaded_files =
    20.7 -              if (inlined_files)
    20.8 -                (if (Sessions.pure_name(name)) Sessions.pure_files(info.dir) else Nil) :::
    20.9 -                  thy_deps.loaded_files
   20.10 +              if (inlined_files) {
   20.11 +                val pure_files =
   20.12 +                  if (Sessions.pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
   20.13 +                  else Nil
   20.14 +                pure_files ::: thy_deps.loaded_files
   20.15 +              }
   20.16                else Nil
   20.17  
   20.18              val all_files =
   20.19 @@ -257,7 +260,7 @@
   20.20        Future.thread("build") {
   20.21          val process =
   20.22            if (Sessions.pure_name(name)) {
   20.23 -            val roots = Sessions.pure_roots.flatMap(root => List("--use", File.platform_path(root)))
   20.24 +            val roots = Sessions.pure_roots.flatMap(root => List("--use", root))
   20.25              val eval =
   20.26                "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
   20.27                " Session.shutdown (); ML_Heap.share_common_data (); " + output_save_state + "));"
    21.1 --- a/src/Pure/Tools/debugger.ML	Thu Apr 07 15:32:47 2016 +0200
    21.2 +++ b/src/Pure/Tools/debugger.ML	Thu Apr 07 16:53:43 2016 +0200
    21.3 @@ -135,7 +135,7 @@
    21.4  
    21.5  fun evaluate {SML, verbose} =
    21.6    ML_Context.eval
    21.7 -    {SML_syntax = SML, SML_env = SML, exchange = false, redirect = false, verbose = verbose,
    21.8 +    {SML = SML, exchange = false, redirect = false, verbose = verbose,
    21.9        debug = SOME false, writeln = writeln_message, warning = warning_message}
   21.10      Position.none;
   21.11  
    22.1 --- a/src/Pure/Tools/ml_process.scala	Thu Apr 07 15:32:47 2016 +0200
    22.2 +++ b/src/Pure/Tools/ml_process.scala	Thu Apr 07 16:53:43 2016 +0200
    22.3 @@ -39,6 +39,7 @@
    22.4      val eval_init =
    22.5        if (heaps.isEmpty) {
    22.6          List(
    22.7 +          "val ML_file = PolyML.use",
    22.8            if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") "structure FixedInt = IntInf"
    22.9            else "",
   22.10            if (Platform.is_windows)
    23.1 --- a/src/Pure/build-jars	Thu Apr 07 15:32:47 2016 +0200
    23.2 +++ b/src/Pure/build-jars	Thu Apr 07 16:53:43 2016 +0200
    23.3 @@ -54,7 +54,6 @@
    23.4    Isar/parse.scala
    23.5    Isar/token.scala
    23.6    ML/ml_lex.scala
    23.7 -  ML/ml_root.scala
    23.8    ML/ml_syntax.scala
    23.9    PIDE/batch_session.scala
   23.10    PIDE/command.scala
    24.1 --- a/src/Tools/Code/code_runtime.ML	Thu Apr 07 15:32:47 2016 +0200
    24.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Apr 07 16:53:43 2016 +0200
    24.3 @@ -81,7 +81,7 @@
    24.4  fun exec ctxt verbose code =
    24.5   (if Config.get ctxt trace then tracing code else ();
    24.6    ML_Context.exec (fn () =>
    24.7 -    ML_Compiler0.use_text ML_Env.context
    24.8 +    ML_Compiler0.ML ML_Env.context
    24.9        {line = 0, file = "generated code", verbose = verbose, debug = false} code));
   24.10  
   24.11  fun value ctxt (get, put, put_ml) (prelude, value) =
   24.12 @@ -536,7 +536,7 @@
   24.13      val thy' = Loaded_Values.put [] thy;
   24.14      val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
   24.15      val _ =
   24.16 -      ML_Compiler0.use_text notifying_context
   24.17 +      ML_Compiler0.ML notifying_context
   24.18          {line = 0, file = Path.implode filepath, verbose = false, debug = false}
   24.19          (File.read filepath);
   24.20      val thy'' = Context.the_global_context ();
    25.1 --- a/src/Tools/Spec_Check/spec_check.ML	Thu Apr 07 15:32:47 2016 +0200
    25.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Thu Apr 07 16:53:43 2016 +0200
    25.3 @@ -136,7 +136,7 @@
    25.4      val _ =
    25.5        Context.setmp_generic_context (SOME (Context.Proof ctxt))
    25.6          (fn () =>
    25.7 -          ML_Compiler0.use_text context
    25.8 +          ML_Compiler0.ML context
    25.9              {line = 0, file = "generated code", verbose = true, debug = false} s) ()
   25.10    in
   25.11      Gen_Construction.parse_pred (! return)
   25.12 @@ -146,7 +146,7 @@
   25.13  fun run_test ctxt s =
   25.14    Context.setmp_generic_context (SOME (Context.Proof ctxt))
   25.15      (fn () =>
   25.16 -      ML_Compiler0.use_text ML_Env.context
   25.17 +      ML_Compiler0.ML ML_Env.context
   25.18          {line = 0, file = "generated code", verbose = false, debug = false} s) ();
   25.19  
   25.20  (*split input into tokens*)