1.1 --- a/doc-src/antiquote_setup.ML	Mon Mar 24 18:44:21 2008 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Mar 24 23:34:24 2008 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4        else txt1 ^ ": " ^ txt2;
     1.5      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     1.6      val _ = writeln (ml (txt1, txt2));
     1.7 -    val _ = ML_Context.use_mltext (ml (txt1, txt2)) false (SOME (Context.Proof ctxt));
     1.8 +    val _ = ML_Context.use_mltext false Position.none (ml (txt1, txt2)) (SOME (Context.Proof ctxt));
     1.9    in
    1.10      "\\indexml" ^ kind ^ enclose "{" "}"
    1.11        (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^

     2.1 --- a/src/Pure/General/secure.ML	Mon Mar 24 18:44:21 2008 +0100
     2.2 +++ b/src/Pure/General/secure.ML	Mon Mar 24 23:34:24 2008 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4    val set_secure: unit -> unit
     2.5    val is_secure: unit -> bool
     2.6    val deny_secure: string -> unit
     2.7 -  val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
     2.8 +  val use_text: int * string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
     2.9    val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
    2.10    val use: string -> unit
    2.11    val commit: unit -> unit
    2.12 @@ -41,8 +41,8 @@
    2.13  fun orig_use_text x = use_text ML_Parse.fix_ints x;
    2.14  fun orig_use_file x = use_file ML_Parse.fix_ints x;
    2.15  
    2.16 -fun use_text name pr verbose txt =
    2.17 -  (secure_mltext (); orig_use_text name pr verbose txt);
    2.18 +fun use_text pos pr verbose txt =
    2.19 +  (secure_mltext (); orig_use_text pos pr verbose txt);
    2.20  
    2.21  fun use_file pr verbose name =
    2.22    (secure_mltext (); orig_use_file pr verbose name);
    2.23 @@ -50,7 +50,7 @@
    2.24  fun use name = use_file Output.ml_output true name;
    2.25  
    2.26  (*commit is dynamically bound!*)
    2.27 -fun commit () = orig_use_text "" Output.ml_output false "commit();";
    2.28 +fun commit () = orig_use_text (0, "") Output.ml_output false "commit();";
    2.29  
    2.30  
    2.31  (* shell commands *)

     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 24 18:44:21 2008 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 24 23:34:24 2008 +0100
     3.3 @@ -7,20 +7,21 @@
     3.4  
     3.5  signature ISAR_CMD =
     3.6  sig
     3.7 -  val generic_setup: string option -> theory -> theory
     3.8 -  val parse_ast_translation: bool * string -> theory -> theory
     3.9 -  val parse_translation: bool * string -> theory -> theory
    3.10 -  val print_translation: bool * string -> theory -> theory
    3.11 -  val typed_print_translation: bool * string -> theory -> theory
    3.12 -  val print_ast_translation: bool * string -> theory -> theory
    3.13 -  val token_translation: string -> theory -> theory
    3.14 -  val oracle: bstring -> string -> string -> theory -> theory
    3.15 +  val generic_setup: (string * Position.T) option -> theory -> theory
    3.16 +  val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
    3.17 +  val parse_translation: bool * (string * Position.T) -> theory -> theory
    3.18 +  val print_translation: bool * (string * Position.T) -> theory -> theory
    3.19 +  val typed_print_translation: bool * (string * Position.T) -> theory -> theory
    3.20 +  val print_ast_translation: bool * (string * Position.T) -> theory -> theory
    3.21 +  val token_translation: string * Position.T -> theory -> theory
    3.22 +  val oracle: bstring -> string -> string * Position.T -> theory -> theory
    3.23    val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    3.24    val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    3.25    val apply_theorems: (Facts.ref * Attrib.src list) list -> theory -> thm list * theory
    3.26    val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
    3.27 -  val declaration: string -> local_theory -> local_theory
    3.28 -  val simproc_setup: string -> string list -> string -> string list -> local_theory -> local_theory
    3.29 +  val declaration: string * Position.T -> local_theory -> local_theory
    3.30 +  val simproc_setup: string -> string list -> string * Position.T -> string list ->
    3.31 +    local_theory -> local_theory
    3.32    val have: ((string * Attrib.src list) * (string * string list) list) list ->
    3.33      bool -> Proof.state -> Proof.state
    3.34    val hence: ((string * Attrib.src list) * (string * string list) list) list ->
    3.35 @@ -62,8 +63,8 @@
    3.36    val kill: Toplevel.transition -> Toplevel.transition
    3.37    val back: Toplevel.transition -> Toplevel.transition
    3.38    val use: Path.T -> Toplevel.transition -> Toplevel.transition
    3.39 -  val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    3.40 -  val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
    3.41 +  val use_mltext_theory: string * Position.T -> Toplevel.transition -> Toplevel.transition
    3.42 +  val use_mltext: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
    3.43    val use_commit: Toplevel.transition -> Toplevel.transition
    3.44    val nested_command: Markup.property list -> string * Position.T -> Toplevel.transition
    3.45    val cd: Path.T -> Toplevel.transition -> Toplevel.transition
    3.46 @@ -135,8 +136,8 @@
    3.47  (* generic_setup *)
    3.48  
    3.49  fun generic_setup NONE = (fn thy => thy |> Context.setup ())
    3.50 -  | generic_setup (SOME txt) =
    3.51 -      ML_Context.use_let "val setup: theory -> theory" "Context.map_theory setup" txt
    3.52 +  | generic_setup (SOME (txt, pos)) =
    3.53 +      ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
    3.54        |> Context.theory_map;
    3.55  
    3.56  
    3.57 @@ -152,50 +153,51 @@
    3.58  
    3.59  in
    3.60  
    3.61 -fun parse_ast_translation (a, txt) =
    3.62 -  txt |> ML_Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^
    3.63 +fun parse_ast_translation (a, (txt, pos)) =
    3.64 +  txt |> ML_Context.use_let pos ("val parse_ast_translation: (string * (" ^ advancedT a ^
    3.65        "Syntax.ast list -> Syntax.ast)) list")
    3.66      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
    3.67    |> Context.theory_map;
    3.68  
    3.69 -fun parse_translation (a, txt) =
    3.70 -  txt |> ML_Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^
    3.71 +fun parse_translation (a, (txt, pos)) =
    3.72 +  txt |> ML_Context.use_let pos ("val parse_translation: (string * (" ^ advancedT a ^
    3.73        "term list -> term)) list")
    3.74      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
    3.75    |> Context.theory_map;
    3.76  
    3.77 -fun print_translation (a, txt) =
    3.78 -  txt |> ML_Context.use_let ("val print_translation: (string * (" ^ advancedT a ^
    3.79 +fun print_translation (a, (txt, pos)) =
    3.80 +  txt |> ML_Context.use_let pos ("val print_translation: (string * (" ^ advancedT a ^
    3.81        "term list -> term)) list")
    3.82      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
    3.83    |> Context.theory_map;
    3.84  
    3.85 -fun print_ast_translation (a, txt) =
    3.86 -  txt |> ML_Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^
    3.87 +fun print_ast_translation (a, (txt, pos)) =
    3.88 +  txt |> ML_Context.use_let pos ("val print_ast_translation: (string * (" ^ advancedT a ^
    3.89        "Syntax.ast list -> Syntax.ast)) list")
    3.90      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
    3.91    |> Context.theory_map;
    3.92  
    3.93 -fun typed_print_translation (a, txt) =
    3.94 -  txt |> ML_Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^
    3.95 +fun typed_print_translation (a, (txt, pos)) =
    3.96 +  txt |> ML_Context.use_let pos ("val typed_print_translation: (string * (" ^ advancedT a ^
    3.97        "bool -> typ -> term list -> term)) list")
    3.98      ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
    3.99    |> Context.theory_map;
   3.100  
   3.101 -val token_translation =
   3.102 -  ML_Context.use_let "val token_translation: (string * string * (string -> output * int)) list"
   3.103 -    "Context.map_theory (Sign.add_tokentrfuns token_translation)"
   3.104 -  #> Context.theory_map;
   3.105 +fun token_translation (txt, pos) =
   3.106 +  txt |> ML_Context.use_let pos
   3.107 +    "val token_translation: (string * string * (string -> output * int)) list"
   3.108 +      "Context.map_theory (Sign.add_tokentrfuns token_translation)"
   3.109 +  |> Context.theory_map;
   3.110  
   3.111  end;
   3.112  
   3.113  
   3.114  (* oracles *)
   3.115  
   3.116 -fun oracle name typ oracle =
   3.117 +fun oracle name typ (oracle, pos) =
   3.118    let val txt =
   3.119 -    "local\n\
   3.120 -    \  type T = " ^ typ ^ ";\n\
   3.121 +    "local\
   3.122 +    \  type T = " ^ typ ^ ";\
   3.123      \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
   3.124      \  val name = " ^ quote name ^ ";\n\
   3.125      \  exception Arg of T;\n\
   3.126 @@ -205,7 +207,7 @@
   3.127      \in\n\
   3.128      \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
   3.129      \end;\n";
   3.130 -  in ML_Context.use_mltext_update txt false end
   3.131 +  in ML_Context.use_mltext_update false pos txt end
   3.132    |> Context.theory_map;
   3.133  
   3.134  
   3.135 @@ -232,16 +234,16 @@
   3.136  
   3.137  (* declarations *)
   3.138  
   3.139 -val declaration =
   3.140 -  ML_Context.use_let "val declaration: Morphism.declaration"
   3.141 +fun declaration (txt, pos) =
   3.142 +  txt |> ML_Context.use_let pos "val declaration: Morphism.declaration"
   3.143      "Context.map_proof (LocalTheory.declaration declaration)"
   3.144 -  #> Context.proof_map;
   3.145 +  |> Context.proof_map;
   3.146  
   3.147  
   3.148  (* simprocs *)
   3.149  
   3.150 -fun simproc_setup name lhss proc identifier =
   3.151 -  ML_Context.use_let
   3.152 +fun simproc_setup name lhss (proc, pos) identifier =
   3.153 +  ML_Context.use_let pos
   3.154      "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
   3.155    ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
   3.156      \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
   3.157 @@ -382,11 +384,12 @@
   3.158    ML_Context.setmp (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
   3.159  
   3.160  (*passes changes of theory context*)
   3.161 -val use_mltext_theory = Toplevel.theory' o (Context.theory_map oo ML_Context.use_mltext_update);
   3.162 +fun use_mltext_theory (txt, pos) =
   3.163 +  Toplevel.theory' (fn int => Context.theory_map (ML_Context.use_mltext_update int pos txt));
   3.164  
   3.165  (*ignore result theory context*)
   3.166 -fun use_mltext verbose txt = Toplevel.keep' (fn int => fn state =>
   3.167 -  (ML_Context.use_mltext txt (verbose andalso int) (try Toplevel.generic_theory_of state)));
   3.168 +fun use_mltext verbose (txt, pos) = Toplevel.keep' (fn int => fn state =>
   3.169 +  (ML_Context.use_mltext (verbose andalso int) pos txt (try Toplevel.generic_theory_of state)));
   3.170  
   3.171  val use_commit = Toplevel.imperative Secure.commit;
   3.172  

     4.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Mar 24 18:44:21 2008 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 24 23:34:24 2008 +0100
     4.3 @@ -307,41 +307,41 @@
     4.4  
     4.5  val _ =
     4.6    OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
     4.7 -    (P.text >> IsarCmd.use_mltext true);
     4.8 +    (P.position P.text >> IsarCmd.use_mltext true);
     4.9  
    4.10  val _ =
    4.11    OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
    4.12 -    (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
    4.13 +    (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
    4.14  
    4.15  val _ =
    4.16    OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
    4.17 -    (P.text >> IsarCmd.use_mltext_theory);
    4.18 +    (P.position P.text >> IsarCmd.use_mltext_theory);
    4.19  
    4.20  val _ =
    4.21    OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
    4.22 -    (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup));
    4.23 +    (Scan.option (P.position P.text) >> (Toplevel.theory o IsarCmd.generic_setup));
    4.24  
    4.25  val _ =
    4.26    OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
    4.27 -    (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
    4.28 -      >> (Toplevel.theory o Method.method_setup));
    4.29 +    (P.name -- P.!!! (P.$$$ "=" |-- P.position P.text -- P.text)
    4.30 +    >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
    4.31  
    4.32  val _ =
    4.33    OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
    4.34 -    (P.opt_target -- P.text
    4.35 +    (P.opt_target -- P.position P.text
    4.36      >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
    4.37  
    4.38  val _ =
    4.39    OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
    4.40      (P.opt_target --
    4.41 -      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text --
    4.42 -      Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
    4.43 +      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
    4.44 +      P.position P.text -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
    4.45      >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
    4.46  
    4.47  
    4.48  (* translation functions *)
    4.49  
    4.50 -val trfun = P.opt_keyword "advanced" -- P.text;
    4.51 +val trfun = P.opt_keyword "advanced" -- P.position P.text;
    4.52  
    4.53  val _ =
    4.54    OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
    4.55 @@ -371,7 +371,7 @@
    4.56  val _ =
    4.57    OuterSyntax.command "token_translation" "install token translation functions"
    4.58      (K.tag_ml K.thy_decl)
    4.59 -    (P.text >> (Toplevel.theory o IsarCmd.token_translation));
    4.60 +    (P.position P.text >> (Toplevel.theory o IsarCmd.token_translation));
    4.61  
    4.62  
    4.63  (* oracles *)
    4.64 @@ -379,7 +379,7 @@
    4.65  val _ =
    4.66    OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
    4.67      (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
    4.68 -      -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
    4.69 +      -- P.position P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
    4.70  
    4.71  
    4.72  (* local theories *)

     5.1 --- a/src/Pure/Isar/method.ML	Mon Mar 24 18:44:21 2008 +0100
     5.2 +++ b/src/Pure/Isar/method.ML	Mon Mar 24 23:34:24 2008 +0100
     5.3 @@ -52,7 +52,7 @@
     5.4    val frule: int -> thm list -> method
     5.5    val iprover_tac: Proof.context -> int option -> int -> tactic
     5.6    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
     5.7 -  val tactic: string -> Proof.context -> method
     5.8 +  val tactic: string * Position.T -> Proof.context -> method
     5.9    type src
    5.10    datatype text =
    5.11      Basic of (Proof.context -> method) * Position.T |
    5.12 @@ -76,7 +76,7 @@
    5.13      -> theory -> theory
    5.14    val add_method: bstring * (src -> Proof.context -> method) * string
    5.15      -> theory -> theory
    5.16 -  val method_setup: bstring * string * string -> theory -> theory
    5.17 +  val method_setup: bstring -> string * Position.T -> string -> theory -> theory
    5.18    val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
    5.19      -> src -> Proof.context -> 'a * Proof.context
    5.20    val simple_args: (Args.T list -> 'a * Args.T list)
    5.21 @@ -353,10 +353,10 @@
    5.22  val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
    5.23  fun set_tactic f = tactic_ref := f;
    5.24  
    5.25 -fun ml_tactic txt ctxt = NAMED_CRITICAL "ML" (fn () =>
    5.26 -  (ML_Context.use_mltext
    5.27 +fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () =>
    5.28 +  (ML_Context.use_mltext false pos
    5.29      ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
    5.30 -      ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
    5.31 +      ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt));
    5.32      ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
    5.33  
    5.34  fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
    5.35 @@ -446,8 +446,8 @@
    5.36  
    5.37  (* method_setup *)
    5.38  
    5.39 -fun method_setup (name, txt, cmt) =
    5.40 -  ML_Context.use_let
    5.41 +fun method_setup name (txt, pos) cmt =
    5.42 +  ML_Context.use_let pos
    5.43      "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
    5.44      "Context.map_theory (Method.add_method method)"
    5.45      ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")
    5.46 @@ -577,8 +577,8 @@
    5.47      "rename parameters of goal"),
    5.48    ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
    5.49      "rotate assumptions of goal"),
    5.50 -  ("tactic", simple_args Args.name tactic, "ML tactic as proof method"),
    5.51 -  ("raw_tactic", simple_args Args.name raw_tactic, "ML tactic as raw proof method")]);
    5.52 +  ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
    5.53 +  ("raw_tactic", simple_args (Args.position Args.name) raw_tactic, "ML tactic as raw proof method")]);
    5.54  
    5.55  
    5.56  (* outer parser *)

     6.1 --- a/src/Pure/ML-Systems/alice.ML	Mon Mar 24 18:44:21 2008 +0100
     6.2 +++ b/src/Pure/ML-Systems/alice.ML	Mon Mar 24 23:34:24 2008 +0100
     6.3 @@ -117,9 +117,8 @@
     6.4  
     6.5  (* ML command execution *)
     6.6  
     6.7 -fun use_text tune name (print, err) verbose txt = (Compiler.eval txt; ());
     6.8 -
     6.9 -fun use_file tune output verbose name = use name;
    6.10 +fun use_text _ _ _ _ txt = (Compiler.eval txt; ());
    6.11 +fun use_file _ _ _ name = use name;
    6.12  
    6.13  
    6.14  

     7.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon Mar 24 18:44:21 2008 +0100
     7.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Mar 24 23:34:24 2008 +0100
     7.3 @@ -22,24 +22,24 @@
     7.4  
     7.5  (* improved versions of use_text/file *)
     7.6  
     7.7 -fun use_text (tune: string -> string) name (print, err) verbose txt =
     7.8 +fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
     7.9    let
    7.10      val in_buffer = ref (String.explode (tune txt));
    7.11      val out_buffer = ref ([]: string list);
    7.12      fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    7.13  
    7.14 -    val line_no = ref 1;
    7.15 -    fun line () = ! line_no;
    7.16 +    val current_line = ref line;
    7.17      fun get () =
    7.18        (case ! in_buffer of
    7.19          [] => NONE
    7.20 -      | c :: cs => (in_buffer := cs; if c = #"\n" then line_no := ! line_no + 1 else (); SOME c));
    7.21 +      | c :: cs =>
    7.22 +          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    7.23      fun put s = out_buffer := s :: ! out_buffer;
    7.24  
    7.25      val _ =
    7.26        (while not (List.null (! in_buffer)) do
    7.27          PolyML.compiler
    7.28 -          {getChar = get, putString = put, lineNumber = line, fileName = name,
    7.29 +          {getChar = get, putString = put, lineNumber = fn () => ! current_line, fileName = name,
    7.30              nameSpace = PolyML.globalNameSpace} ())
    7.31        handle exn => (err (output ()); raise exn);
    7.32    in
    7.33 @@ -50,5 +50,5 @@
    7.34    let
    7.35      val instream = TextIO.openIn name;
    7.36      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    7.37 -  in use_text tune name output verbose txt end;
    7.38 +  in use_text tune (1, name) output verbose txt end;
    7.39  

     8.1 --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 24 18:44:21 2008 +0100
     8.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 24 23:34:24 2008 +0100
     8.3 @@ -1,10 +1,10 @@
     8.4  (*  Title:      Pure/ML-Systems/polyml_old_compiler4.ML
     8.5      ID:         $Id$
     8.6  
     8.7 -Runtime compilation -- for old version of PolyML.compiler (version 4.x).
     8.8 +Runtime compilation -- for old PolyML.compiler (version 4.x).
     8.9  *)
    8.10  
    8.11 -fun use_text (tune: string -> string) name (print, err) verbose txt =
    8.12 +fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
    8.13    let
    8.14      val in_buffer = ref (explode (tune txt));
    8.15      val out_buffer = ref ([]: string list);
    8.16 @@ -30,5 +30,5 @@
    8.17    let
    8.18      val instream = TextIO.openIn name;
    8.19      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    8.20 -  in use_text tune name output verbose txt end;
    8.21 +  in use_text tune (1, name) output verbose txt end;
    8.22  

     9.1 --- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 24 18:44:21 2008 +0100
     9.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 24 23:34:24 2008 +0100
     9.3 @@ -1,27 +1,26 @@
     9.4  (*  Title:      Pure/ML-Systems/polyml_old_compiler5.ML
     9.5      ID:         $Id$
     9.6  
     9.7 -Runtime compilation -- for old version of PolyML.compilerEx (version 5.0, 5.1).
     9.8 +Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
     9.9  *)
    9.10  
    9.11 -fun use_text (tune: string -> string) name (print, err) verbose txt =
    9.12 +fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
    9.13    let
    9.14      val in_buffer = ref (explode (tune txt));
    9.15      val out_buffer = ref ([]: string list);
    9.16      fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    9.17  
    9.18 -    val line_no = ref 1;
    9.19 -    fun line () = ! line_no;
    9.20 +    val current_line = ref line;
    9.21      fun get () =
    9.22        (case ! in_buffer of
    9.23          [] => ""
    9.24 -      | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
    9.25 +      | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
    9.26      fun put s = out_buffer := s :: ! out_buffer;
    9.27  
    9.28      fun exec () =
    9.29        (case ! in_buffer of
    9.30          [] => ()
    9.31 -      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
    9.32 +      | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
    9.33    in
    9.34      exec () handle exn => (err (output ()); raise exn);
    9.35      if verbose then print (output ()) else ()
    9.36 @@ -31,5 +30,5 @@
    9.37    let
    9.38      val instream = TextIO.openIn name;
    9.39      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    9.40 -  in use_text tune name output verbose txt end;
    9.41 +  in use_text tune (1, name) output verbose txt end;
    9.42  

    10.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Mar 24 18:44:21 2008 +0100
    10.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 24 23:34:24 2008 +0100
    10.3 @@ -110,7 +110,7 @@
    10.4  
    10.5  (* ML command execution *)
    10.6  
    10.7 -fun use_text (tune: string -> string) name (print, err) verbose txt =
    10.8 +fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
    10.9    let
   10.10      val ref out_orig = Control.Print.out;
   10.11  
   10.12 @@ -132,7 +132,7 @@
   10.13    let
   10.14      val instream = TextIO.openIn name;
   10.15      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
   10.16 -  in use_text tune name output verbose txt end;
   10.17 +  in use_text tune (1, name) output verbose txt end;
   10.18  
   10.19  
   10.20  

    11.1 --- a/src/Pure/ML/ml_context.ML	Mon Mar 24 18:44:21 2008 +0100
    11.2 +++ b/src/Pure/ML/ml_context.ML	Mon Mar 24 23:34:24 2008 +0100
    11.3 @@ -31,11 +31,11 @@
    11.4      (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit
    11.5    val proj_value_antiq: string -> (Context.generic * Args.T list ->
    11.6        (string * string * string) * (Context.generic * Args.T list)) -> unit
    11.7 -  val eval_antiquotes_fn: (string -> string * string) ref  (* FIXME tmp *)
    11.8 +  val eval_antiquotes_fn: (string * Position.T -> string * string) ref  (* FIXME tmp *)
    11.9    val trace: bool ref
   11.10 -  val use_mltext: string -> bool -> Context.generic option -> unit
   11.11 -  val use_mltext_update: string -> bool -> Context.generic -> Context.generic
   11.12 -  val use_let: string -> string -> string -> Context.generic -> Context.generic
   11.13 +  val use_mltext: bool -> Position.T -> string -> Context.generic option -> unit
   11.14 +  val use_mltext_update: bool -> Position.T -> string -> Context.generic -> Context.generic
   11.15 +  val use_let: Position.T -> string -> string -> string -> Context.generic -> Context.generic
   11.16    val use: Path.T -> unit
   11.17    val evaluate: (string -> unit) * (string -> 'b) -> bool ->
   11.18      string * (unit -> 'a) option ref -> string -> 'a
   11.19 @@ -141,9 +141,9 @@
   11.20  val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;";
   11.21  val isabelle_struct0 = isabelle_struct "";
   11.22  
   11.23 -fun eval_antiquotes txt =
   11.24 +fun eval_antiquotes txt_pos =
   11.25    let
   11.26 -    val ants = Antiquote.scan_antiquotes (txt, Position.line 1);
   11.27 +    val ants = Antiquote.scan_antiquotes txt_pos;
   11.28  
   11.29      fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names)
   11.30        | expand (Antiquote.Antiq x) names =
   11.31 @@ -170,50 +170,51 @@
   11.32  
   11.33  val trace = ref false;
   11.34  
   11.35 -fun eval_wrapper name pr verbose txt =
   11.36 +fun eval_wrapper pr verbose pos txt =
   11.37    let
   11.38 -    val (txt1, txt2) = ! eval_antiquotes_fn txt;  (* FIXME tmp hook *)
   11.39 +    val (txt1, txt2) = ! eval_antiquotes_fn (txt, pos);  (* FIXME tmp hook *)
   11.40      val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
   11.41 -    fun eval nm = use_text nm pr;
   11.42 +    fun eval p =
   11.43 +      use_text (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr;
   11.44    in
   11.45      NAMED_CRITICAL "ML" (fn () =>
   11.46 -      (eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0))
   11.47 +     (eval Position.none false txt1;
   11.48 +      eval pos verbose txt2;
   11.49 +      eval Position.none false isabelle_struct0))
   11.50    end;
   11.51  
   11.52 -fun ML_wrapper pr = eval_wrapper "ML" pr;
   11.53 -
   11.54  end;
   11.55  
   11.56  
   11.57  (* ML evaluation *)
   11.58  
   11.59 -fun use_mltext txt verbose opt_context =
   11.60 -  setmp opt_context (fn () => ML_wrapper Output.ml_output verbose txt) ();
   11.61 +fun use_mltext verbose pos txt opt_context =
   11.62 +  setmp opt_context (fn () => eval_wrapper Output.ml_output verbose pos txt) ();
   11.63  
   11.64 -fun use_mltext_update txt verbose context =
   11.65 -  #2 (pass_context context (fn () => ML_wrapper Output.ml_output verbose txt) ());
   11.66 +fun use_mltext_update verbose pos txt context =
   11.67 +  #2 (pass_context context (fn () => eval_wrapper Output.ml_output verbose pos txt) ());
   11.68  
   11.69 -fun use_context txt = use_mltext_update
   11.70 -  ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false;
   11.71 +fun use_let pos bind body txt =
   11.72 +  use_mltext_update false pos
   11.73 +    ("ML_Context.set_context (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
   11.74 +      " end (ML_Context.the_generic_context ())));");
   11.75  
   11.76 -fun use_let bind body txt =
   11.77 -  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   11.78 -
   11.79 -fun use path = eval_wrapper (Path.implode path) Output.ml_output true (File.read path);
   11.80 +fun use path = eval_wrapper Output.ml_output true (Position.path path) (File.read path);
   11.81  
   11.82  fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   11.83    let
   11.84      val _ = r := NONE;
   11.85 -    val _ = ML_wrapper pr verbose ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
   11.86 +    val _ = eval_wrapper pr verbose Position.none
   11.87 +      ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
   11.88    in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
   11.89  
   11.90  
   11.91  (* basic antiquotations *)
   11.92  
   11.93 +fun context x = (Scan.state >> Context.proof_of) x;
   11.94 +
   11.95  local
   11.96  
   11.97 -fun context x = (Scan.state >> Context.proof_of) x;
   11.98 -
   11.99  val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()"));
  11.100  
  11.101  val _ = inline_antiq "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) =>
  11.102 @@ -243,7 +244,7 @@
  11.103  val _ = inline_antiq "type_name" (type_ false);
  11.104  val _ = inline_antiq "type_syntax" (type_ true);
  11.105  
  11.106 -fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
  11.107 +fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) =>
  11.108    #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
  11.109    |> syn ? ProofContext.const_syntax_name ctxt
  11.110    |> ML_Syntax.print_string);
  11.111 @@ -252,7 +253,7 @@
  11.112  val _ = inline_antiq "const_syntax" (const true);
  11.113  
  11.114  val _ = inline_antiq "const"
  11.115 -  ((Scan.state >> Context.proof_of) -- Scan.lift Args.name --
  11.116 +  (context -- Scan.lift Args.name --
  11.117      Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
  11.118      >> (fn ((ctxt, c), Ts) =>
  11.119        let
  11.120 @@ -276,8 +277,7 @@
  11.121    | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
  11.122  
  11.123  fun thm_antiq kind get get_name = value_antiq kind
  11.124 -  ((Scan.state >> Context.proof_of) --
  11.125 -    Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel)
  11.126 +  (context -- Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel)
  11.127    >> (fn (ctxt, ((name, pos), sel)) =>
  11.128        let
  11.129          val _ = get ctxt (Facts.Named ((name, pos), sel));

    12.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 24 18:44:21 2008 +0100
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 24 23:34:24 2008 +0100
    12.3 @@ -501,8 +501,8 @@
    12.4  fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
    12.5  fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
    12.6  
    12.7 -fun output_ml ml src ctxt txt =
    12.8 - (ML_Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt));
    12.9 +fun output_ml ml src ctxt (txt, pos) =
   12.10 + (ML_Context.use_mltext false pos (ml txt) (SOME (Context.Proof ctxt));
   12.11    (if ! source then str_of_source src else txt)
   12.12    |> (if ! quotes then quote else I)
   12.13    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   12.14 @@ -531,8 +531,8 @@
   12.15    ("prf", args Attrib.thms (output (pretty_prf false))),
   12.16    ("full_prf", args Attrib.thms (output (pretty_prf true))),
   12.17    ("theory", args (Scan.lift Args.name) (output pretty_theory)),
   12.18 -  ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
   12.19 -  ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
   12.20 -  ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];
   12.21 +  ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)),
   12.22 +  ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)),
   12.23 +  ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))];
   12.24  
   12.25  end;

    13.1 --- a/src/Pure/codegen.ML	Mon Mar 24 18:44:21 2008 +0100
    13.2 +++ b/src/Pure/codegen.ML	Mon Mar 24 23:34:24 2008 +0100
    13.3 @@ -963,7 +963,7 @@
    13.4                    [Pretty.str "]"])]]),
    13.5            Pretty.str ");"]) ^
    13.6        "\n\nend;\n") ();
    13.7 -    val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy));
    13.8 +    val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
    13.9      fun iter f k = if k > i then NONE
   13.10        else (case (f () handle Match =>
   13.11            (if quiet then ()
   13.12 @@ -1053,7 +1053,7 @@
   13.13                [Pretty.str "(result ())"],
   13.14              Pretty.str ");"]) ^
   13.15          "\n\nend;\n";
   13.16 -      val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy))
   13.17 +      val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
   13.18      in !eval_result end) ();
   13.19    in e () end;
   13.20  
   13.21 @@ -1148,8 +1148,8 @@
   13.22         val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
   13.23         val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
   13.24       in ((case opt_fname of
   13.25 -         NONE => ML_Context.use_mltext (space_implode "\n" (map snd code))
   13.26 -           false (SOME (Context.Theory thy))
   13.27 +         NONE => ML_Context.use_mltext false Position.none (space_implode "\n" (map snd code))
   13.28 +           (SOME (Context.Theory thy))
   13.29         | SOME fname =>
   13.30             if lib then
   13.31               app (fn (name, s) => File.write

    14.1 --- a/src/Tools/Compute_Oracle/am_compiler.ML	Mon Mar 24 18:44:21 2008 +0100
    14.2 +++ b/src/Tools/Compute_Oracle/am_compiler.ML	Mon Mar 24 23:34:24 2008 +0100
    14.3 @@ -186,7 +186,7 @@
    14.4  
    14.5      in
    14.6  	compiled_rewriter := NONE;	
    14.7 -	use_text "" Output.ml_output false (!buffer);
    14.8 +	use_text (1, "") Output.ml_output false (!buffer);
    14.9  	case !compiled_rewriter of 
   14.10  	    NONE => raise (Compile "cannot communicate with compiled function")
   14.11  	  | SOME r => (compiled_rewriter := NONE; r)

    15.1 --- a/src/Tools/Compute_Oracle/am_sml.ML	Mon Mar 24 18:44:21 2008 +0100
    15.2 +++ b/src/Tools/Compute_Oracle/am_sml.ML	Mon Mar 24 23:34:24 2008 +0100
    15.3 @@ -493,7 +493,7 @@
    15.4  
    15.5  fun writeTextFile name s = File.write (Path.explode name) s
    15.6  
    15.7 -fun use_source src = use_text "" Output.ml_output false src
    15.8 +fun use_source src = use_text (1, "") Output.ml_output false src
    15.9      
   15.10  fun compile cache_patterns const_arity eqs = 
   15.11      let

    16.1 --- a/src/Tools/code/code_target.ML	Mon Mar 24 18:44:21 2008 +0100
    16.2 +++ b/src/Tools/code/code_target.ML	Mon Mar 24 23:34:24 2008 +0100
    16.3 @@ -1093,7 +1093,7 @@
    16.4  fun isar_seri_sml module file =
    16.5    let
    16.6      val output = case file
    16.7 -     of NONE => use_text "generated code" Output.ml_output false o code_output
    16.8 +     of NONE => use_text (1, "generated code") Output.ml_output false o code_output
    16.9        | SOME "-" => PrintMode.setmp [] writeln o code_output
   16.10        | SOME file => File.write (Path.explode file) o code_output;
   16.11    in