--- a/src/Pure/ML/ml_antiquote.ML Wed Feb 19 20:56:29 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Wed Feb 19 21:38:44 2014 +0100
@@ -68,15 +68,17 @@
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
value (Binding.name "theory")
- (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
- (Position.report pos (Theory.get_markup (Context.get_theory thy name));
- "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+ (Context_Position.report ctxt pos
+ (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+ "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
value (Binding.name "theory_context")
- (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
- (Position.report pos (Theory.get_markup (Context.get_theory thy name));
- "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+ (Context_Position.report ctxt pos
+ (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+ "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))) #>
inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
--- a/src/Pure/Thy/thy_load.ML Wed Feb 19 20:56:29 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML Wed Feb 19 21:38:44 2014 +0100
@@ -199,7 +199,7 @@
val _ =
if not do_check orelse File.exists path then ()
else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
- val _ = Position.report pos (Markup.path name);
+ val _ = Context_Position.report ctxt pos (Markup.path name);
in
space_explode "/" name
|> map Thy_Output.verb_text
--- a/src/Pure/Thy/thy_output.ML Wed Feb 19 20:56:29 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Feb 19 21:38:44 2014 +0100
@@ -523,7 +523,7 @@
(case find_first (fn thy => Context.theory_name thy = name)
(Theory.nodes_of (Proof_Context.theory_of ctxt)) of
NONE => error ("No ancestor theory " ^ quote name ^ Position.here pos)
- | SOME thy => (Position.report pos (Theory.get_markup thy); Pretty.str name));
+ | SOME thy => (Context_Position.report ctxt pos (Theory.get_markup thy); Pretty.str name));
(* default output *)
@@ -670,6 +670,6 @@
val _ = Theory.setup
(antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
(fn {context = ctxt, ...} => fn (name, pos) =>
- (Position.report pos (Markup.url name); enclose "\\url{" "}" name)));
+ (Context_Position.report ctxt pos (Markup.url name); enclose "\\url{" "}" name)));
end;