# HG changeset patch # User wenzelm # Date 1395749890 -3600 # Node ID 600f432ab55693e63007e5327e4b8f7980418ab9 # Parent 71eab6907eee1c2e4fb53267c85ac93ca9306b8f added command 'SML_file' for Standard ML without Isabelle/ML add-ons; diff -r 71eab6907eee -r 600f432ab556 NEWS --- a/NEWS Tue Mar 25 10:37:10 2014 +0100 +++ b/NEWS Tue Mar 25 13:18:10 2014 +0100 @@ -38,6 +38,11 @@ "exception_trace", which may be also declared within the context via "declare [[exception_trace = true]]". Minor INCOMPATIBILITY. +* Command 'SML_file' reads and evaluates the given Standard ML file. +Toplevel bindings are stored within the theory context; the initial +environment is restricted to the Standard ML implementation of +Poly/ML, without the add-ons of Isabelle/ML. + *** Prover IDE -- Isabelle/Scala/jEdit *** diff -r 71eab6907eee -r 600f432ab556 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Tue Mar 25 10:37:10 2014 +0100 +++ b/etc/isar-keywords-ZF.el Tue Mar 25 13:18:10 2014 +0100 @@ -20,6 +20,7 @@ "ProofGeneral\\.process_pgip" "ProofGeneral\\.restart" "ProofGeneral\\.undo" + "SML_file" "abbreviation" "also" "apply" @@ -344,6 +345,7 @@ (defconst isar-keywords-theory-decl '("ML" "ML_file" + "SML_file" "abbreviation" "attribute_setup" "axiomatization" diff -r 71eab6907eee -r 600f432ab556 etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Mar 25 10:37:10 2014 +0100 +++ b/etc/isar-keywords.el Tue Mar 25 13:18:10 2014 +0100 @@ -20,6 +20,7 @@ "ProofGeneral\\.process_pgip" "ProofGeneral\\.restart" "ProofGeneral\\.undo" + "SML_file" "abbreviation" "adhoc_overloading" "also" @@ -482,6 +483,7 @@ (defconst isar-keywords-theory-decl '("ML" "ML_file" + "SML_file" "abbreviation" "adhoc_overloading" "atom_decl" diff -r 71eab6907eee -r 600f432ab556 src/Doc/IsarRef/Spec.thy --- a/src/Doc/IsarRef/Spec.thy Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Doc/IsarRef/Spec.thy Tue Mar 25 13:18:10 2014 +0100 @@ -1000,6 +1000,7 @@ text {* \begin{matharray}{rcl} + @{command_def "SML_file"} & : & @{text "theory \ theory"} \\ @{command_def "ML_file"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "ML"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "ML_prf"} & : & @{text "proof \ proof"} \\ @@ -1011,7 +1012,7 @@ \end{matharray} @{rail \ - @@{command ML_file} @{syntax name} + (@@{command SML_file} | @@{command ML_file}) @{syntax name} ; (@@{command ML} | @@{command ML_prf} | @@{command ML_val} | @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text} @@ -1021,6 +1022,14 @@ \begin{description} + \item @{command "SML_file"}~@{text "name"} reads and evaluates the + given Standard ML file. Top-level SML bindings are stored within + the theory context; the initial environment is restricted to the + Standard ML implementation of Poly/ML, without the many add-ons of + Isabelle/ML. Multiple @{command "SML_file"} commands may be used to + build larger Standard ML projects, independently of the regular + Isabelle/ML environment. + \item @{command "ML_file"}~@{text "name"} reads and evaluates the given ML file. The current theory context is passed down to the ML toplevel and may be modified, using @{ML "Context.>>"} or derived ML diff -r 71eab6907eee -r 600f432ab556 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Tue Mar 25 13:18:10 2014 +0100 @@ -99,7 +99,9 @@ else txt1 ^ " : " ^ txt2; val txt' = if kind = "" then txt else kind ^ " " ^ txt; - val _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2)); + val _ = + ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1) + (ml (toks1, toks2)); val kind' = if kind = "" then "ML" else "ML " ^ kind; in "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ diff -r 71eab6907eee -r 600f432ab556 src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Tue Mar 25 10:37:10 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Tue Mar 25 13:18:10 2014 +0100 @@ -120,7 +120,7 @@ ML_Lex.read Position.none "fn _ => (" @ ML_Lex.read_source source @ ML_Lex.read Position.none ");"; - val _ = ML_Context.eval_in (SOME context) false (#pos source) toks; + val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks; in "" end); *} diff -r 71eab6907eee -r 600f432ab556 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Mar 25 13:18:10 2014 +0100 @@ -145,7 +145,8 @@ \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\ \end;\n"); - in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end; + val flags = {SML = false, verbose = false}; + in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end; (* old-style defs *) @@ -238,7 +239,7 @@ let val opt_ctxt = try Toplevel.generic_theory_of state |> Option.map (Context.proof_of #> Diag_State.put state) - in ML_Context.eval_source_in opt_ctxt verbose source end); + in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end); val diag_state = Diag_State.get; diff -r 71eab6907eee -r 600f432ab556 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Mar 25 13:18:10 2014 +0100 @@ -268,17 +268,28 @@ (* use ML text *) val _ = + Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file" + (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy => + let + val ([{lines, pos, ...}], thy') = files thy; + val source = {delimited = true, text = cat_lines lines, pos = pos}; + in + thy' |> Context.theory_map + (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source)) + end))); + +val _ = Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory" (Parse.ML_source >> (fn source => Toplevel.generic_theory - (ML_Context.exec (fn () => ML_Context.eval_source true source) #> + (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #> Local_Theory.propagate_ml_env))); val _ = Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map - (ML_Context.exec (fn () => ML_Context.eval_source true source))) #> + (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #> Proof.propagate_ml_env))); val _ = diff -r 71eab6907eee -r 600f432ab556 src/Pure/ML-Systems/ml_name_space.ML --- a/src/Pure/ML-Systems/ml_name_space.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/ML-Systems/ml_name_space.ML Tue Mar 25 13:18:10 2014 +0100 @@ -54,4 +54,11 @@ allSig = fn _ => [], allFunct = fn _ => []}; +val initial_val : (string * valueVal) list = []; +val initial_type : (string * typeVal) list = []; +val initial_fixity : (string * fixityVal) list = []; +val initial_structure : (string * structureVal) list = []; +val initial_signature : (string * signatureVal) list = []; +val initial_functor : (string * functorVal) list = []; + end; diff -r 71eab6907eee -r 600f432ab556 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Tue Mar 25 13:18:10 2014 +0100 @@ -4,6 +4,24 @@ Compatibility wrapper for Poly/ML. *) +(* ML name space *) + +structure ML_Name_Space = +struct + open PolyML.NameSpace; + type T = PolyML.NameSpace.nameSpace; + val global = PolyML.globalNameSpace; + val initial_val = + List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit") + (#allVal global ()); + val initial_type = #allType global (); + val initial_fixity = #allFix global (); + val initial_structure = #allStruct global (); + val initial_signature = #allSig global (); + val initial_functor = #allFunct global (); +end; + + (* ML system operations *) use "ML-Systems/ml_system.ML"; @@ -94,13 +112,6 @@ (* ML compiler *) -structure ML_Name_Space = -struct - open PolyML.NameSpace; - type T = PolyML.NameSpace.nameSpace; - val global = PolyML.globalNameSpace; -end; - use "ML-Systems/use_context.ML"; use "ML-Systems/compiler_polyml.ML"; diff -r 71eab6907eee -r 600f432ab556 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/ML/ml_compiler.ML Tue Mar 25 13:18:10 2014 +0100 @@ -11,7 +11,8 @@ val exn_message: exn -> string val exn_error_message: exn -> unit val exn_trace: (unit -> 'a) -> 'a - val eval: bool -> Position.T -> ML_Lex.token list -> unit + type flags = {SML: bool, verbose: bool} + val eval: flags -> Position.T -> ML_Lex.token list -> unit end structure ML_Compiler: ML_COMPILER = @@ -28,8 +29,11 @@ val exn_error_message = Output.error_message o exn_message; fun exn_trace e = print_exception_trace exn_message e; -fun eval verbose pos toks = +type flags = {SML: bool, verbose: bool}; + +fun eval {SML, verbose} pos toks = let + val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else (); val line = the_default 1 (Position.line_of pos); val file = the_default "ML" (Position.file_of pos); val text = ML_Lex.flatten toks; diff -r 71eab6907eee -r 600f432ab556 src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/ML/ml_compiler_polyml.ML Tue Mar 25 13:18:10 2014 +0100 @@ -74,10 +74,12 @@ (* eval ML source tokens *) -fun eval verbose pos toks = +type flags = {SML: bool, verbose: bool}; + +fun eval {SML, verbose} pos toks = let val _ = Secure.secure_mltext (); - val space = ML_Env.name_space; + val space = if SML then ML_Env.SML_name_space else ML_Env.name_space; val opt_context = Context.thread_data (); diff -r 71eab6907eee -r 600f432ab556 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Tue Mar 25 13:18:10 2014 +0100 @@ -21,12 +21,12 @@ val trace: bool Config.T val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T -> Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option - val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit - val eval_file: bool -> Path.T -> unit - val eval_source: bool -> Symbol_Pos.source -> unit - val eval_in: Proof.context option -> bool -> Position.T -> + val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit + val eval_file: ML_Compiler.flags -> Path.T -> unit + val eval_source: ML_Compiler.flags -> Symbol_Pos.source -> unit + val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit - val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> unit + val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic end @@ -140,8 +140,10 @@ val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false); val trace = Config.bool trace_raw; -fun eval verbose pos ants = +fun eval flags pos ants = let + val non_verbose = {SML = #SML flags, verbose = false}; + (*prepare source text*) val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ()); val _ = @@ -157,11 +159,11 @@ val _ = Context.setmp_thread_data (Option.map (Context.mapping I (Context_Position.set_visible false)) env_ctxt) - (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) () + (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) () |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context')); - val _ = ML_Compiler.eval verbose pos body; - val _ = ML_Compiler.eval false Position.none reset_env; + val _ = ML_Compiler.eval flags pos body; + val _ = ML_Compiler.eval non_verbose Position.none reset_env; in () end; end; @@ -169,29 +171,29 @@ (* derived versions *) -fun eval_file verbose path = +fun eval_file flags path = let val pos = Path.position path - in eval verbose pos (ML_Lex.read pos (File.read path)) end; + in eval flags pos (ML_Lex.read pos (File.read path)) end; -fun eval_source verbose source = - eval verbose (#pos source) (ML_Lex.read_source source); +fun eval_source flags source = + eval flags (#pos source) (ML_Lex.read_source source); -fun eval_in ctxt verbose pos ants = +fun eval_in ctxt flags pos ants = Context.setmp_thread_data (Option.map Context.Proof ctxt) - (fn () => eval verbose pos ants) (); + (fn () => eval flags pos ants) (); -fun eval_source_in ctxt verbose source = +fun eval_source_in ctxt flags source = Context.setmp_thread_data (Option.map Context.Proof ctxt) - (fn () => eval_source verbose source) (); + (fn () => eval_source flags source) (); fun expression pos bind body ants = - exec (fn () => eval false pos + exec (fn () => eval {SML = false, verbose = false} pos (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @ ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));"))); end; fun use s = - ML_Context.eval_file true (Path.explode s) + ML_Context.eval_file {SML = false, verbose = true} (Path.explode s) handle ERROR msg => (writeln msg; error "ML error"); diff -r 71eab6907eee -r 600f432ab556 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/ML/ml_env.ML Tue Mar 25 13:18:10 2014 +0100 @@ -1,12 +1,14 @@ (* Title: Pure/ML/ml_env.ML Author: Makarius -Local environment of ML results. +Toplevel environment for Standard ML and Isabelle/ML within the +implicit context. *) signature ML_ENV = sig val inherit: Context.generic -> Context.generic -> Context.generic + val SML_name_space: ML_Name_Space.T val name_space: ML_Name_Space.T val local_context: use_context val check_functor: string -> unit @@ -17,56 +19,112 @@ (* context data *) +type tables = + ML_Name_Space.valueVal Symtab.table * + ML_Name_Space.typeVal Symtab.table * + ML_Name_Space.fixityVal Symtab.table * + ML_Name_Space.structureVal Symtab.table * + ML_Name_Space.signatureVal Symtab.table * + ML_Name_Space.functorVal Symtab.table; + +fun merge_tables + ((val1, type1, fixity1, structure1, signature1, functor1), + (val2, type2, fixity2, structure2, signature2, functor2)) : tables = + (Symtab.merge (K true) (val1, val2), + Symtab.merge (K true) (type1, type2), + Symtab.merge (K true) (fixity1, fixity2), + Symtab.merge (K true) (structure1, structure2), + Symtab.merge (K true) (signature1, signature2), + Symtab.merge (K true) (functor1, functor2)); + +type data = {bootstrap: bool, tables: tables, sml_tables: tables}; + +fun make_data (bootstrap, tables, sml_tables) : data = + {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables}; + structure Env = Generic_Data ( - type T = - bool * (*global bootstrap environment*) - (ML_Name_Space.valueVal Symtab.table * - ML_Name_Space.typeVal Symtab.table * - ML_Name_Space.fixityVal Symtab.table * - ML_Name_Space.structureVal Symtab.table * - ML_Name_Space.signatureVal Symtab.table * - ML_Name_Space.functorVal Symtab.table); - val empty : T = - (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty)); - fun extend (_, tabs) : T = (false, tabs); - fun merge - ((_, (val1, type1, fixity1, structure1, signature1, functor1)), - (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T = - (false, - (Symtab.merge (K true) (val1, val2), - Symtab.merge (K true) (type1, type2), - Symtab.merge (K true) (fixity1, fixity2), - Symtab.merge (K true) (structure1, structure2), - Symtab.merge (K true) (signature1, signature2), - Symtab.merge (K true) (functor1, functor2))); + type T = data + val empty = + make_data (true, + (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty), + (Symtab.make ML_Name_Space.initial_val, + Symtab.make ML_Name_Space.initial_type, + Symtab.make ML_Name_Space.initial_fixity, + Symtab.make ML_Name_Space.initial_structure, + Symtab.make ML_Name_Space.initial_signature, + Symtab.make ML_Name_Space.initial_functor)); + fun extend (data : T) = make_data (false, #tables data, #sml_tables data); + fun merge (data : T * T) = + make_data (false, + merge_tables (pairself #tables data), + merge_tables (pairself #sml_tables data)); ); val inherit = Env.put o Env.get; -(* results *) +(* SML name space *) + +val SML_name_space: ML_Name_Space.T = + let + fun lookup which name = + Context.the_thread_data () + |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name); + + fun all which () = + Context.the_thread_data () + |> (fn context => Symtab.dest (which (#sml_tables (Env.get context)))) + |> sort_distinct (string_ord o pairself #1); + + fun enter which entry = + Context.>> (Env.map (fn {bootstrap, tables, sml_tables} => + let val sml_tables' = which (Symtab.update entry) sml_tables + in make_data (bootstrap, tables, sml_tables') end)); + in + {lookupVal = lookup #1, + lookupType = lookup #2, + lookupFix = lookup #3, + lookupStruct = lookup #4, + lookupSig = lookup #5, + lookupFunct = lookup #6, + enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)), + enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)), + enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)), + enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)), + enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)), + enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)), + allVal = all #1, + allType = all #2, + allFix = all #3, + allStruct = all #4, + allSig = all #5, + allFunct = all #6} + end; + + +(* Isabelle/ML name space *) val name_space: ML_Name_Space.T = let fun lookup sel1 sel2 name = Context.thread_data () - |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name) + |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name) |> (fn NONE => sel2 ML_Name_Space.global name | some => some); fun all sel1 sel2 () = Context.thread_data () - |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context)))) + |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context)))) |> append (sel2 ML_Name_Space.global ()) |> sort_distinct (string_ord o pairself #1); fun enter ap1 sel2 entry = if is_some (Context.thread_data ()) then - Context.>> (Env.map (fn (global, tabs) => + Context.>> (Env.map (fn {bootstrap, tables, sml_tables} => let - val _ = if global then sel2 ML_Name_Space.global entry else (); - val tabs' = ap1 (Symtab.update entry) tabs; - in (global, tabs') end)) + val _ = if bootstrap then sel2 ML_Name_Space.global entry else (); + val tables' = ap1 (Symtab.update entry) tables; + in make_data (bootstrap, tables', sml_tables) end)) else sel2 ML_Name_Space.global entry; in {lookupVal = lookup #1 #lookupVal, diff -r 71eab6907eee -r 600f432ab556 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/ML/ml_thms.ML Tue Mar 25 13:18:10 2014 +0100 @@ -130,7 +130,7 @@ else if not (ML_Syntax.is_identifier name) then error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") else - ML_Compiler.eval true Position.none + ML_Compiler.eval {SML = false, verbose = true} Position.none (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); val _ = Theory.setup (Stored_Thms.put []); in () end; diff -r 71eab6907eee -r 600f432ab556 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/Pure.thy Tue Mar 25 13:18:10 2014 +0100 @@ -14,7 +14,7 @@ "infixr" "is" "keywords" "notes" "obtains" "open" "output" "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|" and "theory" :: thy_begin % "theory" - and "ML_file" :: thy_load % "ML" + and "SML_file" "ML_file" :: thy_load % "ML" and "header" :: diag and "chapter" :: thy_heading1 and "section" :: thy_heading2 diff -r 71eab6907eee -r 600f432ab556 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Mar 25 13:18:10 2014 +0100 @@ -639,7 +639,7 @@ fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position) (fn {context, ...} => fn source => - (ML_Context.eval_in (SOME context) false (#pos source) (ml source); + (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source); Symbol_Pos.source_content source |> #1 |> (if Config.get context quotes then quote else I) diff -r 71eab6907eee -r 600f432ab556 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Tue Mar 25 10:37:10 2014 +0100 +++ b/src/Pure/pure_syn.ML Tue Mar 25 13:18:10 2014 +0100 @@ -25,7 +25,7 @@ val source = {delimited = true, text = cat_lines lines, pos = pos}; in gthy - |> ML_Context.exec (fn () => ML_Context.eval_source true source) + |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) |> Local_Theory.propagate_ml_env |> Context.mapping provide (Local_Theory.background_theory provide) end)));