added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
authorwenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25)
changeset 56275600f432ab556
parent 56274 71eab6907eee
child 56276 9e2d5e3debd3
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Doc/IsarRef/Spec.thy
src/Doc/antiquote_setup.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/ML-Systems/ml_name_space.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_thms.ML
src/Pure/Pure.thy
src/Pure/Thy/thy_output.ML
src/Pure/pure_syn.ML
     1.1 --- a/NEWS	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -38,6 +38,11 @@
     1.4  "exception_trace", which may be also declared within the context via
     1.5  "declare [[exception_trace = true]]".  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Command 'SML_file' reads and evaluates the given Standard ML file.
     1.8 +Toplevel bindings are stored within the theory context; the initial
     1.9 +environment is restricted to the Standard ML implementation of
    1.10 +Poly/ML, without the add-ons of Isabelle/ML.
    1.11 +
    1.12  
    1.13  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.14  
     2.1 --- a/etc/isar-keywords-ZF.el	Tue Mar 25 10:37:10 2014 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Tue Mar 25 13:18:10 2014 +0100
     2.3 @@ -20,6 +20,7 @@
     2.4      "ProofGeneral\\.process_pgip"
     2.5      "ProofGeneral\\.restart"
     2.6      "ProofGeneral\\.undo"
     2.7 +    "SML_file"
     2.8      "abbreviation"
     2.9      "also"
    2.10      "apply"
    2.11 @@ -344,6 +345,7 @@
    2.12  (defconst isar-keywords-theory-decl
    2.13    '("ML"
    2.14      "ML_file"
    2.15 +    "SML_file"
    2.16      "abbreviation"
    2.17      "attribute_setup"
    2.18      "axiomatization"
     3.1 --- a/etc/isar-keywords.el	Tue Mar 25 10:37:10 2014 +0100
     3.2 +++ b/etc/isar-keywords.el	Tue Mar 25 13:18:10 2014 +0100
     3.3 @@ -20,6 +20,7 @@
     3.4      "ProofGeneral\\.process_pgip"
     3.5      "ProofGeneral\\.restart"
     3.6      "ProofGeneral\\.undo"
     3.7 +    "SML_file"
     3.8      "abbreviation"
     3.9      "adhoc_overloading"
    3.10      "also"
    3.11 @@ -482,6 +483,7 @@
    3.12  (defconst isar-keywords-theory-decl
    3.13    '("ML"
    3.14      "ML_file"
    3.15 +    "SML_file"
    3.16      "abbreviation"
    3.17      "adhoc_overloading"
    3.18      "atom_decl"
     4.1 --- a/src/Doc/IsarRef/Spec.thy	Tue Mar 25 10:37:10 2014 +0100
     4.2 +++ b/src/Doc/IsarRef/Spec.thy	Tue Mar 25 13:18:10 2014 +0100
     4.3 @@ -1000,6 +1000,7 @@
     4.4  
     4.5  text {*
     4.6    \begin{matharray}{rcl}
     4.7 +    @{command_def "SML_file"} & : & @{text "theory \<rightarrow> theory"} \\
     4.8      @{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     4.9      @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    4.10      @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
    4.11 @@ -1011,7 +1012,7 @@
    4.12    \end{matharray}
    4.13  
    4.14    @{rail \<open>
    4.15 -    @@{command ML_file} @{syntax name}
    4.16 +    (@@{command SML_file} | @@{command ML_file}) @{syntax name}
    4.17      ;
    4.18      (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
    4.19        @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
    4.20 @@ -1021,6 +1022,14 @@
    4.21  
    4.22    \begin{description}
    4.23  
    4.24 +  \item @{command "SML_file"}~@{text "name"} reads and evaluates the
    4.25 +  given Standard ML file.  Top-level SML bindings are stored within
    4.26 +  the theory context; the initial environment is restricted to the
    4.27 +  Standard ML implementation of Poly/ML, without the many add-ons of
    4.28 +  Isabelle/ML.  Multiple @{command "SML_file"} commands may be used to
    4.29 +  build larger Standard ML projects, independently of the regular
    4.30 +  Isabelle/ML environment.
    4.31 +
    4.32    \item @{command "ML_file"}~@{text "name"} reads and evaluates the
    4.33    given ML file.  The current theory context is passed down to the ML
    4.34    toplevel and may be modified, using @{ML "Context.>>"} or derived ML
     5.1 --- a/src/Doc/antiquote_setup.ML	Tue Mar 25 10:37:10 2014 +0100
     5.2 +++ b/src/Doc/antiquote_setup.ML	Tue Mar 25 13:18:10 2014 +0100
     5.3 @@ -99,7 +99,9 @@
     5.4          else txt1 ^ " : " ^ txt2;
     5.5        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     5.6  
     5.7 -      val _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2));
     5.8 +      val _ =
     5.9 +        ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1)
    5.10 +          (ml (toks1, toks2));
    5.11        val kind' = if kind = "" then "ML" else "ML " ^ kind;
    5.12      in
    5.13        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
     6.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 10:37:10 2014 +0100
     6.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 13:18:10 2014 +0100
     6.3 @@ -120,7 +120,7 @@
     6.4            ML_Lex.read Position.none "fn _ => (" @
     6.5            ML_Lex.read_source source @
     6.6            ML_Lex.read Position.none ");";
     6.7 -        val _ = ML_Context.eval_in (SOME context) false (#pos source) toks;
     6.8 +        val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
     6.9        in "" end);
    6.10  *}
    6.11  
     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 10:37:10 2014 +0100
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 13:18:10 2014 +0100
     7.3 @@ -145,7 +145,8 @@
     7.4          \  val " ^ name ^
     7.5          " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
     7.6          \end;\n");
     7.7 -  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end;
     7.8 +    val flags = {SML = false, verbose = false};
     7.9 +  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end;
    7.10  
    7.11  
    7.12  (* old-style defs *)
    7.13 @@ -238,7 +239,7 @@
    7.14    let val opt_ctxt =
    7.15      try Toplevel.generic_theory_of state
    7.16      |> Option.map (Context.proof_of #> Diag_State.put state)
    7.17 -  in ML_Context.eval_source_in opt_ctxt verbose source end);
    7.18 +  in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end);
    7.19  
    7.20  val diag_state = Diag_State.get;
    7.21  
     8.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Mar 25 10:37:10 2014 +0100
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 25 13:18:10 2014 +0100
     8.3 @@ -268,17 +268,28 @@
     8.4  (* use ML text *)
     8.5  
     8.6  val _ =
     8.7 +  Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file"
     8.8 +    (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
     8.9 +        let
    8.10 +          val ([{lines, pos, ...}], thy') = files thy;
    8.11 +          val source = {delimited = true, text = cat_lines lines, pos = pos};
    8.12 +        in
    8.13 +          thy' |> Context.theory_map
    8.14 +            (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source))
    8.15 +        end)));
    8.16 +
    8.17 +val _ =
    8.18    Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
    8.19      (Parse.ML_source >> (fn source =>
    8.20        Toplevel.generic_theory
    8.21 -        (ML_Context.exec (fn () => ML_Context.eval_source true source) #>
    8.22 +        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #>
    8.23            Local_Theory.propagate_ml_env)));
    8.24  
    8.25  val _ =
    8.26    Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
    8.27      (Parse.ML_source >> (fn source =>
    8.28        Toplevel.proof (Proof.map_context (Context.proof_map
    8.29 -        (ML_Context.exec (fn () => ML_Context.eval_source true source))) #>
    8.30 +        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #>
    8.31            Proof.propagate_ml_env)));
    8.32  
    8.33  val _ =
     9.1 --- a/src/Pure/ML-Systems/ml_name_space.ML	Tue Mar 25 10:37:10 2014 +0100
     9.2 +++ b/src/Pure/ML-Systems/ml_name_space.ML	Tue Mar 25 13:18:10 2014 +0100
     9.3 @@ -54,4 +54,11 @@
     9.4    allSig = fn _ => [],
     9.5    allFunct = fn _ => []};
     9.6  
     9.7 +val initial_val : (string * valueVal) list = [];
     9.8 +val initial_type : (string * typeVal) list = [];
     9.9 +val initial_fixity : (string * fixityVal) list = [];
    9.10 +val initial_structure : (string * structureVal) list = [];
    9.11 +val initial_signature : (string * signatureVal) list = [];
    9.12 +val initial_functor : (string * functorVal) list = [];
    9.13 +
    9.14  end;
    10.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 10:37:10 2014 +0100
    10.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 13:18:10 2014 +0100
    10.3 @@ -4,6 +4,24 @@
    10.4  Compatibility wrapper for Poly/ML.
    10.5  *)
    10.6  
    10.7 +(* ML name space *)
    10.8 +
    10.9 +structure ML_Name_Space =
   10.10 +struct
   10.11 +  open PolyML.NameSpace;
   10.12 +  type T = PolyML.NameSpace.nameSpace;
   10.13 +  val global = PolyML.globalNameSpace;
   10.14 +  val initial_val =
   10.15 +    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
   10.16 +      (#allVal global ());
   10.17 +  val initial_type = #allType global ();
   10.18 +  val initial_fixity = #allFix global ();
   10.19 +  val initial_structure = #allStruct global ();
   10.20 +  val initial_signature = #allSig global ();
   10.21 +  val initial_functor = #allFunct global ();
   10.22 +end;
   10.23 +
   10.24 +
   10.25  (* ML system operations *)
   10.26  
   10.27  use "ML-Systems/ml_system.ML";
   10.28 @@ -94,13 +112,6 @@
   10.29  
   10.30  (* ML compiler *)
   10.31  
   10.32 -structure ML_Name_Space =
   10.33 -struct
   10.34 -  open PolyML.NameSpace;
   10.35 -  type T = PolyML.NameSpace.nameSpace;
   10.36 -  val global = PolyML.globalNameSpace;
   10.37 -end;
   10.38 -
   10.39  use "ML-Systems/use_context.ML";
   10.40  use "ML-Systems/compiler_polyml.ML";
   10.41  
    11.1 --- a/src/Pure/ML/ml_compiler.ML	Tue Mar 25 10:37:10 2014 +0100
    11.2 +++ b/src/Pure/ML/ml_compiler.ML	Tue Mar 25 13:18:10 2014 +0100
    11.3 @@ -11,7 +11,8 @@
    11.4    val exn_message: exn -> string
    11.5    val exn_error_message: exn -> unit
    11.6    val exn_trace: (unit -> 'a) -> 'a
    11.7 -  val eval: bool -> Position.T -> ML_Lex.token list -> unit
    11.8 +  type flags = {SML: bool, verbose: bool}
    11.9 +  val eval: flags -> Position.T -> ML_Lex.token list -> unit
   11.10  end
   11.11  
   11.12  structure ML_Compiler: ML_COMPILER =
   11.13 @@ -28,8 +29,11 @@
   11.14  val exn_error_message = Output.error_message o exn_message;
   11.15  fun exn_trace e = print_exception_trace exn_message e;
   11.16  
   11.17 -fun eval verbose pos toks =
   11.18 +type flags = {SML: bool, verbose: bool};
   11.19 +
   11.20 +fun eval {SML, verbose} pos toks =
   11.21    let
   11.22 +    val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
   11.23      val line = the_default 1 (Position.line_of pos);
   11.24      val file = the_default "ML" (Position.file_of pos);
   11.25      val text = ML_Lex.flatten toks;
    12.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Tue Mar 25 10:37:10 2014 +0100
    12.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Tue Mar 25 13:18:10 2014 +0100
    12.3 @@ -74,10 +74,12 @@
    12.4  
    12.5  (* eval ML source tokens *)
    12.6  
    12.7 -fun eval verbose pos toks =
    12.8 +type flags = {SML: bool, verbose: bool};
    12.9 +
   12.10 +fun eval {SML, verbose} pos toks =
   12.11    let
   12.12      val _ = Secure.secure_mltext ();
   12.13 -    val space = ML_Env.name_space;
   12.14 +    val space = if SML then ML_Env.SML_name_space else ML_Env.name_space;
   12.15      val opt_context = Context.thread_data ();
   12.16  
   12.17  
    13.1 --- a/src/Pure/ML/ml_context.ML	Tue Mar 25 10:37:10 2014 +0100
    13.2 +++ b/src/Pure/ML/ml_context.ML	Tue Mar 25 13:18:10 2014 +0100
    13.3 @@ -21,12 +21,12 @@
    13.4    val trace: bool Config.T
    13.5    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    13.6      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
    13.7 -  val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
    13.8 -  val eval_file: bool -> Path.T -> unit
    13.9 -  val eval_source: bool -> Symbol_Pos.source -> unit
   13.10 -  val eval_in: Proof.context option -> bool -> Position.T ->
   13.11 +  val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   13.12 +  val eval_file: ML_Compiler.flags -> Path.T -> unit
   13.13 +  val eval_source: ML_Compiler.flags -> Symbol_Pos.source -> unit
   13.14 +  val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
   13.15      ML_Lex.token Antiquote.antiquote list -> unit
   13.16 -  val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> unit
   13.17 +  val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
   13.18    val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
   13.19      Context.generic -> Context.generic
   13.20  end
   13.21 @@ -140,8 +140,10 @@
   13.22  val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
   13.23  val trace = Config.bool trace_raw;
   13.24  
   13.25 -fun eval verbose pos ants =
   13.26 +fun eval flags pos ants =
   13.27    let
   13.28 +    val non_verbose = {SML = #SML flags, verbose = false};
   13.29 +
   13.30      (*prepare source text*)
   13.31      val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
   13.32      val _ =
   13.33 @@ -157,11 +159,11 @@
   13.34      val _ =
   13.35        Context.setmp_thread_data
   13.36          (Option.map (Context.mapping I (Context_Position.set_visible false)) env_ctxt)
   13.37 -        (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) ()
   13.38 +        (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
   13.39        |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
   13.40  
   13.41 -    val _ = ML_Compiler.eval verbose pos body;
   13.42 -    val _ = ML_Compiler.eval false Position.none reset_env;
   13.43 +    val _ = ML_Compiler.eval flags pos body;
   13.44 +    val _ = ML_Compiler.eval non_verbose Position.none reset_env;
   13.45    in () end;
   13.46  
   13.47  end;
   13.48 @@ -169,29 +171,29 @@
   13.49  
   13.50  (* derived versions *)
   13.51  
   13.52 -fun eval_file verbose path =
   13.53 +fun eval_file flags path =
   13.54    let val pos = Path.position path
   13.55 -  in eval verbose pos (ML_Lex.read pos (File.read path)) end;
   13.56 +  in eval flags pos (ML_Lex.read pos (File.read path)) end;
   13.57  
   13.58 -fun eval_source verbose source =
   13.59 -  eval verbose (#pos source) (ML_Lex.read_source source);
   13.60 +fun eval_source flags source =
   13.61 +  eval flags (#pos source) (ML_Lex.read_source source);
   13.62  
   13.63 -fun eval_in ctxt verbose pos ants =
   13.64 +fun eval_in ctxt flags pos ants =
   13.65    Context.setmp_thread_data (Option.map Context.Proof ctxt)
   13.66 -    (fn () => eval verbose pos ants) ();
   13.67 +    (fn () => eval flags pos ants) ();
   13.68  
   13.69 -fun eval_source_in ctxt verbose source =
   13.70 +fun eval_source_in ctxt flags source =
   13.71    Context.setmp_thread_data (Option.map Context.Proof ctxt)
   13.72 -    (fn () => eval_source verbose source) ();
   13.73 +    (fn () => eval_source flags source) ();
   13.74  
   13.75  fun expression pos bind body ants =
   13.76 -  exec (fn () => eval false pos
   13.77 +  exec (fn () => eval {SML = false, verbose = false} pos
   13.78      (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
   13.79        ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
   13.80  
   13.81  end;
   13.82  
   13.83  fun use s =
   13.84 -  ML_Context.eval_file true (Path.explode s)
   13.85 +  ML_Context.eval_file {SML = false, verbose = true} (Path.explode s)
   13.86      handle ERROR msg => (writeln msg; error "ML error");
   13.87  
    14.1 --- a/src/Pure/ML/ml_env.ML	Tue Mar 25 10:37:10 2014 +0100
    14.2 +++ b/src/Pure/ML/ml_env.ML	Tue Mar 25 13:18:10 2014 +0100
    14.3 @@ -1,12 +1,14 @@
    14.4  (*  Title:      Pure/ML/ml_env.ML
    14.5      Author:     Makarius
    14.6  
    14.7 -Local environment of ML results.
    14.8 +Toplevel environment for Standard ML and Isabelle/ML within the
    14.9 +implicit context.
   14.10  *)
   14.11  
   14.12  signature ML_ENV =
   14.13  sig
   14.14    val inherit: Context.generic -> Context.generic -> Context.generic
   14.15 +  val SML_name_space: ML_Name_Space.T
   14.16    val name_space: ML_Name_Space.T
   14.17    val local_context: use_context
   14.18    val check_functor: string -> unit
   14.19 @@ -17,56 +19,112 @@
   14.20  
   14.21  (* context data *)
   14.22  
   14.23 +type tables =
   14.24 +  ML_Name_Space.valueVal Symtab.table *
   14.25 +  ML_Name_Space.typeVal Symtab.table *
   14.26 +  ML_Name_Space.fixityVal Symtab.table *
   14.27 +  ML_Name_Space.structureVal Symtab.table *
   14.28 +  ML_Name_Space.signatureVal Symtab.table *
   14.29 +  ML_Name_Space.functorVal Symtab.table;
   14.30 +
   14.31 +fun merge_tables
   14.32 +  ((val1, type1, fixity1, structure1, signature1, functor1),
   14.33 +   (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
   14.34 +  (Symtab.merge (K true) (val1, val2),
   14.35 +   Symtab.merge (K true) (type1, type2),
   14.36 +   Symtab.merge (K true) (fixity1, fixity2),
   14.37 +   Symtab.merge (K true) (structure1, structure2),
   14.38 +   Symtab.merge (K true) (signature1, signature2),
   14.39 +   Symtab.merge (K true) (functor1, functor2));
   14.40 +
   14.41 +type data = {bootstrap: bool, tables: tables, sml_tables: tables};
   14.42 +
   14.43 +fun make_data (bootstrap, tables, sml_tables) : data =
   14.44 +  {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables};
   14.45 +
   14.46  structure Env = Generic_Data
   14.47  (
   14.48 -  type T =
   14.49 -    bool * (*global bootstrap environment*)
   14.50 -     (ML_Name_Space.valueVal Symtab.table *
   14.51 -      ML_Name_Space.typeVal Symtab.table *
   14.52 -      ML_Name_Space.fixityVal Symtab.table *
   14.53 -      ML_Name_Space.structureVal Symtab.table *
   14.54 -      ML_Name_Space.signatureVal Symtab.table *
   14.55 -      ML_Name_Space.functorVal Symtab.table);
   14.56 -  val empty : T =
   14.57 -    (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
   14.58 -  fun extend (_, tabs) : T = (false, tabs);
   14.59 -  fun merge
   14.60 -   ((_, (val1, type1, fixity1, structure1, signature1, functor1)),
   14.61 -    (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
   14.62 -    (false,
   14.63 -     (Symtab.merge (K true) (val1, val2),
   14.64 -      Symtab.merge (K true) (type1, type2),
   14.65 -      Symtab.merge (K true) (fixity1, fixity2),
   14.66 -      Symtab.merge (K true) (structure1, structure2),
   14.67 -      Symtab.merge (K true) (signature1, signature2),
   14.68 -      Symtab.merge (K true) (functor1, functor2)));
   14.69 +  type T = data
   14.70 +  val empty =
   14.71 +    make_data (true,
   14.72 +      (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
   14.73 +      (Symtab.make ML_Name_Space.initial_val,
   14.74 +       Symtab.make ML_Name_Space.initial_type,
   14.75 +       Symtab.make ML_Name_Space.initial_fixity,
   14.76 +       Symtab.make ML_Name_Space.initial_structure,
   14.77 +       Symtab.make ML_Name_Space.initial_signature,
   14.78 +       Symtab.make ML_Name_Space.initial_functor));
   14.79 +  fun extend (data : T) = make_data (false, #tables data, #sml_tables data);
   14.80 +  fun merge (data : T * T) =
   14.81 +    make_data (false,
   14.82 +      merge_tables (pairself #tables data),
   14.83 +      merge_tables (pairself #sml_tables data));
   14.84  );
   14.85  
   14.86  val inherit = Env.put o Env.get;
   14.87  
   14.88  
   14.89 -(* results *)
   14.90 +(* SML name space *)
   14.91 +
   14.92 +val SML_name_space: ML_Name_Space.T =
   14.93 +  let
   14.94 +    fun lookup which name =
   14.95 +      Context.the_thread_data ()
   14.96 +      |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
   14.97 +
   14.98 +    fun all which () =
   14.99 +      Context.the_thread_data ()
  14.100 +      |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
  14.101 +      |> sort_distinct (string_ord o pairself #1);
  14.102 +
  14.103 +    fun enter which entry =
  14.104 +      Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
  14.105 +        let val sml_tables' = which (Symtab.update entry) sml_tables
  14.106 +        in make_data (bootstrap, tables, sml_tables') end));
  14.107 +  in
  14.108 +   {lookupVal    = lookup #1,
  14.109 +    lookupType   = lookup #2,
  14.110 +    lookupFix    = lookup #3,
  14.111 +    lookupStruct = lookup #4,
  14.112 +    lookupSig    = lookup #5,
  14.113 +    lookupFunct  = lookup #6,
  14.114 +    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
  14.115 +    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
  14.116 +    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
  14.117 +    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
  14.118 +    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
  14.119 +    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
  14.120 +    allVal       = all #1,
  14.121 +    allType      = all #2,
  14.122 +    allFix       = all #3,
  14.123 +    allStruct    = all #4,
  14.124 +    allSig       = all #5,
  14.125 +    allFunct     = all #6}
  14.126 +  end;
  14.127 +
  14.128 +
  14.129 +(* Isabelle/ML name space *)
  14.130  
  14.131  val name_space: ML_Name_Space.T =
  14.132    let
  14.133      fun lookup sel1 sel2 name =
  14.134        Context.thread_data ()
  14.135 -      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
  14.136 +      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
  14.137        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
  14.138  
  14.139      fun all sel1 sel2 () =
  14.140        Context.thread_data ()
  14.141 -      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
  14.142 +      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
  14.143        |> append (sel2 ML_Name_Space.global ())
  14.144        |> sort_distinct (string_ord o pairself #1);
  14.145  
  14.146      fun enter ap1 sel2 entry =
  14.147        if is_some (Context.thread_data ()) then
  14.148 -        Context.>> (Env.map (fn (global, tabs) =>
  14.149 +        Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
  14.150            let
  14.151 -            val _ = if global then sel2 ML_Name_Space.global entry else ();
  14.152 -            val tabs' = ap1 (Symtab.update entry) tabs;
  14.153 -          in (global, tabs') end))
  14.154 +            val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
  14.155 +            val tables' = ap1 (Symtab.update entry) tables;
  14.156 +          in make_data (bootstrap, tables', sml_tables) end))
  14.157        else sel2 ML_Name_Space.global entry;
  14.158    in
  14.159     {lookupVal    = lookup #1 #lookupVal,
    15.1 --- a/src/Pure/ML/ml_thms.ML	Tue Mar 25 10:37:10 2014 +0100
    15.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Mar 25 13:18:10 2014 +0100
    15.3 @@ -130,7 +130,7 @@
    15.4        else if not (ML_Syntax.is_identifier name) then
    15.5          error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
    15.6        else
    15.7 -        ML_Compiler.eval true Position.none
    15.8 +        ML_Compiler.eval {SML = false, verbose = true} Position.none
    15.9            (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
   15.10      val _ = Theory.setup (Stored_Thms.put []);
   15.11    in () end;
    16.1 --- a/src/Pure/Pure.thy	Tue Mar 25 10:37:10 2014 +0100
    16.2 +++ b/src/Pure/Pure.thy	Tue Mar 25 13:18:10 2014 +0100
    16.3 @@ -14,7 +14,7 @@
    16.4      "infixr" "is" "keywords" "notes" "obtains" "open" "output"
    16.5      "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
    16.6    and "theory" :: thy_begin % "theory"
    16.7 -  and "ML_file" :: thy_load % "ML"
    16.8 +  and "SML_file" "ML_file" :: thy_load % "ML"
    16.9    and "header" :: diag
   16.10    and "chapter" :: thy_heading1
   16.11    and "section" :: thy_heading2
    17.1 --- a/src/Pure/Thy/thy_output.ML	Tue Mar 25 10:37:10 2014 +0100
    17.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Mar 25 13:18:10 2014 +0100
    17.3 @@ -639,7 +639,7 @@
    17.4  
    17.5  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
    17.6    (fn {context, ...} => fn source =>
    17.7 -   (ML_Context.eval_in (SOME context) false (#pos source) (ml source);
    17.8 +   (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source);
    17.9      Symbol_Pos.source_content source
   17.10      |> #1
   17.11      |> (if Config.get context quotes then quote else I)
    18.1 --- a/src/Pure/pure_syn.ML	Tue Mar 25 10:37:10 2014 +0100
    18.2 +++ b/src/Pure/pure_syn.ML	Tue Mar 25 13:18:10 2014 +0100
    18.3 @@ -25,7 +25,7 @@
    18.4            val source = {delimited = true, text = cat_lines lines, pos = pos};
    18.5          in
    18.6            gthy
    18.7 -          |> ML_Context.exec (fn () => ML_Context.eval_source true source)
    18.8 +          |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source)
    18.9            |> Local_Theory.propagate_ml_env
   18.10            |> Context.mapping provide (Local_Theory.background_theory provide)
   18.11          end)));