--- 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) ^
--- 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 *)
--- 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;
--- 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 *)
--- 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 *)
--- 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;
--- 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;
--- 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;
--- 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;
--- 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;
--- 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));
--- 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;
--- 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
--- 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)
--- 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
--- 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