# HG changeset patch
# User wenzelm
# Date 1372233519 -7200
# Node ID 9a8f4fdac3cff10b26e9fbe45447008df534d72b
# Parent  e09e1091394d74aec9bdb48e2df39c41301f0bd0
more position information for markup;

diff -r e09e1091394d -r 9a8f4fdac3cf src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Tue Jun 25 20:38:06 2013 +0200
+++ b/src/Pure/pure_syn.ML	Wed Jun 26 09:58:39 2013 +0200
@@ -9,7 +9,8 @@
 
 val _ =
   Outer_Syntax.command
-    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
+    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
+    "begin theory context"
     (Thy_Header.args >> (fn header =>
       Toplevel.print o
         Toplevel.init_theory
@@ -17,7 +18,8 @@
 
 val _ =
   Outer_Syntax.command
-    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
+    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
+    "ML text from file"
     (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
         let
           val [{src_path, text, pos}] = files (Context.theory_of gthy);