structure ML_Compiler;
authorwenzelm
Mon Jun 01 23:28:07 2009 +0200 (2009-06-01)
changeset 31334999fa9e1dbdd
parent 31333 fcd010617e6c
child 31335 ba5b7749fa61
structure ML_Compiler;
src/Pure/ML/ml_context.ML
     1.1 --- a/src/Pure/ML/ml_context.ML	Mon Jun 01 23:28:06 2009 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Mon Jun 01 23:28:07 2009 +0200
     1.3 @@ -64,8 +64,8 @@
     1.4        else if not (ML_Syntax.is_identifier name) then
     1.5          error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
     1.6        else setmp stored_thms ths' (fn () =>
     1.7 -        use_text ML_Env.local_context (0, "") true
     1.8 -          ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
     1.9 +        ML_Compiler.eval true Position.none
    1.10 +          (ML_Lex.tokenize ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);"))) ();
    1.11    in () end;
    1.12  
    1.13  val ml_store_thms = ml_store "";
    1.14 @@ -124,6 +124,7 @@
    1.15  val struct_name = "Isabelle";
    1.16  val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n");
    1.17  val end_env = ML_Lex.tokenize "end;";
    1.18 +val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
    1.19  
    1.20  in
    1.21  
    1.22 @@ -165,26 +166,21 @@
    1.23  
    1.24  fun eval verbose pos txt =
    1.25    let
    1.26 -    fun eval_raw p = use_text ML_Env.local_context
    1.27 -      (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p));
    1.28 -
    1.29      (*prepare source text*)
    1.30      val _ = Position.report Markup.ML_source pos;
    1.31      val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
    1.32 -    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ())
    1.33 -      |>> pairself (implode o map ML_Lex.text_of);
    1.34 -    val _ = if ! trace then tracing (cat_lines [env, body]) else ();
    1.35 +    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
    1.36 +    val _ =
    1.37 +      if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
    1.38 +      else ();
    1.39  
    1.40      (*prepare static ML environment*)
    1.41      val _ = Context.setmp_thread_data env_ctxt
    1.42 -        (fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
    1.43 +        (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) ()
    1.44        |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
    1.45  
    1.46 -    (*eval ML*)
    1.47 -    val _ = eval_raw pos verbose body;
    1.48 -
    1.49 -    (*reset static ML environment*)
    1.50 -    val _ = eval_raw Position.none false "structure Isabelle = struct end";
    1.51 +    val _ = ML_Compiler.eval verbose pos body;
    1.52 +    val _ = ML_Compiler.eval false Position.none reset_env;
    1.53    in () end;
    1.54  
    1.55  end;