# HG changeset patch
# User wenzelm
# Date 1392842324 -3600
# Node ID e2d71b8b0d954c27843111269f1927551ff9dcaf
# Parent  ad446b45effff7a9b2f494a1421160fe893aa9ef
prefer guarded Context_Position.report where feasible;

diff -r ad446b45efff -r e2d71b8b0d95 src/Pure/ML/ml_antiquote.ML
--- 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") #>
diff -r ad446b45efff -r e2d71b8b0d95 src/Pure/Thy/thy_load.ML
--- 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
diff -r ad446b45efff -r e2d71b8b0d95 src/Pure/Thy/thy_output.ML
--- 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;