1.1 --- a/doc-src/antiquote_setup.ML	Sun May 30 18:23:50 2010 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Sun May 30 21:34:19 2010 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4          else if kind = "exception" then txt1 ^ " of " ^ txt2
     1.5          else txt1 ^ ": " ^ txt2;
     1.6        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     1.7 -      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
     1.8 +      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)
     1.9        val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.10      in
    1.11        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^

     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun May 30 18:23:50 2010 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun May 30 21:34:19 2010 +0200
     2.3 @@ -836,7 +836,7 @@
     2.4              [str "]"]), Pretty.brk 1,
     2.5            str "| NONE => NONE);"]) ^
     2.6        "\n\nend;\n";
     2.7 -    val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
     2.8 +    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
     2.9      val values = Config.get ctxt random_values;
    2.10      val bound = Config.get ctxt depth_bound;
    2.11      val start = Config.get ctxt depth_start;

     3.1 --- a/src/Pure/Isar/attrib.ML	Sun May 30 18:23:50 2010 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Sun May 30 21:34:19 2010 +0200
     3.3 @@ -153,7 +153,9 @@
     3.4    Context.theory_map (ML_Context.expression pos
     3.5      "val (name, scan, comment): binding * attribute context_parser * string"
     3.6      "Context.map_theory (Attrib.setup name scan comment)"
     3.7 -    ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
     3.8 +    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
     3.9 +      ML_Lex.read pos txt @
    3.10 +      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    3.11  
    3.12  
    3.13  (* add/del syntax *)

     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun May 30 18:23:50 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun May 30 21:34:19 2010 +0200
     4.3 @@ -94,11 +94,13 @@
     4.4  (* generic setup *)
     4.5  
     4.6  fun global_setup (txt, pos) =
     4.7 -  ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup" txt
     4.8 +  ML_Lex.read pos txt
     4.9 +  |> ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup"
    4.10    |> Context.theory_map;
    4.11  
    4.12  fun local_setup (txt, pos) =
    4.13 -  ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup" txt
    4.14 +  ML_Lex.read pos txt
    4.15 +  |> ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup"
    4.16    |> Context.proof_map;
    4.17  
    4.18  
    4.19 @@ -115,35 +117,40 @@
    4.20  in
    4.21  
    4.22  fun parse_ast_translation (a, (txt, pos)) =
    4.23 -  txt |> ML_Context.expression pos
    4.24 +  ML_Lex.read pos txt
    4.25 +  |> ML_Context.expression pos
    4.26      ("val parse_ast_translation: (string * (" ^ advancedT a ^
    4.27        "Syntax.ast list -> Syntax.ast)) list")
    4.28      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
    4.29    |> Context.theory_map;
    4.30  
    4.31  fun parse_translation (a, (txt, pos)) =
    4.32 -  txt |> ML_Context.expression pos
    4.33 +  ML_Lex.read pos txt
    4.34 +  |> ML_Context.expression pos
    4.35      ("val parse_translation: (string * (" ^ advancedT a ^
    4.36        "term list -> term)) list")
    4.37      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
    4.38    |> Context.theory_map;
    4.39  
    4.40  fun print_translation (a, (txt, pos)) =
    4.41 -  txt |> ML_Context.expression pos
    4.42 +  ML_Lex.read pos txt
    4.43 +  |> ML_Context.expression pos
    4.44      ("val print_translation: (string * (" ^ advancedT a ^
    4.45        "term list -> term)) list")
    4.46      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
    4.47    |> Context.theory_map;
    4.48  
    4.49  fun print_ast_translation (a, (txt, pos)) =
    4.50 -  txt |> ML_Context.expression pos
    4.51 +  ML_Lex.read pos txt
    4.52 +  |> ML_Context.expression pos
    4.53      ("val print_ast_translation: (string * (" ^ advancedT a ^
    4.54        "Syntax.ast list -> Syntax.ast)) list")
    4.55      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
    4.56    |> Context.theory_map;
    4.57  
    4.58  fun typed_print_translation (a, (txt, pos)) =
    4.59 -  txt |> ML_Context.expression pos
    4.60 +  ML_Lex.read pos txt
    4.61 +  |> ML_Context.expression pos
    4.62      ("val typed_print_translation: (string * (" ^ advancedT a ^
    4.63        "bool -> typ -> term list -> term)) list")
    4.64      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
    4.65 @@ -156,15 +163,16 @@
    4.66  
    4.67  fun oracle (name, pos) (body_txt, body_pos) =
    4.68    let
    4.69 -    val body = Symbol_Pos.content (Symbol_Pos.explode (body_txt, body_pos));
    4.70 -    val txt =
    4.71 -      "local\n\
    4.72 -      \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
    4.73 -      \  val body = " ^ body ^ ";\n\
    4.74 -      \in\n\
    4.75 -      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
    4.76 -      \end;\n";
    4.77 -  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos txt)) end;
    4.78 +    val body = ML_Lex.read body_pos body_txt;
    4.79 +    val ants =
    4.80 +      ML_Lex.read Position.none
    4.81 +       ("local\n\
    4.82 +        \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
    4.83 +        \  val body = ") @ body @ ML_Lex.read Position.none (";\n\
    4.84 +        \in\n\
    4.85 +        \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
    4.86 +        \end;\n");
    4.87 +  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end;
    4.88  
    4.89  
    4.90  (* old-style axioms *)
    4.91 @@ -180,7 +188,8 @@
    4.92  (* declarations *)
    4.93  
    4.94  fun declaration pervasive (txt, pos) =
    4.95 -  txt |> ML_Context.expression pos
    4.96 +  ML_Lex.read pos txt
    4.97 +  |> ML_Context.expression pos
    4.98      "val declaration: Morphism.declaration"
    4.99      ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)")
   4.100    |> Context.proof_map;
   4.101 @@ -188,12 +197,13 @@
   4.102  
   4.103  (* simprocs *)
   4.104  
   4.105 -fun simproc_setup name lhss (proc, pos) identifier =
   4.106 -  ML_Context.expression pos
   4.107 +fun simproc_setup name lhss (txt, pos) identifier =
   4.108 +  ML_Lex.read pos txt
   4.109 +  |> ML_Context.expression pos
   4.110      "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
   4.111 -  ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
   4.112 -    \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
   4.113 -    \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") proc
   4.114 +    ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
   4.115 +      \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
   4.116 +      \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
   4.117    |> Context.proof_map;
   4.118  
   4.119  
   4.120 @@ -290,7 +300,7 @@
   4.121  (* diagnostic ML evaluation *)
   4.122  
   4.123  fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
   4.124 -  (ML_Context.eval_in
   4.125 +  (ML_Context.eval_text_in
   4.126      (Option.map Context.proof_of (try Toplevel.generic_theory_of state)) verbose pos txt));
   4.127  
   4.128  

     5.1 --- a/src/Pure/Isar/isar_syn.ML	Sun May 30 18:23:50 2010 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun May 30 21:34:19 2010 +0200
     5.3 @@ -321,13 +321,13 @@
     5.4      (Keyword.tag_ml Keyword.thy_decl)
     5.5      (Parse.ML_source >> (fn (txt, pos) =>
     5.6        Toplevel.generic_theory
     5.7 -        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
     5.8 +        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> propagate_env)));
     5.9  
    5.10  val _ =
    5.11    Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
    5.12      (Parse.ML_source >> (fn (txt, pos) =>
    5.13        Toplevel.proof (Proof.map_context (Context.proof_map
    5.14 -        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
    5.15 +        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)));
    5.16  
    5.17  val _ =
    5.18    Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)

     6.1 --- a/src/Pure/Isar/method.ML	Sun May 30 18:23:50 2010 +0200
     6.2 +++ b/src/Pure/Isar/method.ML	Sun May 30 21:34:19 2010 +0200
     6.3 @@ -286,7 +286,7 @@
     6.4      val ctxt' = ctxt |> Context.proof_map
     6.5        (ML_Context.expression pos
     6.6          "fun tactic (facts: thm list) : tactic"
     6.7 -        "Context.map_proof (Method.set_tactic tactic)" txt);
     6.8 +        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt));
     6.9    in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
    6.10  
    6.11  fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
    6.12 @@ -376,7 +376,9 @@
    6.13    Context.theory_map (ML_Context.expression pos
    6.14      "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
    6.15      "Context.map_theory (Method.setup name scan comment)"
    6.16 -    ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
    6.17 +    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
    6.18 +      ML_Lex.read pos txt @
    6.19 +      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    6.20  
    6.21  
    6.22  
    6.23 @@ -463,9 +465,9 @@
    6.24    setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
    6.25      (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
    6.26        "rotate assumptions of goal" #>
    6.27 -  setup (Binding.name "tactic") (Scan.lift (Parse.position Args.name) >> tactic)
    6.28 +  setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
    6.29      "ML tactic as proof method" #>
    6.30 -  setup (Binding.name "raw_tactic") (Scan.lift (Parse.position Args.name) >> raw_tactic)
    6.31 +  setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
    6.32      "ML tactic as raw proof method"));
    6.33  
    6.34  

     7.1 --- a/src/Pure/ML/ml_context.ML	Sun May 30 18:23:50 2010 +0200
     7.2 +++ b/src/Pure/ML/ml_context.ML	Sun May 30 21:34:19 2010 +0200
     7.3 @@ -27,12 +27,16 @@
     7.4    val trace: bool Unsynchronized.ref
     7.5    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     7.6      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
     7.7 -  val eval: bool -> Position.T -> Symbol_Pos.text -> unit
     7.8 +  val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
     7.9 +  val eval_text: bool -> Position.T -> Symbol_Pos.text -> unit
    7.10    val eval_file: Path.T -> unit
    7.11 -  val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
    7.12 -  val evaluate: Proof.context -> bool ->
    7.13 -    string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
    7.14 -  val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
    7.15 +  val eval_in: Proof.context option -> bool -> Position.T ->
    7.16 +    ML_Lex.token Antiquote.antiquote list -> unit
    7.17 +  val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
    7.18 +  val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
    7.19 +    Context.generic -> Context.generic
    7.20 +  val evaluate:
    7.21 +    Proof.context -> bool -> string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
    7.22  end
    7.23  
    7.24  structure ML_Context: ML_CONTEXT =
    7.25 @@ -159,11 +163,9 @@
    7.26  
    7.27  val trace = Unsynchronized.ref false;
    7.28  
    7.29 -fun eval verbose pos txt =
    7.30 +fun eval verbose pos ants =
    7.31    let
    7.32      (*prepare source text*)
    7.33 -    val _ = Position.report Markup.ML_source pos;
    7.34 -    val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
    7.35      val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
    7.36      val _ =
    7.37        if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
    7.38 @@ -183,24 +185,32 @@
    7.39  
    7.40  (* derived versions *)
    7.41  
    7.42 -fun eval_file path = eval true (Path.position path) (File.read path);
    7.43 +fun eval_text verbose pos txt = eval verbose pos (ML_Lex.read pos txt);
    7.44 +fun eval_file path = eval_text true (Path.position path) (File.read path);
    7.45  
    7.46 -fun eval_in ctxt verbose pos txt =
    7.47 -  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
    7.48 +fun eval_in ctxt verbose pos ants =
    7.49 +  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) ();
    7.50 +
    7.51 +fun eval_text_in ctxt verbose pos txt =
    7.52 +  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_text verbose pos txt) ();
    7.53 +
    7.54 +fun expression pos bind body ants =
    7.55 +  exec (fn () => eval false pos
    7.56 +    (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
    7.57 +      ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
    7.58 +
    7.59  
    7.60  (* FIXME not thread-safe -- reference can be accessed directly *)
    7.61  fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
    7.62    let
    7.63 +    val ants =
    7.64 +      ML_Lex.read Position.none ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
    7.65      val _ = r := NONE;
    7.66 -    val _ = Context.setmp_thread_data (SOME (Context.Proof ctxt)) (fn () =>
    7.67 -      eval verbose Position.none ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))")) ();
    7.68 +    val _ =
    7.69 +      Context.setmp_thread_data (SOME (Context.Proof ctxt))
    7.70 +        (fn () => eval verbose Position.none ants) ();
    7.71    in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
    7.72  
    7.73 -fun expression pos bind body txt =
    7.74 -  exec (fn () => eval false pos
    7.75 -    ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
    7.76 -      " end (ML_Context.the_generic_context ())));"));
    7.77 -
    7.78  end;
    7.79  
    7.80  structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;

     8.1 --- a/src/Pure/ML/ml_lex.ML	Sun May 30 18:23:50 2010 +0200
     8.2 +++ b/src/Pure/ML/ml_lex.ML	Sun May 30 21:34:19 2010 +0200
     8.3 @@ -26,7 +26,7 @@
     8.4      (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
     8.5        Source.source) Source.source
     8.6    val tokenize: string -> token list
     8.7 -  val read_antiq: Symbol_Pos.T list * Position.T -> token Antiquote.antiquote list
     8.8 +  val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
     8.9  end;
    8.10  
    8.11  structure ML_Lex: ML_LEX =
    8.12 @@ -263,16 +263,21 @@
    8.13    source #>
    8.14    Source.exhaust;
    8.15  
    8.16 -fun read_antiq (syms, pos) =
    8.17 -  (Source.of_list syms
    8.18 -    |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
    8.19 -      (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    8.20 -    |> Source.exhaust
    8.21 -    |> tap (List.app (Antiquote.report report_token))
    8.22 -    |> tap Antiquote.check_nesting
    8.23 -    |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
    8.24 -  handle ERROR msg =>
    8.25 -    cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
    8.26 +fun read pos txt =
    8.27 +  let
    8.28 +    val _ = Position.report Markup.ML_source pos;
    8.29 +    val syms = Symbol_Pos.explode (txt, pos);
    8.30 +  in
    8.31 +    (Source.of_list syms
    8.32 +      |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
    8.33 +        (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    8.34 +      |> Source.exhaust
    8.35 +      |> tap (List.app (Antiquote.report report_token))
    8.36 +      |> tap Antiquote.check_nesting
    8.37 +      |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
    8.38 +    handle ERROR msg =>
    8.39 +      cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos)
    8.40 +  end;
    8.41  
    8.42  end;
    8.43  

     9.1 --- a/src/Pure/Thy/thy_output.ML	Sun May 30 18:23:50 2010 +0200
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Sun May 30 21:34:19 2010 +0200
     9.3 @@ -587,7 +587,7 @@
     9.4  
     9.5  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
     9.6    (fn {context, ...} => fn (txt, pos) =>
     9.7 -   (ML_Context.eval_in (SOME context) false pos (ml txt);
     9.8 +   (ML_Context.eval_in (SOME context) false pos (ml pos txt);
     9.9      Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
    9.10      |> (if ! quotes then quote else I)
    9.11      |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    9.12 @@ -596,13 +596,21 @@
    9.13        #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
    9.14        #> space_implode "\\isasep\\isanewline%\n")));
    9.15  
    9.16 +fun ml_enclose bg en pos txt =
    9.17 +  ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
    9.18 +
    9.19  in
    9.20  
    9.21 -val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
    9.22 -val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
    9.23 -val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
    9.24 -val _ = ml_text "ML_functor" (fn txt => "ML_Env.check_functor " ^ ML_Syntax.print_string txt);
    9.25 -val _ = ml_text "ML_text" (K "");
    9.26 +val _ = ml_text "ML" (ml_enclose "fn _ => (" ");");
    9.27 +val _ = ml_text "ML_type" (ml_enclose "val _ = NONE : (" ") option;");
    9.28 +val _ = ml_text "ML_struct" (ml_enclose "functor XXX() = struct structure XX = " " end;");
    9.29 +
    9.30 +val _ = ml_text "ML_functor"   (* FIXME formal treatment of functor name (!?) *)
    9.31 +  (fn pos => fn txt =>
    9.32 +    ML_Lex.read Position.none ("ML_Env.check_functor " ^
    9.33 +      ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos)))));
    9.34 +
    9.35 +val _ = ml_text "ML_text" (K (K []));
    9.36  
    9.37  end;
    9.38  

    10.1 --- a/src/Pure/codegen.ML	Sun May 30 18:23:50 2010 +0200
    10.2 +++ b/src/Pure/codegen.ML	Sun May 30 21:34:19 2010 +0200
    10.3 @@ -894,7 +894,7 @@
    10.4                    [str "]"])]]),
    10.5            str ");"]) ^
    10.6        "\n\nend;\n";
    10.7 -    val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
    10.8 +    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
    10.9      val dummy_report = ([], false)
   10.10    in (fn size => (! test_fn size, dummy_report)) end;
   10.11  
   10.12 @@ -926,7 +926,7 @@
   10.13                str ");"]) ^
   10.14            "\n\nend;\n";
   10.15          val _ = NAMED_CRITICAL "codegen" (fn () =>   (* FIXME ??? *)
   10.16 -          ML_Context.eval_in (SOME ctxt) false Position.none s);
   10.17 +          ML_Context.eval_text_in (SOME ctxt) false Position.none s);
   10.18        in !eval_result end;
   10.19    in e () end;
   10.20  
   10.21 @@ -1001,7 +1001,7 @@
   10.22        val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs;
   10.23        val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
   10.24          (case opt_fname of
   10.25 -          NONE => ML_Context.eval false Position.none (cat_lines (map snd code))
   10.26 +          NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))
   10.27          | SOME fname =>
   10.28              if lib then app (fn (name, s) => File.write
   10.29                  (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)

    11.1 --- a/src/Tools/Code/code_eval.ML	Sun May 30 18:23:50 2010 +0200
    11.2 +++ b/src/Tools/Code/code_eval.ML	Sun May 30 21:34:19 2010 +0200
    11.3 @@ -165,7 +165,8 @@
    11.4        in
    11.5          thy
    11.6          |> Code_Target.add_reserved target module_name
    11.7 -        |> Context.theory_map (ML_Context.exec (fn () => ML_Context.eval true Position.none code_body))
    11.8 +        |> Context.theory_map
    11.9 +          (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
   11.10          |> fold (add_eval_tyco o apsnd pr) tyco_map
   11.11          |> fold (add_eval_constr o apsnd pr) constr_map
   11.12          |> fold (add_eval_const o apsnd pr) const_map