# HG changeset patch # User wenzelm # Date 1395146188 -3600 # Node ID 76c72f4d0667379aee496945fad8cc316ce2a2e9 # Parent 0a11d17eeeffcccaab19eb25e9b1f84bbf8fefbb clarified bootstrap process: switch to ML with context and antiquotations earlier; diff -r 0a11d17eeeff -r 76c72f4d0667 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Tue Mar 18 12:25:17 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Tue Mar 18 13:36:28 2014 +0100 @@ -288,7 +288,7 @@ fun isar in_stream term : isar = Source.tty in_stream |> Symbol.source - |> Source.map_filter (fn "\\<^newline>" => SOME "\n" | s => SOME s) (*Proof General legacy*) + |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s) (*Proof General legacy*) |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none |> toplevel_source term (SOME true) lookup_commands_dynamic; diff -r 0a11d17eeeff -r 76c72f4d0667 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Mar 18 12:25:17 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Tue Mar 18 13:36:28 2014 +0100 @@ -22,6 +22,7 @@ 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 -> ML_Lex.token Antiquote.antiquote list -> unit @@ -174,6 +175,10 @@ (* derived versions *) +fun eval_file verbose path = + let val pos = Path.position path + in eval verbose pos (ML_Lex.read pos (File.read path)) end; + fun eval_source verbose source = eval verbose (#pos source) (ML_Lex.read_source source); diff -r 0a11d17eeeff -r 76c72f4d0667 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Tue Mar 18 12:25:17 2014 +0100 +++ b/src/Pure/ML/ml_env.ML Tue Mar 18 13:36:28 2014 +0100 @@ -20,23 +20,26 @@ structure Env = Generic_Data ( type T = - ML_Name_Space.valueVal Symtab.table * - ML_Name_Space.typeVal Symtab.table * - ML_Name_Space.fixityVal Symtab.table * - ML_Name_Space.structureVal Symtab.table * - ML_Name_Space.signatureVal Symtab.table * - ML_Name_Space.functorVal Symtab.table; - val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty); - val extend = I; + 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 = - (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)); + ((_, (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))); ); val inherit = Env.put o Env.get; @@ -48,18 +51,22 @@ let fun lookup sel1 sel2 name = Context.thread_data () - |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name) + |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (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 (Env.get context))) + |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (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 (ap1 (Symtab.update entry))) + Context.>> (Env.map (fn (global, tabs) => + let + val _ = if global then sel2 ML_Name_Space.global entry else (); + val tabs' = ap1 (Symtab.update entry) tabs; + in (global, tabs') end)) else sel2 ML_Name_Space.global entry; in {lookupVal = lookup #1 #lookupVal, diff -r 0a11d17eeeff -r 76c72f4d0667 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Mar 18 12:25:17 2014 +0100 +++ b/src/Pure/ROOT.ML Tue Mar 18 13:36:28 2014 +0100 @@ -39,7 +39,7 @@ use "ML/ml_lex.ML"; use "ML/ml_parse.ML"; use "General/secure.ML"; -(*^^^^^ end of basic ML bootstrap ^^^^^*) +(*^^^^^ end of ML bootstrap 0 ^^^^^*) use "General/integer.ML"; use "General/stack.ML"; use "General/queue.ML"; @@ -222,7 +222,6 @@ use "Isar/keyword.ML"; use "Isar/parse.ML"; use "Isar/args.ML"; -use "ML/ml_context.ML"; (*theory sources*) use "Thy/thy_header.ML"; @@ -230,6 +229,11 @@ use "Thy/html.ML"; use "Thy/latex.ML"; +(*ML with context and antiquotations*) +use "ML/ml_context.ML"; +val use = ML_Context.eval_file true o Path.explode; +(*^^^^^ end of ML bootstrap 1 ^^^^^*) + (*basic proof engine*) use "Isar/proof_display.ML"; use "Isar/attrib.ML"; diff -r 0a11d17eeeff -r 76c72f4d0667 src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML Tue Mar 18 12:25:17 2014 +0100 +++ b/src/Pure/Thy/term_style.ML Tue Mar 18 13:36:28 2014 +0100 @@ -68,8 +68,8 @@ end); fun sub_symbols (d :: s :: ss) = - if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s) - then d :: "\\<^sub>" :: sub_symbols (s :: ss) + if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\<^") s) + then d :: "\<^sub>" :: sub_symbols (s :: ss) else d :: s :: ss | sub_symbols cs = cs;