# HG changeset patch
# User wenzelm
# Date 1275248059 -7200
# Node ID 3af985b1055084bfa68aa7a7a7fb2dd4b874145c
# Parent  953fc49834390456811dcd65e2a4fb9126b42d1d
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;

diff -r 953fc4983439 -r 3af985b10550 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sun May 30 18:23:50 2010 +0200
+++ b/doc-src/antiquote_setup.ML	Sun May 30 21:34:19 2010 +0200
@@ -66,7 +66,7 @@
         else if kind = "exception" then txt1 ^ " of " ^ txt2
         else txt1 ^ ": " ^ txt2;
       val txt' = if kind = "" then txt else kind ^ " " ^ txt;
-      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
+      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)
       val kind' = if kind = "" then "ML" else "ML " ^ kind;
     in
       "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
diff -r 953fc4983439 -r 3af985b10550 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Sun May 30 21:34:19 2010 +0200
@@ -836,7 +836,7 @@
             [str "]"]), Pretty.brk 1,
           str "| NONE => NONE);"]) ^
       "\n\nend;\n";
-    val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
+    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
     val values = Config.get ctxt random_values;
     val bound = Config.get ctxt depth_bound;
     val start = Config.get ctxt depth_start;
diff -r 953fc4983439 -r 3af985b10550 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun May 30 21:34:19 2010 +0200
@@ -153,7 +153,9 @@
   Context.theory_map (ML_Context.expression pos
     "val (name, scan, comment): binding * attribute context_parser * string"
     "Context.map_theory (Attrib.setup name scan comment)"
-    ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
+    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
+      ML_Lex.read pos txt @
+      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
 
 
 (* add/del syntax *)
diff -r 953fc4983439 -r 3af985b10550 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun May 30 21:34:19 2010 +0200
@@ -94,11 +94,13 @@
 (* generic setup *)
 
 fun global_setup (txt, pos) =
-  ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup" txt
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup"
   |> Context.theory_map;
 
 fun local_setup (txt, pos) =
-  ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup" txt
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup"
   |> Context.proof_map;
 
 
@@ -115,35 +117,40 @@
 in
 
 fun parse_ast_translation (a, (txt, pos)) =
-  txt |> ML_Context.expression pos
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos
     ("val parse_ast_translation: (string * (" ^ advancedT a ^
       "Syntax.ast list -> Syntax.ast)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
   |> Context.theory_map;
 
 fun parse_translation (a, (txt, pos)) =
-  txt |> ML_Context.expression pos
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos
     ("val parse_translation: (string * (" ^ advancedT a ^
       "term list -> term)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
   |> Context.theory_map;
 
 fun print_translation (a, (txt, pos)) =
-  txt |> ML_Context.expression pos
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos
     ("val print_translation: (string * (" ^ advancedT a ^
       "term list -> term)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
   |> Context.theory_map;
 
 fun print_ast_translation (a, (txt, pos)) =
-  txt |> ML_Context.expression pos
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos
     ("val print_ast_translation: (string * (" ^ advancedT a ^
       "Syntax.ast list -> Syntax.ast)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
   |> Context.theory_map;
 
 fun typed_print_translation (a, (txt, pos)) =
-  txt |> ML_Context.expression pos
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos
     ("val typed_print_translation: (string * (" ^ advancedT a ^
       "bool -> typ -> term list -> term)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
@@ -156,15 +163,16 @@
 
 fun oracle (name, pos) (body_txt, body_pos) =
   let
-    val body = Symbol_Pos.content (Symbol_Pos.explode (body_txt, body_pos));
-    val txt =
-      "local\n\
-      \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
-      \  val body = " ^ body ^ ";\n\
-      \in\n\
-      \  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 body_pos txt)) end;
+    val body = ML_Lex.read body_pos body_txt;
+    val ants =
+      ML_Lex.read Position.none
+       ("local\n\
+        \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
+        \  val body = ") @ body @ ML_Lex.read Position.none (";\n\
+        \in\n\
+        \  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 body_pos ants)) end;
 
 
 (* old-style axioms *)
@@ -180,7 +188,8 @@
 (* declarations *)
 
 fun declaration pervasive (txt, pos) =
-  txt |> ML_Context.expression pos
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos
     "val declaration: Morphism.declaration"
     ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)")
   |> Context.proof_map;
@@ -188,12 +197,13 @@
 
 (* simprocs *)
 
-fun simproc_setup name lhss (proc, pos) identifier =
-  ML_Context.expression pos
+fun simproc_setup name lhss (txt, pos) identifier =
+  ML_Lex.read pos txt
+  |> ML_Context.expression pos
     "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
-  ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
-    \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
-    \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") proc
+    ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
+      \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
+      \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
   |> Context.proof_map;
 
 
@@ -290,7 +300,7 @@
 (* diagnostic ML evaluation *)
 
 fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
-  (ML_Context.eval_in
+  (ML_Context.eval_text_in
     (Option.map Context.proof_of (try Toplevel.generic_theory_of state)) verbose pos txt));
 
 
diff -r 953fc4983439 -r 3af985b10550 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun May 30 21:34:19 2010 +0200
@@ -321,13 +321,13 @@
     (Keyword.tag_ml Keyword.thy_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> propagate_env)));
 
 val _ =
   Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)));
 
 val _ =
   Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
diff -r 953fc4983439 -r 3af985b10550 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Pure/Isar/method.ML	Sun May 30 21:34:19 2010 +0200
@@ -286,7 +286,7 @@
     val ctxt' = ctxt |> Context.proof_map
       (ML_Context.expression pos
         "fun tactic (facts: thm list) : tactic"
-        "Context.map_proof (Method.set_tactic tactic)" txt);
+        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt));
   in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
 
 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
@@ -376,7 +376,9 @@
   Context.theory_map (ML_Context.expression pos
     "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
     "Context.map_theory (Method.setup name scan comment)"
-    ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
+    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
+      ML_Lex.read pos txt @
+      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
 
 
 
@@ -463,9 +465,9 @@
   setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
     (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
       "rotate assumptions of goal" #>
-  setup (Binding.name "tactic") (Scan.lift (Parse.position Args.name) >> tactic)
+  setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
     "ML tactic as proof method" #>
-  setup (Binding.name "raw_tactic") (Scan.lift (Parse.position Args.name) >> raw_tactic)
+  setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
     "ML tactic as raw proof method"));
 
 
diff -r 953fc4983439 -r 3af985b10550 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Sun May 30 21:34:19 2010 +0200
@@ -27,12 +27,16 @@
   val trace: bool Unsynchronized.ref
   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 -> Symbol_Pos.text -> unit
+  val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
+  val eval_text: bool -> Position.T -> Symbol_Pos.text -> unit
   val eval_file: Path.T -> unit
-  val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
-  val evaluate: Proof.context -> bool ->
-    string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
-  val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
+  val eval_in: Proof.context option -> bool -> Position.T ->
+    ML_Lex.token Antiquote.antiquote list -> unit
+  val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
+  val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
+    Context.generic -> Context.generic
+  val evaluate:
+    Proof.context -> bool -> string * (unit -> 'a) option Unsynchronized.ref -> string -> 'a
 end
 
 structure ML_Context: ML_CONTEXT =
@@ -159,11 +163,9 @@
 
 val trace = Unsynchronized.ref false;
 
-fun eval verbose pos txt =
+fun eval verbose pos ants =
   let
     (*prepare source text*)
-    val _ = Position.report Markup.ML_source pos;
-    val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
     val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
     val _ =
       if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
@@ -183,24 +185,32 @@
 
 (* derived versions *)
 
-fun eval_file path = eval true (Path.position path) (File.read path);
+fun eval_text verbose pos txt = eval verbose pos (ML_Lex.read pos txt);
+fun eval_file path = eval_text true (Path.position path) (File.read path);
+
+fun eval_in ctxt verbose pos ants =
+  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) ();
 
-fun eval_in ctxt verbose pos txt =
-  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
+fun eval_text_in ctxt verbose pos txt =
+  Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_text verbose pos txt) ();
+
+fun expression pos bind body ants =
+  exec (fn () => eval 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 ())));")));
+
 
 (* FIXME not thread-safe -- reference can be accessed directly *)
 fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   let
+    val ants =
+      ML_Lex.read Position.none ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
     val _ = r := NONE;
-    val _ = Context.setmp_thread_data (SOME (Context.Proof ctxt)) (fn () =>
-      eval verbose Position.none ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))")) ();
+    val _ =
+      Context.setmp_thread_data (SOME (Context.Proof ctxt))
+        (fn () => eval verbose Position.none ants) ();
   in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
 
-fun expression pos bind body txt =
-  exec (fn () => eval false pos
-    ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
-      " end (ML_Context.the_generic_context ())));"));
-
 end;
 
 structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
diff -r 953fc4983439 -r 3af985b10550 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML	Sun May 30 21:34:19 2010 +0200
@@ -26,7 +26,7 @@
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
   val tokenize: string -> token list
-  val read_antiq: Symbol_Pos.T list * Position.T -> token Antiquote.antiquote list
+  val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
 end;
 
 structure ML_Lex: ML_LEX =
@@ -263,16 +263,21 @@
   source #>
   Source.exhaust;
 
-fun read_antiq (syms, pos) =
-  (Source.of_list syms
-    |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
-      (SOME (false, fn msg => recover msg >> map Antiquote.Text))
-    |> Source.exhaust
-    |> tap (List.app (Antiquote.report report_token))
-    |> tap Antiquote.check_nesting
-    |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
-  handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
+fun read pos txt =
+  let
+    val _ = Position.report Markup.ML_source pos;
+    val syms = Symbol_Pos.explode (txt, pos);
+  in
+    (Source.of_list syms
+      |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
+        (SOME (false, fn msg => recover msg >> map Antiquote.Text))
+      |> Source.exhaust
+      |> tap (List.app (Antiquote.report report_token))
+      |> tap Antiquote.check_nesting
+      |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
+    handle ERROR msg =>
+      cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos)
+  end;
 
 end;
 
diff -r 953fc4983439 -r 3af985b10550 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun May 30 21:34:19 2010 +0200
@@ -587,7 +587,7 @@
 
 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
   (fn {context, ...} => fn (txt, pos) =>
-   (ML_Context.eval_in (SOME context) false pos (ml txt);
+   (ML_Context.eval_in (SOME context) false pos (ml pos txt);
     Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
     |> (if ! quotes then quote else I)
     |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
@@ -596,13 +596,21 @@
       #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
       #> space_implode "\\isasep\\isanewline%\n")));
 
+fun ml_enclose bg en pos txt =
+  ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
+
 in
 
-val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
-val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
-val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
-val _ = ml_text "ML_functor" (fn txt => "ML_Env.check_functor " ^ ML_Syntax.print_string txt);
-val _ = ml_text "ML_text" (K "");
+val _ = ml_text "ML" (ml_enclose "fn _ => (" ");");
+val _ = ml_text "ML_type" (ml_enclose "val _ = NONE : (" ") option;");
+val _ = ml_text "ML_struct" (ml_enclose "functor XXX() = struct structure XX = " " end;");
+
+val _ = ml_text "ML_functor"   (* FIXME formal treatment of functor name (!?) *)
+  (fn pos => fn txt =>
+    ML_Lex.read Position.none ("ML_Env.check_functor " ^
+      ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos)))));
+
+val _ = ml_text "ML_text" (K (K []));
 
 end;
 
diff -r 953fc4983439 -r 3af985b10550 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Pure/codegen.ML	Sun May 30 21:34:19 2010 +0200
@@ -894,7 +894,7 @@
                   [str "]"])]]),
           str ");"]) ^
       "\n\nend;\n";
-    val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
+    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
     val dummy_report = ([], false)
   in (fn size => (! test_fn size, dummy_report)) end;
 
@@ -926,7 +926,7 @@
               str ");"]) ^
           "\n\nend;\n";
         val _ = NAMED_CRITICAL "codegen" (fn () =>   (* FIXME ??? *)
-          ML_Context.eval_in (SOME ctxt) false Position.none s);
+          ML_Context.eval_text_in (SOME ctxt) false Position.none s);
       in !eval_result end;
   in e () end;
 
@@ -1001,7 +1001,7 @@
       val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs;
       val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
         (case opt_fname of
-          NONE => ML_Context.eval false Position.none (cat_lines (map snd code))
+          NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))
         | SOME fname =>
             if lib then app (fn (name, s) => File.write
                 (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
diff -r 953fc4983439 -r 3af985b10550 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Sun May 30 18:23:50 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Sun May 30 21:34:19 2010 +0200
@@ -165,7 +165,8 @@
       in
         thy
         |> Code_Target.add_reserved target module_name
-        |> Context.theory_map (ML_Context.exec (fn () => ML_Context.eval true Position.none code_body))
+        |> Context.theory_map
+          (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
         |> fold (add_eval_tyco o apsnd pr) tyco_map
         |> fold (add_eval_constr o apsnd pr) constr_map
         |> fold (add_eval_const o apsnd pr) const_map