# HG changeset patch
# User wenzelm
# Date 1206398064 -3600
# Node ID ae7564661e766f9ec84a5bb81ca55bac4dd92078
# Parent  0aed2ba71388299943a4d4fed921c1b8ee36a303
ML runtime compilation: pass position, tuned signature;

diff -r 0aed2ba71388 -r ae7564661e76 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/doc-src/antiquote_setup.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -36,7 +36,7 @@
       else txt1 ^ ": " ^ txt2;
     val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     val _ = writeln (ml (txt1, txt2));
-    val _ = ML_Context.use_mltext (ml (txt1, txt2)) false (SOME (Context.Proof ctxt));
+    val _ = ML_Context.use_mltext false Position.none (ml (txt1, txt2)) (SOME (Context.Proof ctxt));
   in
     "\\indexml" ^ kind ^ enclose "{" "}"
       (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/General/secure.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -10,7 +10,7 @@
   val set_secure: unit -> unit
   val is_secure: unit -> bool
   val deny_secure: string -> unit
-  val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
+  val use_text: int * string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit
   val commit: unit -> unit
@@ -41,8 +41,8 @@
 fun orig_use_text x = use_text ML_Parse.fix_ints x;
 fun orig_use_file x = use_file ML_Parse.fix_ints x;
 
-fun use_text name pr verbose txt =
-  (secure_mltext (); orig_use_text name pr verbose txt);
+fun use_text pos pr verbose txt =
+  (secure_mltext (); orig_use_text pos pr verbose txt);
 
 fun use_file pr verbose name =
   (secure_mltext (); orig_use_file pr verbose name);
@@ -50,7 +50,7 @@
 fun use name = use_file Output.ml_output true name;
 
 (*commit is dynamically bound!*)
-fun commit () = orig_use_text "" Output.ml_output false "commit();";
+fun commit () = orig_use_text (0, "") Output.ml_output false "commit();";
 
 
 (* shell commands *)
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -7,20 +7,21 @@
 
 signature ISAR_CMD =
 sig
-  val generic_setup: string option -> theory -> theory
-  val parse_ast_translation: bool * string -> theory -> theory
-  val parse_translation: bool * string -> theory -> theory
-  val print_translation: bool * string -> theory -> theory
-  val typed_print_translation: bool * string -> theory -> theory
-  val print_ast_translation: bool * string -> theory -> theory
-  val token_translation: string -> theory -> theory
-  val oracle: bstring -> string -> string -> theory -> theory
+  val generic_setup: (string * Position.T) option -> theory -> theory
+  val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
+  val parse_translation: bool * (string * Position.T) -> theory -> theory
+  val print_translation: bool * (string * Position.T) -> theory -> theory
+  val typed_print_translation: bool * (string * Position.T) -> theory -> theory
+  val print_ast_translation: bool * (string * Position.T) -> theory -> theory
+  val token_translation: string * Position.T -> theory -> theory
+  val oracle: bstring -> string -> string * Position.T -> theory -> theory
   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
   val apply_theorems: (Facts.ref * Attrib.src list) list -> theory -> thm list * theory
   val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
-  val declaration: string -> local_theory -> local_theory
-  val simproc_setup: string -> string list -> string -> string list -> local_theory -> local_theory
+  val declaration: string * Position.T -> local_theory -> local_theory
+  val simproc_setup: string -> string list -> string * Position.T -> string list ->
+    local_theory -> local_theory
   val have: ((string * Attrib.src list) * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
   val hence: ((string * Attrib.src list) * (string * string list) list) list ->
@@ -62,8 +63,8 @@
   val kill: Toplevel.transition -> Toplevel.transition
   val back: Toplevel.transition -> Toplevel.transition
   val use: Path.T -> Toplevel.transition -> Toplevel.transition
-  val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
-  val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
+  val use_mltext_theory: string * Position.T -> Toplevel.transition -> Toplevel.transition
+  val use_mltext: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
   val use_commit: Toplevel.transition -> Toplevel.transition
   val nested_command: Markup.property list -> string * Position.T -> Toplevel.transition
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
@@ -135,8 +136,8 @@
 (* generic_setup *)
 
 fun generic_setup NONE = (fn thy => thy |> Context.setup ())
-  | generic_setup (SOME txt) =
-      ML_Context.use_let "val setup: theory -> theory" "Context.map_theory setup" txt
+  | generic_setup (SOME (txt, pos)) =
+      ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
       |> Context.theory_map;
 
 
@@ -152,50 +153,51 @@
 
 in
 
-fun parse_ast_translation (a, txt) =
-  txt |> ML_Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^
+fun parse_ast_translation (a, (txt, pos)) =
+  txt |> ML_Context.use_let 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) =
-  txt |> ML_Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^
+fun parse_translation (a, (txt, pos)) =
+  txt |> ML_Context.use_let 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) =
-  txt |> ML_Context.use_let ("val print_translation: (string * (" ^ advancedT a ^
+fun print_translation (a, (txt, pos)) =
+  txt |> ML_Context.use_let 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) =
-  txt |> ML_Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^
+fun print_ast_translation (a, (txt, pos)) =
+  txt |> ML_Context.use_let 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) =
-  txt |> ML_Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^
+fun typed_print_translation (a, (txt, pos)) =
+  txt |> ML_Context.use_let 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)")
   |> Context.theory_map;
 
-val token_translation =
-  ML_Context.use_let "val token_translation: (string * string * (string -> output * int)) list"
-    "Context.map_theory (Sign.add_tokentrfuns token_translation)"
-  #> Context.theory_map;
+fun token_translation (txt, pos) =
+  txt |> ML_Context.use_let pos
+    "val token_translation: (string * string * (string -> output * int)) list"
+      "Context.map_theory (Sign.add_tokentrfuns token_translation)"
+  |> Context.theory_map;
 
 end;
 
 
 (* oracles *)
 
-fun oracle name typ oracle =
+fun oracle name typ (oracle, pos) =
   let val txt =
-    "local\n\
-    \  type T = " ^ typ ^ ";\n\
+    "local\
+    \  type T = " ^ typ ^ ";\
     \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
     \  val name = " ^ quote name ^ ";\n\
     \  exception Arg of T;\n\
@@ -205,7 +207,7 @@
     \in\n\
     \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
     \end;\n";
-  in ML_Context.use_mltext_update txt false end
+  in ML_Context.use_mltext_update false pos txt end
   |> Context.theory_map;
 
 
@@ -232,16 +234,16 @@
 
 (* declarations *)
 
-val declaration =
-  ML_Context.use_let "val declaration: Morphism.declaration"
+fun declaration (txt, pos) =
+  txt |> ML_Context.use_let pos "val declaration: Morphism.declaration"
     "Context.map_proof (LocalTheory.declaration declaration)"
-  #> Context.proof_map;
+  |> Context.proof_map;
 
 
 (* simprocs *)
 
-fun simproc_setup name lhss proc identifier =
-  ML_Context.use_let
+fun simproc_setup name lhss (proc, pos) identifier =
+  ML_Context.use_let 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, \
@@ -382,11 +384,12 @@
   ML_Context.setmp (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
 
 (*passes changes of theory context*)
-val use_mltext_theory = Toplevel.theory' o (Context.theory_map oo ML_Context.use_mltext_update);
+fun use_mltext_theory (txt, pos) =
+  Toplevel.theory' (fn int => Context.theory_map (ML_Context.use_mltext_update int pos txt));
 
 (*ignore result theory context*)
-fun use_mltext verbose txt = Toplevel.keep' (fn int => fn state =>
-  (ML_Context.use_mltext txt (verbose andalso int) (try Toplevel.generic_theory_of state)));
+fun use_mltext verbose (txt, pos) = Toplevel.keep' (fn int => fn state =>
+  (ML_Context.use_mltext (verbose andalso int) pos txt (try Toplevel.generic_theory_of state)));
 
 val use_commit = Toplevel.imperative Secure.commit;
 
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -307,41 +307,41 @@
 
 val _ =
   OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
-    (P.text >> IsarCmd.use_mltext true);
+    (P.position P.text >> IsarCmd.use_mltext true);
 
 val _ =
   OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
-    (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
+    (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
 
 val _ =
   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
-    (P.text >> IsarCmd.use_mltext_theory);
+    (P.position P.text >> IsarCmd.use_mltext_theory);
 
 val _ =
   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
-    (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup));
+    (Scan.option (P.position P.text) >> (Toplevel.theory o IsarCmd.generic_setup));
 
 val _ =
   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
-    (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
-      >> (Toplevel.theory o Method.method_setup));
+    (P.name -- P.!!! (P.$$$ "=" |-- P.position P.text -- P.text)
+    >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
   OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
-    (P.opt_target -- P.text
+    (P.opt_target -- P.position P.text
     >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
 
 val _ =
   OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
     (P.opt_target --
-      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text --
-      Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
+      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
+      P.position P.text -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
     >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
 
 
 (* translation functions *)
 
-val trfun = P.opt_keyword "advanced" -- P.text;
+val trfun = P.opt_keyword "advanced" -- P.position P.text;
 
 val _ =
   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
@@ -371,7 +371,7 @@
 val _ =
   OuterSyntax.command "token_translation" "install token translation functions"
     (K.tag_ml K.thy_decl)
-    (P.text >> (Toplevel.theory o IsarCmd.token_translation));
+    (P.position P.text >> (Toplevel.theory o IsarCmd.token_translation));
 
 
 (* oracles *)
@@ -379,7 +379,7 @@
 val _ =
   OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
     (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
-      -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
+      -- P.position P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
 
 
 (* local theories *)
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/Isar/method.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -52,7 +52,7 @@
   val frule: int -> thm list -> method
   val iprover_tac: Proof.context -> int option -> int -> tactic
   val set_tactic: (Proof.context -> thm list -> tactic) -> unit
-  val tactic: string -> Proof.context -> method
+  val tactic: string * Position.T -> Proof.context -> method
   type src
   datatype text =
     Basic of (Proof.context -> method) * Position.T |
@@ -76,7 +76,7 @@
     -> theory -> theory
   val add_method: bstring * (src -> Proof.context -> method) * string
     -> theory -> theory
-  val method_setup: bstring * string * string -> theory -> theory
+  val method_setup: bstring -> string * Position.T -> string -> theory -> theory
   val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
     -> src -> Proof.context -> 'a * Proof.context
   val simple_args: (Args.T list -> 'a * Args.T list)
@@ -353,10 +353,10 @@
 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
 fun set_tactic f = tactic_ref := f;
 
-fun ml_tactic txt ctxt = NAMED_CRITICAL "ML" (fn () =>
-  (ML_Context.use_mltext
+fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () =>
+  (ML_Context.use_mltext false pos
     ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
-      ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
+      ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt));
     ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
 
 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
@@ -446,8 +446,8 @@
 
 (* method_setup *)
 
-fun method_setup (name, txt, cmt) =
-  ML_Context.use_let
+fun method_setup name (txt, pos) cmt =
+  ML_Context.use_let pos
     "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
     "Context.map_theory (Method.add_method method)"
     ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")
@@ -577,8 +577,8 @@
     "rename parameters of goal"),
   ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
     "rotate assumptions of goal"),
-  ("tactic", simple_args Args.name tactic, "ML tactic as proof method"),
-  ("raw_tactic", simple_args Args.name raw_tactic, "ML tactic as raw proof method")]);
+  ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
+  ("raw_tactic", simple_args (Args.position Args.name) raw_tactic, "ML tactic as raw proof method")]);
 
 
 (* outer parser *)
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/ML-Systems/alice.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -117,9 +117,8 @@
 
 (* ML command execution *)
 
-fun use_text tune name (print, err) verbose txt = (Compiler.eval txt; ());
-
-fun use_file tune output verbose name = use name;
+fun use_text _ _ _ _ txt = (Compiler.eval txt; ());
+fun use_file _ _ _ name = use name;
 
 
 
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -22,24 +22,24 @@
 
 (* improved versions of use_text/file *)
 
-fun use_text (tune: string -> string) name (print, err) verbose txt =
+fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
   let
     val in_buffer = ref (String.explode (tune txt));
     val out_buffer = ref ([]: string list);
     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
 
-    val line_no = ref 1;
-    fun line () = ! line_no;
+    val current_line = ref line;
     fun get () =
       (case ! in_buffer of
         [] => NONE
-      | c :: cs => (in_buffer := cs; if c = #"\n" then line_no := ! line_no + 1 else (); SOME c));
+      | c :: cs =>
+          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
     fun put s = out_buffer := s :: ! out_buffer;
 
     val _ =
       (while not (List.null (! in_buffer)) do
         PolyML.compiler
-          {getChar = get, putString = put, lineNumber = line, fileName = name,
+          {getChar = get, putString = put, lineNumber = fn () => ! current_line, fileName = name,
             nameSpace = PolyML.globalNameSpace} ())
       handle exn => (err (output ()); raise exn);
   in
@@ -50,5 +50,5 @@
   let
     val instream = TextIO.openIn name;
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
-  in use_text tune name output verbose txt end;
+  in use_text tune (1, name) output verbose txt end;
 
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/ML-Systems/polyml_old_compiler4.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -1,10 +1,10 @@
 (*  Title:      Pure/ML-Systems/polyml_old_compiler4.ML
     ID:         $Id$
 
-Runtime compilation -- for old version of PolyML.compiler (version 4.x).
+Runtime compilation -- for old PolyML.compiler (version 4.x).
 *)
 
-fun use_text (tune: string -> string) name (print, err) verbose txt =
+fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
   let
     val in_buffer = ref (explode (tune txt));
     val out_buffer = ref ([]: string list);
@@ -30,5 +30,5 @@
   let
     val instream = TextIO.openIn name;
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
-  in use_text tune name output verbose txt end;
+  in use_text tune (1, name) output verbose txt end;
 
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/ML-Systems/polyml_old_compiler5.ML
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -1,27 +1,26 @@
 (*  Title:      Pure/ML-Systems/polyml_old_compiler5.ML
     ID:         $Id$
 
-Runtime compilation -- for old version of PolyML.compilerEx (version 5.0, 5.1).
+Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
 *)
 
-fun use_text (tune: string -> string) name (print, err) verbose txt =
+fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
   let
     val in_buffer = ref (explode (tune txt));
     val out_buffer = ref ([]: string list);
     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
 
-    val line_no = ref 1;
-    fun line () = ! line_no;
+    val current_line = ref line;
     fun get () =
       (case ! in_buffer of
         [] => ""
-      | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
+      | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
     fun put s = out_buffer := s :: ! out_buffer;
 
     fun exec () =
       (case ! in_buffer of
         [] => ()
-      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
+      | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
   in
     exec () handle exn => (err (output ()); raise exn);
     if verbose then print (output ()) else ()
@@ -31,5 +30,5 @@
   let
     val instream = TextIO.openIn name;
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
-  in use_text tune name output verbose txt end;
+  in use_text tune (1, name) output verbose txt end;
 
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -110,7 +110,7 @@
 
 (* ML command execution *)
 
-fun use_text (tune: string -> string) name (print, err) verbose txt =
+fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
   let
     val ref out_orig = Control.Print.out;
 
@@ -132,7 +132,7 @@
   let
     val instream = TextIO.openIn name;
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
-  in use_text tune name output verbose txt end;
+  in use_text tune (1, name) output verbose txt end;
 
 
 
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -31,11 +31,11 @@
     (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit
   val proj_value_antiq: string -> (Context.generic * Args.T list ->
       (string * string * string) * (Context.generic * Args.T list)) -> unit
-  val eval_antiquotes_fn: (string -> string * string) ref  (* FIXME tmp *)
+  val eval_antiquotes_fn: (string * Position.T -> string * string) ref  (* FIXME tmp *)
   val trace: bool ref
-  val use_mltext: string -> bool -> Context.generic option -> unit
-  val use_mltext_update: string -> bool -> Context.generic -> Context.generic
-  val use_let: string -> string -> string -> Context.generic -> Context.generic
+  val use_mltext: bool -> Position.T -> string -> Context.generic option -> unit
+  val use_mltext_update: bool -> Position.T -> string -> Context.generic -> Context.generic
+  val use_let: Position.T -> string -> string -> string -> Context.generic -> Context.generic
   val use: Path.T -> unit
   val evaluate: (string -> unit) * (string -> 'b) -> bool ->
     string * (unit -> 'a) option ref -> string -> 'a
@@ -141,9 +141,9 @@
 val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;";
 val isabelle_struct0 = isabelle_struct "";
 
-fun eval_antiquotes txt =
+fun eval_antiquotes txt_pos =
   let
-    val ants = Antiquote.scan_antiquotes (txt, Position.line 1);
+    val ants = Antiquote.scan_antiquotes txt_pos;
 
     fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names)
       | expand (Antiquote.Antiq x) names =
@@ -170,49 +170,50 @@
 
 val trace = ref false;
 
-fun eval_wrapper name pr verbose txt =
+fun eval_wrapper pr verbose pos txt =
   let
-    val (txt1, txt2) = ! eval_antiquotes_fn txt;  (* FIXME tmp hook *)
+    val (txt1, txt2) = ! eval_antiquotes_fn (txt, pos);  (* FIXME tmp hook *)
     val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
-    fun eval nm = use_text nm pr;
+    fun eval p =
+      use_text (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr;
   in
     NAMED_CRITICAL "ML" (fn () =>
-      (eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0))
+     (eval Position.none false txt1;
+      eval pos verbose txt2;
+      eval Position.none false isabelle_struct0))
   end;
 
-fun ML_wrapper pr = eval_wrapper "ML" pr;
-
 end;
 
 
 (* ML evaluation *)
 
-fun use_mltext txt verbose opt_context =
-  setmp opt_context (fn () => ML_wrapper Output.ml_output verbose txt) ();
+fun use_mltext verbose pos txt opt_context =
+  setmp opt_context (fn () => eval_wrapper Output.ml_output verbose pos txt) ();
 
-fun use_mltext_update txt verbose context =
-  #2 (pass_context context (fn () => ML_wrapper Output.ml_output verbose txt) ());
+fun use_mltext_update verbose pos txt context =
+  #2 (pass_context context (fn () => eval_wrapper Output.ml_output verbose pos txt) ());
 
-fun use_context txt = use_mltext_update
-  ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false;
+fun use_let pos bind body txt =
+  use_mltext_update false pos
+    ("ML_Context.set_context (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
+      " end (ML_Context.the_generic_context ())));");
 
-fun use_let bind body txt =
-  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
-
-fun use path = eval_wrapper (Path.implode path) Output.ml_output true (File.read path);
+fun use path = eval_wrapper Output.ml_output true (Position.path path) (File.read path);
 
 fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   let
     val _ = r := NONE;
-    val _ = ML_wrapper pr verbose ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
+    val _ = eval_wrapper pr verbose Position.none
+      ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
   in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
 
 
 (* basic antiquotations *)
 
-local
+fun context x = (Scan.state >> Context.proof_of) x;
 
-fun context x = (Scan.state >> Context.proof_of) x;
+local
 
 val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()"));
 
@@ -243,7 +244,7 @@
 val _ = inline_antiq "type_name" (type_ false);
 val _ = inline_antiq "type_syntax" (type_ true);
 
-fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
+fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) =>
   #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
   |> syn ? ProofContext.const_syntax_name ctxt
   |> ML_Syntax.print_string);
@@ -252,7 +253,7 @@
 val _ = inline_antiq "const_syntax" (const true);
 
 val _ = inline_antiq "const"
-  ((Scan.state >> Context.proof_of) -- Scan.lift Args.name --
+  (context -- Scan.lift Args.name --
     Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
     >> (fn ((ctxt, c), Ts) =>
       let
@@ -276,8 +277,7 @@
   | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
 
 fun thm_antiq kind get get_name = value_antiq kind
-  ((Scan.state >> Context.proof_of) --
-    Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel)
+  (context -- Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel)
   >> (fn (ctxt, ((name, pos), sel)) =>
       let
         val _ = get ctxt (Facts.Named ((name, pos), sel));
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -501,8 +501,8 @@
 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
 
-fun output_ml ml src ctxt txt =
- (ML_Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt));
+fun output_ml ml src ctxt (txt, pos) =
+ (ML_Context.use_mltext false pos (ml txt) (SOME (Context.Proof ctxt));
   (if ! source then str_of_source src else txt)
   |> (if ! quotes then quote else I)
   |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
@@ -531,8 +531,8 @@
   ("prf", args Attrib.thms (output (pretty_prf false))),
   ("full_prf", args Attrib.thms (output (pretty_prf true))),
   ("theory", args (Scan.lift Args.name) (output pretty_theory)),
-  ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
-  ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
-  ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];
+  ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)),
+  ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)),
+  ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))];
 
 end;
diff -r 0aed2ba71388 -r ae7564661e76 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/codegen.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -963,7 +963,7 @@
                   [Pretty.str "]"])]]),
           Pretty.str ");"]) ^
       "\n\nend;\n") ();
-    val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy));
+    val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
     fun iter f k = if k > i then NONE
       else (case (f () handle Match =>
           (if quiet then ()
@@ -1053,7 +1053,7 @@
               [Pretty.str "(result ())"],
             Pretty.str ");"]) ^
         "\n\nend;\n";
-      val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy))
+      val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
     in !eval_result end) ();
   in e () end;
 
@@ -1148,8 +1148,8 @@
        val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
        val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
      in ((case opt_fname of
-         NONE => ML_Context.use_mltext (space_implode "\n" (map snd code))
-           false (SOME (Context.Theory thy))
+         NONE => ML_Context.use_mltext false Position.none (space_implode "\n" (map snd code))
+           (SOME (Context.Theory thy))
        | SOME fname =>
            if lib then
              app (fn (name, s) => File.write
diff -r 0aed2ba71388 -r ae7564661e76 src/Tools/Compute_Oracle/am_compiler.ML
--- a/src/Tools/Compute_Oracle/am_compiler.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Tools/Compute_Oracle/am_compiler.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -186,7 +186,7 @@
 
     in
 	compiled_rewriter := NONE;	
-	use_text "" Output.ml_output false (!buffer);
+	use_text (1, "") Output.ml_output false (!buffer);
 	case !compiled_rewriter of 
 	    NONE => raise (Compile "cannot communicate with compiled function")
 	  | SOME r => (compiled_rewriter := NONE; r)
diff -r 0aed2ba71388 -r ae7564661e76 src/Tools/Compute_Oracle/am_sml.ML
--- a/src/Tools/Compute_Oracle/am_sml.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -493,7 +493,7 @@
 
 fun writeTextFile name s = File.write (Path.explode name) s
 
-fun use_source src = use_text "" Output.ml_output false src
+fun use_source src = use_text (1, "") Output.ml_output false src
     
 fun compile cache_patterns const_arity eqs = 
     let
diff -r 0aed2ba71388 -r ae7564661e76 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Tools/code/code_target.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -1093,7 +1093,7 @@
 fun isar_seri_sml module file =
   let
     val output = case file
-     of NONE => use_text "generated code" Output.ml_output false o code_output
+     of NONE => use_text (1, "generated code") Output.ml_output false o code_output
       | SOME "-" => PrintMode.setmp [] writeln o code_output
       | SOME file => File.write (Path.explode file) o code_output;
   in